基于时间自动机的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对车载设备系统的时间自动机模型进行了分析;使用模拟器,通过实验随机得到了车载设备各实体之间通过通道相互通信、控制消息序列,仿真了车载设备工作流程时序图,分析了车载设备系统模型中的状态变化；使用验证器,通过快速搜索整个系统的状态空间,验证了车载设备系统的可达性、时间特性、安全性和活性等各项特性。

论文目录

• 摘要
• Abstract
• 第1章 绪论
• 1.1 研究背景
• 1.2 研究现状
• 1.2.1 列控系统形式化方法研究现状
• 1.2.2 列控系统时间自动机的研究现状
• 1.3 论文的研究意义
• 1.4 论文的主要内容
• 第2章 CTCS-3级列控车载设备介绍
• 2.1 CTCS-3级列车运行控制系统概述
• 2.1.1 CTCS应用等级划分
• 2.1.2 CTCS-3级列控系统基本描述
• 2.1.3 CTCS-3级列控地面设备
• 2.1.4 CTCS-3级列控车载设备
• 2.2 CTCS-3级列控车载设备功能
• 2.3 CTCS-3级列控车载设备工作模式
• 第3章 CTCS-3级列控车载设备工作流程分析
• 3.1 车载任务启动流程
• 3.2 车载越行流程
• 3.3 列车冒进后防护流程
• 3.4 司机触发的SH流程
• 3.5 车载任务结束流程
• 3.6 车载工作流程图关系
• 第4章 基于时间自动机的UPPAAL工具
• 4.1 形式化方法
• 4.1.1 形式化方法概述
• 4.1.2 形式化方法分类
• 4.1.3 形式化方法验证
• 4.2 时间自动机
• 4.2.1 时间自动机概述
• 4.2.2 时间自动机特性分析
• 4.3 模型分析验证工具UPPAAL
• 4.3.1 UPPAAL结构
• 4.3.2 UPPAAL理论模型
• 第5章 基于时间自动机的车载设备系统建模
• 5.1 VC时间自动机模型
• 5.2 DMI时间自动机模型
• 5.3 RBC时间自动机模型
• 第6章 基于UPPAAL的车载设备系统分析验证
• 6.1 车载设备系统模型仿真分析
• 6.1.1 车载任务启动流程仿真时序图分析
• 6.1.2 车载越行流程仿真时序图分析
• 6.1.3 列车冒进后防护流程仿真时序图分析
• 6.1.4 司机触发的SH流程仿真时序图分析
• 6.1.5 车载任务结束流程仿真时序图分析
• 6.2 车载设备系统模型验证
• 6.2.1 可达性验证
• 6.2.2 时间特性验证
• 6.2.3 安全性验证
• 6.2.4 活性验证
• 结论
• 致谢
• 参考文献
• 攻读硕士学位期间发表的论文