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

• 作者: 宋巍 李晅松 陶先平
• 来源期刊: 软件学报
• 学科: 工学
• 关键词: 普适计算 三值语义 运行时验证
• 年，卷（期）: 2018,（6）
• 所属期刊栏目: 形式化方法的理论基础专题
• 页码范围: 1622-1634
• 页数: 13页
• 分类号: TP301
• 字数: 11057字
• 语种: 中文
• DOI: 10.13328/j.cnki.jos.005466

摘要

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