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