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

作者：吕继东; 李开成; 唐涛; 袁磊

来源：中国铁道科学, 2012, (05): 91-97.

• 高速铁路列控系统
• 混合通信顺序进程
• 混合自动机
• 行车许可场景 High speed train control system
• Hybrid communicating sequential process
• Hybrid automata
• Movement authority scenario

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

• 单位
  轨道交通控制与安全国家重点实验室; 北京交通大学