摘要：

无线调车机车信号和监控系统(STP)是基于无线数传电台,实现车载和地面设备之间双向信息传输的实时信号监控和安全防护系统。为保证系统中车-地之间交互信息的实时性、可靠性与完整性,依据欧标EN50159,在现有ETCS安全通信协议EuroRadio的基础上,通过增加安全连接超时重发、双序号时间戳和故障导向安全机制,设计一套适用于STP系统的安全通信协议,并利用分层着色Petri网和ASK-CTL时序逻辑验证语言对其进行建模和形式化验证。分析结果表明,该协议不仅满足功能安全性要求,同时还能保证系统在非理想信道环境下的故障导向安全。

关键词: 安全通信协议, 时序逻辑, 分层着色Petri网, ASK-CTL形式化验证, 故障导向安全

Abstract:

The STP system is based on data-transmission radio.By the data transmission between the mobile equipment and the ground equipment,it can realize the real-time monitoring of train signal,which is used to ensure the safety protection of the train.To make sure that the information,which transmits by wireless to be real-time,reliable and complete,this paper designs a safety communication protocol for STP.According to En50159,it adds some extra safety measures,such as time-out,sequence-number and so on in STP safe communication protocol,which is based on EuroRadio,to ensure the communication system to be fail-safe.And it uses hierarchical Colored Petri Net(CPN) and ASK-CTL formula to build hierarchy models and make formal verification of the proposed protocol.Analysis results show that the proposed protocol for STP has the functional safety,and it also can be fail-safe,even though the transmission happens during the undesired channel.

Key words: safety communication protocol, temporal logic, hierarchical Colored Petri Net(CPN), ASK-CTL formal verification, fail-safe

中图分类号: 

• TP393