主页期刊介绍编委会编辑部服务介绍道德声明在线审稿编委办公编辑办公English
2018-2019年专刊出版计划 微信服务介绍 最新一期:2018年第12期
     
在线出版
各期目录
纸质出版
分辑系列
论文检索
论文排行
综述文章
专刊文章
美文分享
各期封面
E-mail Alerts
RSS
旧版入口
中国科学院软件研究所
  
投稿指南 问题解答 下载区 收费标准 在线投稿
李晅松,陶先平,宋巍.普适计算应用时空性质的运行时验证.软件学报,2018,29(6):1622-1634
普适计算应用时空性质的运行时验证
Runtime Verification of Spatio-Temporal Properties for Pervasive Computing Applications
投稿时间:2017-07-01  修订日期:2017-09-01
DOI:10.13328/j.cnki.jos.005466
中文关键词:  普适计算  三值语义  运行时验证
英文关键词:pervasive computing  3-value semantics  runtime verification
基金项目:国家重点研发计划(2017YFB1001801);国家自然科学基金(61702263,61373011);江苏省自然科学基金(BK20171427);中央高校基本科研业务费专项资金(30917011322)
作者单位E-mail
李晅松 南京理工大学 计算机科学与工程学院, 江苏 南京 210094
计算机软件新技术国家重点实验室(南京大学), 江苏 南京 210023 
lixs@njust.edu.cn 
陶先平 计算机软件新技术国家重点实验室(南京大学), 江苏 南京 210023  
宋巍 南京理工大学 计算机科学与工程学院, 江苏 南京 210094
计算机软件新技术国家重点实验室(南京大学), 江苏 南京 210023 
 
摘要点击次数: 646
全文下载次数: 476
中文摘要:
      运行时验证是提升普适计算应用可靠性的重要手段.这类应用的很多性质同时涉及时间关系和空间位置关系,这样的时空性质给运行时的验证带来了特有挑战:一方面,传统的时态逻辑难以描述空间性质;另一方面,适合描述空间性质的Ambient Logic在真值不确定等情况下不能很好地支持有限轨迹中时间性质的描述.为支持普适计算应用时空性质的运行时验证,引入三值逻辑语义,提出了AL3(3-valued ambient logic);并在此基础上设计实现了基于AL3的性质检验算法和运行时监控器.最后,通过案例分析和运行效率实验阐明了所提方法的有效性和可行性.
英文摘要:
      Runtime verification is an important method for improving software reliability of pervasive computing applications. Some properties of these applications consider both temporal and spatial relationships. Such spatio-temporal properties bring some specific challenges for runtime verification. On one hand, traditional temporal logic cannot describe spatial properties. On the other hand, while ambient logic is suitable for spatial properties, it does not properly support the description of temporal properties in finite traces, especially when the truth values cannot be decided. In order to support the runtime verification of spatio-temporal properties for pervasive computing applications, this paper firstly imports 3-valued semantics and proposes AL3 (3-valued ambient logic). On the basis of AL3, it designs and implements an algorithm for properties checking and a runtime monitor. Moreover, the paper uses a case study and a performance measurement to clarify the usability and feasibility of the proposed approach.
HTML  下载PDF全文  查看/发表评论  下载PDF阅读器
 

京公网安备 11040202500064号

主办单位:中国科学院软件研究所 中国计算机学会
编辑部电话:+86-10-62562563 E-mail: jos@iscas.ac.cn
Copyright 中国科学院软件研究所《软件学报》版权所有 All Rights Reserved
本刊全文数据库版权所有,未经许可,不得转载,本刊保留追究法律责任的权利