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

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

来源：软件学报, 2018, 29(06): 1622-1634.

DOI：10.13328/j.cnki.jos.005466

• 普适计算
• 三值语义
• 运行时验证

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

• 单位
  计算机软件新技术国家重点实验室; 南京大学; 南京理工大学