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

来源：计算机工程杂志2018年第12期北京时间：

作者：李堃,张雪松

单位：1.中国铁道科学研究院通信信号研究所,北京 100081; 2.中国铁道科学研究院电子信息研究所,北京 100081

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

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

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