摘要
探讨基于时间自动机理论进行物联网系统建模和模型检测的理论、方法、工具和实践。对时间自动机的基础理论进行比较全面和精确的论述,完善部分概念及其精确的形式化定义。提出基于时间自动机理论进行建模的方法,并指出时间自动机理论研究对物联网系统建模的指导意义。介绍时间自动机的建模工具UPPAAL,说明基于UPPAAL建立时间自动机模型的建模、仿真和检测方法。结合物联网系统中一个经典的温度感知服务的系统需求、理论与实践相结合,进行温度感知管理系统时间自动机建模,并进行模型仿真与模型检测。实验结果表明,该系统能够正确感知温度,具有容错性且不会陷入死锁。
-
单位中国科学院新疆理化技术研究所; 中国科学院大学; 江苏中科西北星信息科技有限公司