中国铁道科学2012，Vol.33Issue(5)：91-97,7.DOI:10.3969/j.issn.1001-4632.2012.05.14
基于混合通信顺序进程的高速铁路列控系统形式化建模与验证方法
Formal Modeling and Verification Method for High Speed Train Control System Based on Hybrid Communicating Sequential Process
摘要
Abstract
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.关键词
高速铁路列控系统/混合通信顺序进程/混合自动机/行车许可场景Key words
High speed train control system/ Hybrid communicating sequential process/ Hybrid automata/ Movement authority scenario分类
交通工程引用本文复制引用
吕继东,李开成,唐涛,袁磊..基于混合通信顺序进程的高速铁路列控系统形式化建模与验证方法[J].中国铁道科学,2012,33(5):91-97,7.基金项目
国家"八六三"计划项目(2011AA010104) （2011AA010104）
北京交通大学轨道交通控制与安全国家重点实验室开放课题(RCS2011K010) （RCS2011K010）
北京交通大学科技基金资助项目(2012JBM024) （2012JBM024）
