形式化建模在CTCS-3列控系统中的应用
毕业论文关键词： 时间自动机；形式化建模；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
上一篇：MATLAB红外图像去噪算法研究
下一篇：动车组转向架轴承故障诊断+源程序