无线通信具有传输速率高、双向传输等优点,列车运行控制系统逐渐由传统的基于轨道电路的列车控制向基于通信的列车控制方向发展。列车运行控制系统作为安全苛求系统,要求列车与地面能够安全的通信,而无线通信本身存在重复(repetition)、删除(deletion)、插入(insertion)、乱序(resequence)恶化(corruption)、延时(delay)、伪装((?)nasquerade)等典型的安全隐患,不能保证数据传输的安全性,不能满足列车运行控制系统安全通信的要求,安全通信协议由此产生。安全通信协议运行于列车运行控制系统这种安全苛求系统中,而本质上又是一种通信协议,因此,该协议的验证既包括安全功能的验证,也包括协议性能的验证,这给该协议的验证带来了挑战。论文针对列控系统安全通信协议的特性,在深入分析现有通信协议验证方法侧重点和局限性的基础上,将列控系统安全通信协议的验证内容归纳为功能和性能两个方面。论文提出将模型检验与仿真结合的方法验证安全通信协议,利用有色Petri网(Colored Petri Net, CPN)支持的模型检验功能验证安全通信协议的功能,利用CPN的仿真功能验证安全通信协议的性能。论文首先以欧洲列车运行控制系统(European Train Control System, ETCS)安全通信协议为背景,利用CPN的分层功能,建立安全通信协议模型。参考协议规范定义的安全通信协议的时序逻辑,利用CPN自带的基于计算树时序逻辑(Computational Tree Logic, CTL)的模型检验工具ASK-CTL验证协议逻辑功能的正确性,以及在理想条件下时间的正确性。验证结果符合预期效果,可以初步说明验证方法的合理性。论文进一步参考列车运行控制系统在实现过程中一些具体的技术指标,利用CPN的仿真功能仿真了随机条件下安全通信协议的时间特性,并且应用数理统计的知识对仿真结果进行评估,说明随机因素是如何影响安全通信协议的性能。与国内外相关研究相比,论文的主要创新点如下：(1)针对Petri网给复杂系统建模困难的问题,提出了分层建模方法,运用有色Petri网的分层能力首先建立安全通信协议的逻辑模型,然后在逻辑模型基础上增加时间描述模块形成时间模型,最后在时间模型上增加随机事件描述模块体现随机因素；(2)针对既有通信协议验证方法的功能验证能力局限,即只能仿真协议的性能指标,不能验证协议的功能特性,提出用模型检验的方法验证安全通信协议的功能,针对既有基于Petri网的模型检验方法在描述事件发生次序方面困难的缺陷,利用有色Petri网自带模型检验工具ASK-CTL这一特点,提出用有色Petri网完成对安全通信协议的模型检验,得到基于ASK-CTL的协议的逻辑特性验证方法,提高了模型检验能力；(3)针对模型检验无法表示系统具体性能指标的问题,提出基于有色Petri网的仿真方法得出安全通信协议的性能指标,用数理统计的方法对仿真结果进行定量的评估分析；(4)针对目前安全苛求系统的验证方法没有考虑性能指标的问题,提出基于有色Petri网的模型检验与仿真结合的方法,针对安全通信协议功能与性能两方面的需求完成对协议的综合验证。论文最后以北京交通大学自主研发的基于通信的列车运行控制系统(Communication Based Train Control System, CBTC)安全通信协议为例,采用ASK-CTL完成其功能的验证,通过验证协议的状态转换路径的唯一性、执行行为的偏序关系和可靠特性,对如何保证协议的确定性提出了建议；采用CPN和数理统计对协议的稳定性、失效率及其影响因素进行了分析,通过这样的分析结果直接为协议的设计提供依据,同时证明了论文提出方法的有效性。