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

作     者：高莺 张琦 陈黎洁 刘宏杰 GAO Ying[1a;1c];ZHANG Qi＇h[1c];CHEN Lijie[1d];LIU Hongjie[2;2b;1 c]

作者机构：中国铁道科学研究院研究生部北京100081 中国铁道科学研究院通信信号研究所北京100081 中国铁道科学研究院国家铁路智能运输系统工程技术研究中心100081 中国铁道科学研究院标准计量研究所100081 北京交通大学轨道交通控制与安全国家重点实验室北京100044 北京交通大学轨道交通运行控制系统国家工程研究中心北京100044 

基　　金：国家自然科学基金(U1434209) 中国铁路总公司科技研究开发计划课题(2015D002-B) 中央高校基本科研业务费专项资金(016JBM007) 中国铁道科学研究院科研项目(1551ZJ0804) 交控科技设计创新学科发展基金(9907006510) 

出 版 物：《北京交通大学学报》 (JOURNAL OF BEIJING JIAOTONG UNIVERSITY)

年 卷 期：2018年第42卷第2期

页      码：61-68页

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

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

学科分类：0810[工学-土木类] 08[工学] 0805[工学-能源动力学] 081001[081001] 082302[082302] 0812[工学-测绘类] 0823[工学-农业工程类] 

D　O　I：10.11860/j.issn.1673-0291.2018.02.009

馆 藏 号：203288932...