基于HCSP的列控系统安全性建模与验证分析

Modeling and verification analysis for safety property of HCSP based train control system

高速铁路列车运行控制系统是保证列车安全、高效运行的核心设备,如何验证系统功能的正确性从而提高系统的安全性是至关重要的。引入了一种基于进程演算的方法—混合通信顺序进程(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.