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

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

作　　者：吕继东[1] 唐涛[1] 李开成[1] 王海峰[1] 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)

机构地区：[1]北京交通大学轨道交通运行控制系统国家工程研究中心

出　　处：《铁路计算机应用》2017年第1期11-17,共7页Railway Computer Application

基　　金：国家自然科学基金资助项目(61304185);中国铁路总公司科技研究开发计划课题(2014X003-D)

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

关 键 词：列车运行控制系统 安全性 混合通信顺序进程 注册与启动 模型转换 验证 

分 类 号：U284.482[交通运输工程—交通信息工程及控制] U238[交通运输工程—道路与铁道工程]