物联网系统时间自动机建模的研究与应用

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

面向全自动运行的城轨交通火灾联动方案设计与建模验证

全自动运行是未来城市轨道交通发展的主要方向,与传统驾驶模式相比,对于特殊运行场景下的应急处理能力与处理效率有着更高的要求。本文基于列车发生火灾的特殊运行场景,区别于以往由调度人员作为综合监控系统与列车自动监督系统的联动桥梁,设计了全自动驾驶场景下的火灾联动方案,确定了火灾报警系统的火灾识别流程、列车控制管理系统的数据转发和应急控制流程、运行控制中心的火灾响应流程,以及各系统之间的通信校验流程;同时,使用基于时间自动机理论的UPPAAL工具,对从火灾识别到火灾应急响应的全过程进行了形式化建模分析,并且对该联动方案的安全性和功能进行了形式化验证。验证结果表明,该联动方案能够有效地满足各个系统之间的联动要求,为全自动驾驶模式下的非正常运行场景的应急联动处理打下基础。

一种基于时间自动机的安全智能合约生成方法

区块链是一种去中心化的计算范式,在诸多领域具有良好的应用前景。智能合约是区块链应用的关键,然而,智能合约的安全问题时有发生,有些甚至造成重大的经济损失。为了避免智能合约在设计开发阶段出现由逻辑不严谨或错误逻辑所造成的安全漏洞,提出一种基于时间自动机模型的安全智能合约生成方法。相较于直接编写合约代码,该方法通过将证明为正确的模型转换为可执行的智能合约代码,有效解决在智能合约开发设计阶段所存在的安全性问题。利用UPPAAL工具将人类可理解的文本合约建模为时间自动机并通过模型验证来确保模型的安全性和可靠性。通过对智能合约的正式定义建立时间自动机与智能合约的映射规则,根据相应的映射规则,时间自动机被转换为模块化的Solidity智能合约代码。设计一个具体的商品预售活动案例进行分析,结果表明,通过所提方法生成的商品预售合约的Solidity代码可成功编译并部署在以太坊测试网络中。