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

计算机科学 ›› 2013, Vol. 40 ›› Issue (Z11): 94-97.

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

王瑾,孙景昊,何兴权,孟亚坤

东北大学计算机与通信工程学院沈阳510275;东北大学计算机与通信工程学院沈阳510275;东北大学计算机与通信工程学院沈阳510275;东北大学计算机与通信工程学院沈阳510275

出版日期:2018-11-16 发布日期:2018-11-16
基金资助:
本文受河北省青年科学基金项目(F2013501048),秦皇岛市科技支撑计划(2012021A101)资助

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

WANG Jin,SUN Jing-hao,HE Xing-quan and MENG Ya-kun

Online:2018-11-16 Published:2018-11-16

摘要/Abstract

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

关键词: 重载列车,安全监测,时间自动机,UppAal

Abstract: 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．

Key words: Heavy haul railway,Safety supervision,Timed automaton,UppAal

王瑾,孙景昊,何兴权,孟亚坤. 重载列车上人员攀车行为感知及其时间自动机模型[J]. 计算机科学, 2013, 40(Z11): 94-97. https://doi.org/

WANG Jin,SUN Jing-hao,HE Xing-quan and MENG Ya-kun. Safety Supervision System for Heavy Haul Railway:Timed Automaton Model and Verfication[J]. Computer Science, 2013, 40(Z11): 94-97. https://doi.org/

参考文献

[1] 姜子英,程建平,刘森林,等.我国煤电的外部成本初步研究[J].煤炭学报,2008,5(11):1325-1328
[2] 陈雍君,周磊山,余吉安.重载铁路列车运行调整计划的序优化策略研究[J].铁道学报,2013,5(1):1-7
[3] 孙景昊,白秋果,刘杰民.港口铁水联运信息协同平台关键技术研究[R].北戴河:东北大学,2012
[4] Aho A V,Ullman J D．Fundations of computer science[M]．New York:Computer Science Press,1992
[5] Lee E A．Cyber-Physical Systems-Are Computing Foundations Adequate?[C]∥Position Paper for NSF Workshop On Cyber-Physical Systems:Research Motivation,Techniques and Roadmap．2006
[6] Alur R,Dill D．A theory of timed automata[J]．TheoreticalComputer Science,1994,126:183-235
[7] 谭国真,孙景昊,王宝财,等．时变网络中国邮路问题的时间自动机模型[J].软件学报,2011,22(6):1267-1280
[8] Behrmann G,David A,Larsen K G．A tutorial on UppAal:Formal methods for the design of real-time systems[M]．Berlin Heidelberg:Springer,2004:200-236
[9] 李力行,金芝,李戈.基于时间自动机的物联网服务建模与验证[J].计算机学报,2011,4(8):1365-1377

Metrics

Viewed

Full text

Abstract

Cited

Shared

Discussed