列控-安全信息传输系统可靠性及安全性的形式化分析

作者：高莺; 张琦; 陈黎洁; 刘宏杰

来源：北京交通大学学报, 2018, 42(02): 61-68.

• 列控-安全信息传输系统
• Petri网
• 可靠性
• 安全性
• 模型检验

基于通信的列控(CBTC)系统使用基于IEEE 802.11系列的无线局域网实现车-地双向信息传输,但是无线局域网无法满足安全苛求列控系统在信息传输可靠性和安全性方面的需求.为了解决该问题,可以采用双网冗余的结构提高无线局域网信息传输的可靠性,再在无线局域网之上增加安全通信协议来保证信息传输的安全性.本文提出在双网冗余无线局域网基础之上增加安全通信协议形成列控-安全信息传输系统(China-Radio),使用随机Petri网建立了双网冗余结构的无线局域网的可靠性模型,并与单网结构进行了定量对比和形式化分析,验证了双网冗余结构可靠性的提升;使用有色Petri网对China-Radio系统建模,并采用模型检验的方法证明China-Radio系统的功能安全性,能够满足列控系统的需求.

• 单位
  轨道交通控制与安全国家重点实验室; 中国铁道科学研究院; 中国铁道科学研究院通信信号研究所; 北京交通大学