关键词：安全通信协议；ETCS；EURORADIO；有色Petri网；形式化分析
摘 要：安全通信协议是保证基于通信的列车运行控制系统中通信安全的主要因素,其性质和最终实现正确的形式化验证具有重要意义.本文将欧洲列车运行控制系统安全通信协议规范中的一些未强制规定的要求明确化,选择分层赋时有色Petri网(CPN)对修改后的安全通信协议进行研究,综合安全层、信道与应用层模型提出无线通信系统模型的分层结构,通过改变信道与应用层模型的参数,分析修改的安全通信协议中安全连接建立的时间特性.分析结果表明:信道丢包率为0.1、0.05、0.01的情况下,修改的安全通信协议安全连接建立时间特性是符合规范要求的.