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

• 作者: 吕继东 唐涛 李开成 袁磊
• 来源期刊: 中国铁道科学
• 学科: 交通运输
• 关键词: 高速铁路列控系统 混合通信顺序进程 混合自动机 行车许可场景
• 年，卷（期）: 2012,（5）
• 页码范围: 91-97
• 分类号: U284.482|U238
• 字数: 5379字
• 语种: 中文
• DOI: 10.3969/j.issn.1001-4632.2012.05.14

摘要

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

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	唐涛	北京交通大学轨道交通控制与安全国家重点实验室	152	2578	27.0	40.0
2	李开成	北京交通大学轨道交通运行控制系统国家工程研究中心	49	532	14.0	21.0
3	袁磊	北京交通大学轨道交通控制与安全国家重点实验室	22	164	7.0	12.0
4	吕继东	北京交通大学轨道交通运行控制系统国家工程研究中心	25	310	9.0	17.0