STP安全通信协议设计与形式化验证  

Design and Formal Verification of Safety Communication Protocol in STP

作　　者：李堃 张雪松[2] LI Kun;ZHANG Xuesong(Institute of Communication Signals,China Academy of Railway Sciences,Beijing 100081,China;Institute of Electronic Information,China Academy of Railway Sciences,Beijing 100081,China)

机构地区：[1]中国铁道科学研究院通信信号研究所,北京100081 [2]中国铁道科学研究院电子信息研究所,北京100081

出　　处：《计算机工程》2018年第12期120-128,共9页Computer Engineering

基　　金：中国铁道科学研究院重点课题项目“基于新一代无线移动通信的调车机车控制技术研究”(2016YJ054);中国铁路总公司科研重点课题项目“通信信号设备提升关键技术研究-STP互联互通技术要求研究”(2017X012-B)。

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

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

分 类 号：TP393[自动化与计算机技术—计算机应用技术]