CTCS-3级列控系统车地交互流程形式化建模与验证
刘中田
吕继东
孙伟亮
1.北京交通大学,电子信息工程学院,北京,1000442.北京交通大学,电子信息工程学院,北京,1000443.北京交通大学,电子信息工程学院,北京,100044
摘要：正在建设的时速300km/h以上的高速铁路已采用CTCS-3级列车运行控制系统.车地信息交互流程是影响CTCS-3级列控系统的效率、可靠性和安全性的主要因素之一.基于时间自动机理论对车地交互流程进行建模与验证具有重要意义.首先将车地交互流程分为4个典型的子流程:任务启动流程、正常行车流程、RBC切换流程和任务结束流程,然后针对这些子流程建立无线闭塞中心(RBC)、车载设备(ATP)和铁路专用移动通信网(GSM-R)的时间自动机网络模型,最后利用时间自动机模型验证工具UPPAAL进行仿真分析,验证了CTCS-3级列控系统的车地交互流程的安全性和受限活性.
关键词：列车运行控制系统车地信息交互流程形式化建模与验证时间自动机
分类号：TP391.9(计算技术、计算机技术)
资助基金：国家"863"计划项目资助(0912JJ0104-XH00-H-HZ-00 1-20100419)北京交通大学科技基金项目资助(2007XM004)
论文发表日期：2011-01-01
在线出版日期：2025-08-15（本平台首次上网日期，不代表文献的发表时间）
页数：6( 76-81 )
英文信息