摘要：近年来随着高速铁路的发展，时速在300km/h以上的的高速铁路都已经用CTCS-3级列车运行控制系统。为了提高CTCS-3级列控系统的安全性、可靠性和效率性，验证CTCS-3级列控系统的信息传递流程的安全性和受限性变得十分重要，于是形式化建模在CTCS-3列控系统中的应用的课题被提了出来。因此，论文介绍了基于时间自动机模型验证工具UPPAAL对CTCS-3级列控系统的信息传递进行仿真分析，该系统包含列车注册模块、列车运行控制器模块、列车撤销模块、车载控制器EVC模块、地面设备模块。通过这几个模块之间的仿真，可以模拟出列车运行过程中车-地之间信息传递的流程，明确各个系统所负责的的工作和跳转的约束，最终验证了列车运行控制系统的列车信息登陆、建立会晤、列车信息撤销位置报告、行车许可等过程。 21794
毕业论文关键词： 时间自动机；形式化建模；CTCS-3列控系统
Formal Modeling of Application in CTCS-3 Train Control System
Abstract: Recently with the rapid development of High-speed railway, speed more than 300 km/h in the high-speed railway has been used in CTCS-3 train operation control system. In order to improve the safety, reliability and efficiency of the CTCS-3 train control system, it is important to test CTCS-3 train control system in the security of information transmission process. A CTCS-3 train operation control system monitoring model is designed in this paper based on UPPAAL time automata. According to the communication process between the train and the RBCs, the model is pided into various modules, including the process of train normal control module, train login module, the train control module, vehicle controller module and RBC controller module. It can simulate the process of train running, understand the train running information. The simulation result showed that this model can verify the correct process of message login, the train position reporting and driving licensing.
Key Words: Timed Automata; forms modeling; CTCS-3 Train Control System
目录
1 绪论 1
1.1 国内外研究现状 1
1.2 本论文研究意义 2
1.3 本论文的结构 2
1.4 作者在课题研究中所做的工作 3
2 形式化方法 4
2.1 形式化方法的简单介绍 4
2.1.1 形式化方法及其应用 4
2.1.2 形式化方法的特点介绍 5
2.2 时间自动机 5
2.2.1 时间自动机的历史和基本功能的介绍 5
2.2.2 验证工具UPPAAL 6
2.2.3 验证工具UPPAAL扩展语言介绍 8
3 列车运行控制系统 11
3.1 国内外列车运行控制系统的介绍 11
3.2 CTCS-3级列控系统组成 11
3.3 列控系统信息传递的方式 12
3.3.1 点式设备 12
3.3.2 轨道电路 14
3.3.3 无线传输 14
3.4 高速铁路信号与控制系统的特点 15
4 列控系统建模分析 16
4.1 列车注册模块 16
4.2 列车正常运行模块设计 17
4.3 RBC切换模块 20 形式化建模在CTCS-3列控系统中的应用:http://www.youerw.com/tongxin/lunwen_14160.html