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

• 作者: 张雪松 李堃
• 来源期刊: 计算机工程
• 学科: 工学
• 关键词: 安全通信协议 时序逻辑 分层着色Petri网 ASK-CTL形式化验证 故障导向安全
• 年，卷（期）: 2018,（12）
• 所属期刊栏目: 移动互联与通信技术
• 页码范围: 120-128
• 页数: 9页
• 分类号: TP393
• 字数: 5164字
• 语种: 中文
• DOI: 10.19678/j.issn.1000-3428.0049260

摘要

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

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	张雪松	中国铁道科学研究院电子信息研究所	8	25	3.0	4.0
2	李堃	中国铁道科学研究院通信信号研究所	1	0	0.0	0.0