重载列车上人员攀车行为感知及其时间自动机模型

Safety Supervision System for Heavy Haul Railway:Timed Automaton Model and Verfication

重载列车进港安全监测是我国港口信息化建设中的重点和难点问题。实现列车运行过程追踪自动化对于保证安全高效完成列车进港监测具有十分重要的作用。在速度触发的条件下,设计了能够实时感知人员攀车行为的低功耗信息物理系统,并基于时间自动机理论给出了该系统的实时行为模型。应用UppAal工具仿真了系统的运行轨迹,并验证了系统可达性、安全性、活性和实时性等系统关键性质。实验结果表明,系统不仅在逻辑上满足正确性,而且在任何系统状态上都不会对时间约束发生偏移性错误。

Safety supervision for trains approaching port is an improtant and difficult issue in China port information construction. Realizing full automation of train traveling process tracing plays a very significant role in ensuring safety and high efficiency in supervision in port. A cyber-physical system was designed to deal with the incident when some person climbs the train traveling on the heavy haul railway, and an associated timed automaton model was proposed to describe the real-time behaviors of the system. A random run sequence was simulated by the UppAal tool, and the verfication results show that the system designed in this paper satisfies the critical properties, such as reachability, security, liveness and timing constraints.