摘要:物联网设备的使用范围正在不断扩张. 模型检测是提升这类设备可靠性和安全性的有效手段, 但常用的模型检测方法不能很好地刻画这类设备常见的跨空间移动和通信行为. 为此, 提出一种面向物联网设备移动与通信行为的建模及验证方法, 以实现对这类设备时空相关性质的验证. 通过将推拉动作和全局通信机制融入ambient calculus, 提出全局通信移动环境演算(ACGC)并给出了ACGC对ambient logic的模型检测算法; 在此基础上, 提出描述物联网设备移动和通信行为的移动通信建模语言(MLMC), 并给出将MLMC描述转换为ACGC模型的方法; 进一步地, 实现模型检测工具ACGCCk以验证物联网设备的性质是否得到满足, 并通过一些优化加快检测速度; 最后, 通过案例研究和实验分析阐明所提方法的有效性.

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

摘要:面向动作的上下文感知（activity-oriented context-aware，简称AOCA）应用组织环境中的资源，为用户动作的顺利进行提供支持.为应对环境和动作相关需求的开放性，这类应用采用轻量级、增量式的开发方法进行开发.相对于在开发阶段描述全局信息的开发方法，AOCA应用的开发可能由不同开发者在不同时间共同参与，这可能会导致较多的不一致等问题，且难以在开发阶段被发现.围绕使用运行时验证手段提高AOCA应用可靠性这一目标展开研究.给出了对于AOCA应用运行状态进行形式化规约、对于系统级和应用级性质进行描述的方法.进一步地设计实现了AOCA应用监控器.最后，通过案例分析以及性能评估证实了该方法的有效性.