第五章分别对列车注册模块、列车正常运行模块、RBC切换模块、和列车撤销模块进行分析和验证。
第751章对本文进行总结，展望未来的工作。
1.4    作者在课题研究中所做的工作
(1) 确定系统设计方案，查阅先关论文期刊，仔细研究本论文的实施方法，熟悉UPPALL软件编写，写开题报告。
(2) 完成CTCS-3列控系统的车地交互系统（地面系统和车载系统）的网络模型搭建。
(3) 对CTCS-3列控系统的车地交互系统形式化建模的结果进行分析，完成毕业设计论文，整理毕业设计文件和实验记录。
(4) 送评阅教师审查及修改，制作答辩用的PPT，参加毕业设计答辩。
2    形式化方法
2.1    形式化方法的简单介绍
想要很好的掌握形式化方发首先必须具备很好的数学功底如：数学分析（或者高等数学），离散数学。形式化方发主要具有抽象和形式化相结合的特点、 需要具备理论证明和构造性分析、基本模型的建立与性质掌握。通过形式化的语义符号描述和工具表述设计所需要的计算机系统，最终得以严格规范的验证系统的性质和正确性。用户的各种需求、系统需要的功能以及各种性质形式化描述都能够被详细地描述出来，它能够确切地描述其具体工作过程。在严格的数学的基础上，形式化方法具有严格的语法和语义定义，从而可以准确地描述系统模型。
形式化方法在应用有两种形式：一种为形式化规范，另一种为形式化验证。第一种情况中，形式化方法用于生成范例，然后将规范作为传统系统开发的根本。形式化规范的优势在于确切、抽象、简明和可操纵。操作可以包含范例的一致性检查、原型的主动生成或经由证明的方法推导出范例的一些特殊性质。在第二种情况，形式规范形成后作为验证程序正确性的依据。除具有与第一种情况类似的益处，还可以利用形式化方法证明规范及其相应程序的正确性，以表明程序与其规范的一致性，这样，可以使软件开发有可能具有与数学证明同样的确定性[6]。
形式化方法的理论基础分别是由集合论、逻辑理论、代数理论、软件结构理论构成的。在集合论中涉及到的集合运算、关系、映射对于状态变换是非常适用的。在逻辑理论中，一阶谓词演算是一个形式逻辑系统，具有一整套证明技术，采用一阶谓词演算方法进行规范说明是非常合适的。将一阶谓词演算和程序联系起来，主要需要解决两方面互相转换的问题，即谓词演算转换成程序和程序转换成谓词的问题。将谓词演算转换成程序的问题也就是程序的自动生成问题，也称为软件的自动生成问题。而将程序转换成谓词的问题属于程序验证的问题。逻辑理论提供了一些方法用于规范的推理和程序的执行。而代数理论包括代数规范、范畴论、进程代数、共代数等理论的发展也大大地推进了形式化方法的发展。上述的结构理论提供了一个计算模型，该计算模型描述了所开发的软件系统的结构及其组成部分、状态机和过程的形式上的对应模型。形式化方法与这些技术相结合，形成了应用于不同领域的不同的形式化方法[7]。
2.1.1    形式化方法及其应用
在我国科学技术高速发展的今天，并发软件系统在各个领域都能够发现它如：国防、航天、铁路等关键领域，对于这些关系国民经济、关乎人命财产安全的领域，怎样设计出一套高性能的并发软件十分重要，并且验证其正确性和可靠性和安全性也至关重要。想要通过实物模型来发现问题和缺陷这样的途径是不仅耗时间和费人力难度很大、效率很低，并且这其中还会存在错误，因此我们想到通过对某种办法来解决此问题，那就是形式化分析方法，它能够有效的减少设计上的错误、检查其中的缺陷，加强系统的抗外界病毒侵入的能力，下面介绍几个在形式化方法的典型应用。 形式化建模在CTCS-3列控系统中的应用(3):http://www.751com.cn/tongxin/lunwen_14160.html