| CTCS-3级列控系统车地交互流程形式化建模与验证 |
| |
| 引用本文： | 刘中田,吕继东,孙伟亮. CTCS-3级列控系统车地交互流程形式化建模与验证[J]. 北京交通大学学报(自然科学版), 2011, 35(2) |
| |
| 作者姓名： | 刘中田 吕继东 孙伟亮 |
| |
| 作者单位： | 北京交通大学,电子信息工程学院,北京,100044;北京交通大学,电子信息工程学院,北京,100044;北京交通大学,电子信息工程学院,北京,100044 |
| |
| 基金项目： | 国家“863”计划项目资助(0912JJ0104-XH00-H-HZ-001-20100419); 北京交通大学科技基金项目资助(2007XM004) |
| |
| 摘 要： | 正在建设的时速300 km/h以上的高速铁路已采用CTCS-3级列车运行控制系统.车地信息交互流程是影响CTCS-3级列控系统的效率、可靠性和安全性的主要因素之一.基于时间自动机理论对车地交互流程进行建模与验证具有重要意义.首先将车地交互流程分为4个典型的子流程:任务启动流程、正常行车流程、RBC切换流程和任务结束流程,然后针对这些子流程建立无线闭塞中心(RBC)、车载设备(ATP)和铁路专用移动通信网(GSM-R)的时间自动机网络模型,最后利用时间自动机模型验证工具UPPAAL进行仿真分析,验证了CTCS-3级列控系统的车地交互流程的安全性和受限活性.
|
| 关 键 词： | 列车运行控制系统 车地信息交互流程 形式化建模与验证 时间自动机 |
Formal modeling and checking of procedure message exchange between train-ground for CTCS level 3 |
| |
| LIU Zhongtian,LU Jidong,SUN Weiliang. Formal modeling and checking of procedure message exchange between train-ground for CTCS level 3[J]. JOURNAL OF BEIJING JIAOTONG UNIVERSITY, 2011, 35(2) |
| |
| Authors: | LIU Zhongtian LU Jidong SUN Weiliang |
| |
| Affiliation: | LIU Zhongtian,LU Jidong,SUN Weiliang(School of Electronics and Information Engineering,Beijing Jiaotong University,Beijing 100044,China) |
| |
| Abstract: | It is confirmed that the chinese train control system(CTCS) level 3 is adopted in newly-built railway lines,where the train speed is expected to exceed 300 kilometers per hour.Procedure message exchange between train and ground is one of the most significant factors that affect the transportation efficiency,reliability and safety of the CTCS level 3.It is very important to use time automata for formal modeling and checking of procedure message exchange between train and ground.Firstly,we divide procedure me... |
| |
| Keywords: | chinese train control system(CTCS) procedure message exchange between train and ground formal modeling and checking time automata |
| 本文献已被 CNKI 万方数据 等数据库收录！ |
