CTCS-3级列控系统车地交互流程形式化建模与验证

• 作者: 刘中田 吕继东 孙伟亮
• 来源期刊: 北京交通大学学报
• 学科: 工学
• 关键词: 列车运行控制系统 车地信息交互流程 形式化建模与验证 时间自动机
• 年，卷（期）: 2011,（2）
• 所属期刊栏目: 电子信息工程
• 页码范围: 76-81
• 分类号: TP391.9
• 字数: 4194字
• 语种: 中文
• DOI: 10.3969/j.issn.1673-0291.2011.02.014

摘要

正在建设的时速300km/h以上的高速铁路已采用CTCS-3级列车运行控制系统.车地信息交互流程是影响CTCS-3级列控系统的效率、可靠性和安全性的主要因素之一.基于时间自动机理论对车地交互流程进行建模与验证具有重要意义.首先将车地交互流程分为4个典型的子流程:任务启动流程、正常行车流程、RBC切换流程和任务结束流程,然后针对这些子流程建立无线闭塞中心(RBC)、车载设备(ATP)和铁路专用移动通信网(GSM-R)的时间自动机网络模型,最后利用时间自动机模型验证工具UPPAAL进行仿真分析,验证了CTCS-3级列控系统的车地交互流程的安全性和受限活性.

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	刘中田	北京交通大学电子信息工程学院	24	145	7.0	10.0
2	吕继东	北京交通大学电子信息工程学院	25	310	9.0	17.0
3	孙伟亮	北京交通大学电子信息工程学院	3	28	3.0	3.0