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

作     者：李堃 张雪松 LI Kun;ZHANG Xuesong

作者机构：中国铁道科学研究院通信信号研究所北京100081 中国铁道科学研究院电子信息研究所北京100081 

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

出 版 物：《计算机工程》 (Computer Engineering)

年 卷 期：2018年第44卷第12期

页      码：120-128页

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

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

学科分类：12[管理学] 1201[管理学-管理科学与工程类] 08[工学] 081201[081201] 0812[工学-测绘类] 

D　O　I：10.19678/j.issn.1000-3428.0049260

馆 藏 号：203416087...