基于混合通信顺序进程的高速铁路列控系统形式化建模与验证方法  

Formal Modeling and Verification Method for High Speed Train Control System Based on Hybrid Communicating Sequential Process

作　　者：吕继东 李开成 唐涛[2] 袁磊[2] 

机构地区：[1]北京交通大学轨道交通运行控制系统国家工程研究中心,北京100044 [2]北京交通大学轨道交通控制与安全国家重点实验室,北京100044

出　　处：《中国铁道科学》2012年第5期91-97,共7页China Railway Science

基　　金：国家“八六三”计划项目(2011AA010104);北京交通大学轨道交通控制与安全国家重点实验室开放课题(RCS2011K010);北京交通大学科技基金资助项目(2012JBM024)

摘　　要：针对高速铁路列控系统的混杂特性,提出一种基于混合通信顺序进程(HCSP)的列控系统形式化建模与验证方法。引入了HCSP的假设条件,建立列控系统的行为模型;定义了HCSP到混合自动机(HA)的转换规则,将HCSP模型转换成HA模型;利用模型检验工具PHAVer对HA模型进行自动验证。以高速铁路列控系统典型的行车许可运营场景为例,建立区间闭塞分区行车许可场景的HCSP模型;根据转换规则将行车许可场景的HCSP模型转换成HA模型;用PHAVer验证了所建立的区间闭塞分区行车许可场景模型的正确性,从而证明了基于HCSP的高速铁路列控系统建模及验证方法的有效性。According to the hybrid characteristics of high speed train control system, a formal modeling and verification method for train control system is proposed based on Hybrid Communicating Sequential Process (HCSP). HCSP assumed conditions are introduced to establish the behavior model of train control system. The transformation rules from HCSP to hybrid automata (HA) are defined so as to convert HCSP model into HA model. The HA models are automatically verified by a model checking tool PHAVer. The typical movement authority scenario of high speed train control system is taken as a case study and a HCSP model is built for the movement authority scenario of interval block section. The HCSP model of movement authority scenario is converted into HA model by the defined transformation rules. The correctness of the model built for the movement authority scenario of interval block section is validated by PHAVer. Accordingly, the proposed modeling and verification method for high speed train control system based on HCSP is proved to be effective.

关 键 词：高速铁路列控系统 混合通信顺序进程 混合自动机 行车许可场景 

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