作者投稿和查稿 主编审稿 专家审稿 编委审稿 远程编辑

计算机工程 ›› 2018, Vol. 44 ›› Issue (12): 120-128. doi: 10.19678/j.issn.1000-3428.0049260

• 移动互联与通信技术 • 上一篇    下一篇

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

李堃1,张雪松2   

  1. 1.中国铁道科学研究院通信信号研究所,北京 100081; 2.中国铁道科学研究院电子信息研究所,北京 100081
  • 收稿日期:2017-11-10 出版日期:2018-12-15 发布日期:2018-12-15
  • 作者简介:李堃(1993—),女,硕士研究生,主研方向为交通信息工程及控制、通信工程;张雪松,研究员
  • 基金资助:

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

Design and Formal Verification of Safety Communication Protocol in STP

LI Kun 1,ZHANG Xuesong 2   

  1. 1.Institute of Communication Signals,China Academy of Railway Sciences,Beijing 100081,China; 2.Institute of Electronic Information,China Academy of Railway Sciences,Beijing 100081,China
  • Received:2017-11-10 Online:2018-12-15 Published:2018-12-15

摘要:

无线调车机车信号和监控系统(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

中图分类号: