基于时间自动机的CTCS-3级列控车载设备建模与验证

摘要

铁路系统历来对安全性要求较高,CTCS-3级列控设备作为高速列车的控制系统对安全性的要求更高。车载设备系统是中国铁路CTCS-3级列控系统中的重要组成部分,UPPAAL是一种基于时间自动机理论的实时系统分析建模验证工具,使用UPPAAL对CTCS-3级列控系统车载设备中的车载安全计算机VC、司机-车载设备接口DMI和无线闭塞中心RBC进行分析建模验证,可以验证车载设备系统的特性。研究车载设备系统的建模,对于完善车载设备仿真系统性能、加快车载设备系统软件设计、节省现场测试成本等具有重要的现实意义。
　　 论文完成的主要工作如下:
　　 1.概述了国内外基于形式化方法和时间自动机理论的列控系统建模的研究现状,提出了用时间自动机对车载设备建模的意义。
　　 2.介绍了CTCS-3级列控车载设备结构、功能以及工作模式。
　　 3.分析了工作在CTCS-3级时的车载任务启动流程、车载越行流程、列车冒进后防护流程、司机触发的SH流程和车载任务结束流程,建立了各个工作流程的状态转换图,说明了车载设备的信息交互及状态转换过程。
　　 4.介绍了时间自动机理论及其模型检验工具UPPAAL的使用方法。
　　 5.基于时间自动机理论对VC、DMI和RBC分别建模:根据研究对象的特点,在合理的抽象和假设之后,确定了各个模型的状态,状态转换路径、状态转换的约束条件和触发事件,得到了车载设备的各个时间自动机模型。
　　 6.通过使用UPPAAL对车载设备系统的时间自动机模型进行了分析；使用模拟器,通过实验随机得到了车载设备各实体之间通过通道相互通信、控制消息序列,仿真了车载设备工作流程时序图,分析了车载设备系统模型中的状态变化；使用验证器,通过快速搜索整个系统的状态空间,验证了车载设备系统的可达性、时间特性、安全性和活性等各项特性。