摘要
高速铁路列车运行控制系统是保证列车安全、高效运行的核心设备,如何验证系统功能的正确性从而提高系统的安全性是至关重要的。引入了一种基于进程演算的方法—混合通信顺序进程(HCSP,Hybrid Communication Sequential Process),利用该方法对列控系统进行了形式化描述,并针对典型的场景—注册与启动场景进行了HCSP建模,通过引入转换规则,进行了相应模型转换,应用模型检验工具UPPAAL进行了仿真和功能验证,验证结论表明了场景模型功能的正确性以及方法的可行性。
The high speed train control system is a core equipment, which plays an important role in assuring safety and improving efficiency in railway. How to verify the correctness of the functions of system in order to improve the safety is especially important. In this article, the process calculus based method called hybrid communication sequential process(HCSP) was introduced. The formal description to the train control system was taken by HCSP. For typical scenarios, the scenarios of registration and start up were modeled by HCSP. By introducing transition rules,the corresponding model transformation was carried out. The model checking tool UPPAAL was used to simulate and verify the function. The results showed that the model was correct and the method was feasible.
作者
吕继东
唐涛
李开成
王海峰
LV Jidong;TANG Tao;LI Kaicheng;WANG Haifeng(National Engineering Research Center of Rail Transportation Operation and Control System, Beijing Jiaotong University, Beijing 100044, China)
出处
《铁路计算机应用》
2017年第1期11-17,共7页
Railway Computer Application
基金
国家自然科学基金资助项目(61304185)
中国铁路总公司科技研究开发计划课题(2014X003-D)
关键词
列车运行控制系统
安全性
混合通信顺序进程
注册与启动
模型转换
验证
train control system
safety
hybrid communication sequential process(HCSP)
registration and start up
model transition
verification