| 普适计算应用时空性质的运行时验证 |
| |
| 引用本文： | 李晅松,陶先平,宋巍. 普适计算应用时空性质的运行时验证[J]. 软件学报, 2018, 29(6): 1622-1634 |
| |
| 作者姓名： | 李晅松 陶先平 宋巍 |
| |
| 作者单位： | 南京理工大学 计算机科学与工程学院, 江苏 南京 210094;计算机软件新技术国家重点实验室(南京大学), 江苏 南京 210023,计算机软件新技术国家重点实验室(南京大学), 江苏 南京 210023,南京理工大学 计算机科学与工程学院, 江苏 南京 210094;计算机软件新技术国家重点实验室(南京大学), 江苏 南京 210023 |
| |
| 基金项目： | 国家重点研发计划（2017YFB1001801），国家自然科学基金（61702263，61373011），江苏省自然科学基金（BK20171427），中央高校基本科研业务费专项资金（30917011322） |
| |
| 摘 要： | 运行时验证是提升普适计算应用可靠性的重要手段.这类应用的很多性质同时涉及时间关系和空间位置关系，这样的时空性质给运行时验证带来了特有的挑战.一方面，传统的时态逻辑难以描述空间性质；另一方面，适合描述空间性质的Ambient Logic在真值不确定等情况下不能很好支持有限轨迹中时间性质的描述.为支持普适计算应用时空性质的运行时验证，本文引入三值逻辑语义，提出了AL3（3-valued Ambient Logic）；并在此基础上设计实现了基于AL3的性质检验算法和运行时监控器.最后，通过案例分析和运行效率实验阐明了所提方法的有效性和可行性.
|
| 关 键 词： | 普适计算 三值语义 运行时验证 |
| 收稿时间： | 2017-07-01 |
| 修稿时间： | 2017-09-01 |
Runtime Verification of Spatio-Temporal Properties for Pervasive Computing Applications |
| |
| LI Xuan-Song,TAO Xian-Ping and SONG Wei. Runtime Verification of Spatio-Temporal Properties for Pervasive Computing Applications[J]. Journal of Software, 2018, 29(6): 1622-1634 |
| |
| Authors: | LI Xuan-Song TAO Xian-Ping SONG Wei |
| |
| Affiliation: | School of Computer Science and Engineering, Nanjing University of Science and Technology, Nanjing 210094, China;State Key Laboratory for Novel Software Technology(Nanjing University), Nanjing 210023, China,State Key Laboratory for Novel Software Technology(Nanjing University), Nanjing 210023, China and School of Computer Science and Engineering, Nanjing University of Science and Technology, Nanjing 210094, China;State Key Laboratory for Novel Software Technology(Nanjing University), Nanjing 210023, China |
| |
| Abstract: | |
| |
| Keywords: | pervasive computing 3-value semantics runtime verification |
|
| 点击此处可从《软件学报》浏览原始摘要信息 |
|
点击此处可从《软件学报》下载全文 |
|
