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

摘要

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.%针对高速铁路列控系统的混杂特性,提出一种基于混合通信顺序进程(HCSP)的列控系统形式化建模与验证方法.引入了HCSP的假设条件,建立列控系统的行为模型；定义了HCSP到混合自动机(HA)的转换规则,将HCSP模型转换成HA模型；利用模型检验工具PHAVer对HA模型进行自动验证.以高速铁路列控系统典型的行车许可运营场景为例,建立区间闭塞分区行车许可场景的HCSP模型；根据转换规则将行车许可场景的HCSP模型转换成HA模型；用PHAVer验证了所建立的区间闭塞分区行车许可场景模型的正确性,从而证明了基于HCSP的高速铁路列控系统建模及验证方法的有效性.