| CTCS-3级列控系统车地交互流程形式化建模与验证 |
| |
| 引用本文： | 刘中田,吕继东,孙伟亮.CTCS-3级列控系统车地交互流程形式化建模与验证[J].Canadian Metallurgical Quarterly,2011,35(2). |
| |
| 作者姓名： | 刘中田 吕继东 孙伟亮 |
| |
| 作者单位： | 北京交通大学,电子信息工程学院,北京,100044 |
| |
| 基金项目： | 国家"863"计划项目资助，北京交通大学科技基金资助 |
| |
| 摘 要： | 正在建设的时速300km/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].Canadian Metallurgical Quarterly,2011,35(2). |
| |
| Authors: | LIU Zhongtian LU Jidong SUN Weiliang |
| |
| Abstract: | |
| |
| Keywords: | |
| 本文献已被 万方数据 等数据库收录！ |
