列车运行控制系统中安全通信协议的形式化分析

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

Formal Analysis on Safety Communication Protocol in Train Control System

The safety communication protocol is a main factor affecting the communication safety of the train control system.Its properties and final implementation of formal verification are of great significance to the train control system.After explicitely specifying the requirements which have not been defined as mandatory terms in the EURORADIO specification,the hierarchy model of the wireless communication system with the hierarchy timed Colored Petri Net(CPN) is proposed,combining the models of safety layer,channel,and application layer.The time property of safety connection in the advanced safety communication protocol is analyzed according to the parameters of the channels and application models.Analysis results show that in the case of the probability of data loss in a channel being 0.1,0.05,and 0.01,the time characteristic for safety connection of the advanced safety communication protocol can fulfill the requiremerrts of the requirements of the specification.