4.4    列车撤销模块建模    21
4.5    车载EVC模块    22
4.6    室外设备模块    24
5    系统流程分析验证    26
5.1    列车注册系统流程分析验证模块验证    26
5.2    列车正常运行模型验证    27
5.3    RBC切换模块验证    27
5.4    列车撤销模块验证    29
6    结论与展望    30
致谢    31
参考文献    32
1    绪论
铁路信号技术已成为提高铁路运输经济效益、改善劳动条件的一种手段和发展趋势。随着铁路的不断提速，对铁路信号的要求越来越高，从原先的对地面设备控制改为向列车的直接控制，并且从原来的开环向闭环控制转变，因此铁路部门提出来适合我国国情的CTCS(Chinese Train Control System，中国列车运行控制系统)。近几年的客运专线大量采用CTCS-2和CTCS-3级的列控系统。我国铁路要积极发展新一代安全性能好、运行效率高的列车运行控系统。使得在较高起点上, 在较短时间内, 以高速铁路、客运专线的建设等为重点, 建立和发展我国的铁路信号安全综合控制监测系统和运营管理系统。列车运行控制系统面临前所未有的发展机会, 运用形式化建模来提高列控系统的安全性能以适应建设信息化、智能化、高科技现代化铁路的需要。
1.1    国内外研究现状
1.2    本论文研究意义
在整个铁路的发展过程中，国内和国外的开发人员都采用不同的建模语言对系统进行形式化得建模。其中最为常见的是Petri网和以UML为代表的面向对象建模方法。但由于UML语法结构虽然采用了形式化的规约，但其语义缺乏严格的数学定义。只能进行静态的模型建立，不能进行动态的模型仿真。难以直接用数学工具对所建模型进行严密有效分析和验证，因此难予进行有效的模型修改和改进。
然而运用有色Petri网建模时，用户需要具备良好的数学基础。并且会随着被描述系统的深入，系统规模增大，建模难度也会增大。难以实现细节与需求的分开。它的建模方法只是用来描述和分析系统，不是计算机的实现工具，必须要通过一定的方法才能将有色Petri网用代码来实现[5]。
基于这两种常见的建模方法的缺点，我们选择了一种具有丰富、易懂的UPPAAL。它的界面灵活、清晰，能够提高安全性、稳定性的需要，并且使得系统的研发人员更加有效的发现系统设计的缺陷，系统操作人员更快更好地掌握列车运行控制系统的信息交互基本流程，最终提高到铁路部门所迫切要求的操作性能、经济实用性能、功能完备的性能。同时信号专业的学生在学习铁路信号理论时，也可以在实验过程中对该CTCS-3级列车运行控制系统进行软件平台上的实践操作，提高学习效果。
1.3    本论文的结构
本文有如下结构：
第一章前言，介绍国内外列控系统发展现状和本文的主要研究内容和意义。
第二章介绍形式化语言的基本内容、规范校验、特点和应用，并且提及时间自动机的基本概念，时间自动机的扩展语言和验证工具。
第三章介绍了国内外列车运行控制系统，CTCS-3级列控系统组成，并且介绍了列控系统信息传递的方式和高速铁路信号与控制系统的特点。
第四章介绍CTCS-3级列控系统及其各个子系统的功能，介绍各个子系统之间如何进行信息传递，具体分析各个系统功能需求。为系统各个流程的建模做好准备。同时设计各个子系统的状态、初始状态、触发事件、状态转移，并对这些子系统进行建模。 形式化建模在CTCS-3列控系统中的应用(2):http://www.youerw.com/tongxin/lunwen_14160.html