普适计算应用时空性质的运行时验证

来源：软件学报杂志2018年第6期北京时间：

作者：李晅松,陶先平,宋巍

单位：李晅松，南京理工大学 计算机科学与工程学院, 江苏 南京 210094;计算机软件新技术国家重点实验室(南京大学), 江苏 南京 21002311,陶先平，计算机软件新技术国家重点实验室(南京大学), 江苏 南京 21002302,宋巍，南京理工大学 计算机科学与工程学院, 江苏 南京 210094;计算机软件新技术国家重点实验室(南京大学), 江苏 南京 21002303

摘要：运行时验证是提升普适计算应用可靠性的重要手段.这类应用的很多性质同时涉及时间关系和空间位置关系，这样的时空性质给运行时的验证带来了特有挑战：一方面，传统的时态逻辑难以描述空间性质；另一方面，适合描述空间性质的Ambient Logic在真值不确定等情况下不能很好地支持有限轨迹中时间性质的描述.为支持普适计算应用时空性质的运行时验证，引入三值逻辑语义，提出了AL3（3-valued ambient logic）；并在此基础上设计实现了基于AL3的性质检验算法和运行时监控器.最后，通过案例分析和运行效率实验阐明了所提方法的有效性和可行性.

关键词：普适计算;三值语义;运行时验证

基金资助：国家重点研发计划（2017YFB1001801）；国家自然科学基金（61702263，61373011）；江苏省自然科学基金（BK20171427）；中央高校基本科研业务费专项资金（30917011322）