| 基于混合通信顺序进程的高速铁路列控系统形式化建模与验证方法 |
| |
| 引用本文： | 吕继东,李开成,唐涛,袁磊.基于混合通信顺序进程的高速铁路列控系统形式化建模与验证方法[J].中国铁道科学,2012,33(5):91-97. |
| |
| 作者姓名： | 吕继东 李开成 唐涛 袁磊 |
| |
| 作者单位： | 1. 北京交通大学轨道交通运行控制系统国家工程研究中心,北京,100044
2. 北京交通大学轨道交通控制与安全国家重点实验室,北京,100044 |
| |
| 基金项目： | 国家"八六三"计划项目，北京交通大学轨道交通控制与安全国家重点实验室开放课题，北京交通大学科技基金资助项目 |
| |
| 摘 要： | 针对高速铁路列控系统的混杂特性,提出一种基于混合通信顺序进程(HCSP)的列控系统形式化建模与验证方法。引入了HCSP的假设条件,建立列控系统的行为模型;定义了HCSP到混合自动机(HA)的转换规则,将HCSP模型转换成HA模型;利用模型检验工具PHAVer对HA模型进行自动验证。以高速铁路列控系统典型的行车许可运营场景为例,建立区间闭塞分区行车许可场景的HCSP模型;根据转换规则将行车许可场景的HCSP模型转换成HA模型;用PHAVer验证了所建立的区间闭塞分区行车许可场景模型的正确性,从而证明了基于HCSP的高速铁路列控系统建模及验证方法的有效性。
|
| 关 键 词： | 高速铁路列控系统 混合通信顺序进程 混合自动机 行车许可场景 |
Formal Modeling and Verification Method for High Speed Train Control System Based on Hybrid Communicating Sequential Process |
| |
| L Jidong
,
LI Kaicheng
,
TANG Tao
,
YUAN Lei.Formal Modeling and Verification Method for High Speed Train Control System Based on Hybrid Communicating Sequential Process[J].China Railway Science,2012,33(5):91-97. |
| |
| Authors: | L Jidong LI Kaicheng TANG Tao YUAN Lei |
| |
| Institution: | 1.National Engineering Research Center of Rail Transportation Operation and Control System,Beijing Jiaotong University,Beijing 100044,China; 2.State Key Laboratory of Rail Traffic Control and Safety,Beijing Jiaotong University,Beijing 100044,China) |
| |
| Abstract: | |
| |
| Keywords: | |
| 本文献已被 CNKI 万方数据 等数据库收录！ |
|
