在CBTC(Communications-based Train Control,基于通信的列车控制)系统中,ATS(Automatic Train Supervision,自动列车监控)子系统实时监控列车运行线路及列车运行状况,为调度人员提供实际运行线路上的大量现场信息。ATS系统设备间的数据交互都是通过通信协议来完成,通信协议将系统内的设备联系起来形成一个有机的整体,从而使系统中各子单元共同协作完成特定的功能,通信协议质量的好坏直接关系到系统功能的完成和系统性能的优劣。传统的通信协议验证大多是通过大量的实践来检验协议设计的正确性,这样的验证方法无法从理论的角度来证明通信协议设计的正确性,同时也很难发现一些隐藏很深的设计漏洞。所以应用形式化的验证方法对协议的设计模型进行验证是非常有意义的。本文对实验室自主研发的ATS系统的内部通信协议进行了设计和形式化的验证工作,并给出了验证结果分析。首先,介绍了形式化的验证方法,形式化验证方法的意义在于它能够证明待验证系统模型设计的正确性,它会遍历系统内所有的状态迁移路径来验证模式是否满足指定的性质。接下来阐述了符号模型检验方法的原理及其支持工具SMV,具体说明了SMV的基本工作原理和语法,同时指出了在使用SMV的过程中发现的一些问题。其次,依据需求对内部通信协议进行了设计。先简要介绍了设计工具RationalRose,接着阐述了ATS系统内部通信协议的需求以及相应的设计策略,简单来说内部通信协议的需求即通信协议要满足ATS系统对数据传输的需求,接着针对需求进行了内部通信协议的架构设计和模块划分工作,最后以UML类图、序列图和活动图的方式对内部通信协议的功能进行了概要设计,为形式化验证工作提供了建模基础。最后,使用形式化的方法对内部通信协议关键模块进行了验证,通过抽象内部通信协议的有限状态迁移图,用SMV语言对待验证的模型进行描述,用CTL公式对待验证的性质进行表达。其中对于临界区的操作模型进行了改进,使得验证最终得以通过,对于数据冗余、处理关键数据报文处理的形式化验证均一次通过。通过形式化验证证明了通信协议关键模型设计的正确性,进而保证了内部通信协议的开发质量。