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

作者：李堃; 张雪松

来源：计算机工程, 2018, 44(12): 120-128.

DOI：10.19678/j.issn.1000-3428.0049260

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

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

• 单位
  中国铁道科学研究院通信信号研究所