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

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

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

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

矿井机车自主驾驶过程的建模及验证

文章首先使用自然语言描述了矿井机车自主驾驶系统的结构和控制过程;然后基于时间自动机理论对自主驾驶中涉及的机车控制器、机车运行服务器以及其他车载设备、被控对象建模,从而得到自主驾驶的时间自动机网络模型;最后应用时间自动机模型验证工具UPPAAL对自主驾驶模型进行了仿真分析和验证。验证结果表明建立的模型满足系统的功能性需求和实时性需求,证明了系统设计的正确性。