| 列控-安全信息传输系统可靠性及安全性的形式化分析 |
| |
| 引用本文： | 高莺,张琦,陈黎洁,刘宏杰.列控-安全信息传输系统可靠性及安全性的形式化分析[J].北京交通大学学报(自然科学版),2018,42(2):61-68. |
| |
| 作者姓名： | 高莺 张琦 陈黎洁 刘宏杰 |
| |
| 作者单位： | 中国铁道科学研究院研究生部,北京100081;中国铁道科学研究院国家铁路智能运输系统工程技术研究中心,北京100081;中国铁道科学研究院通信信号研究所,北京100081;中国铁道科学研究院国家铁路智能运输系统工程技术研究中心,北京100081;中国铁道科学研究院标准计量研究所,北京,100081;北京交通大学轨道交通控制与安全国家重点实验室,北京100044;北京交通大学轨道交通运行控制系统国家工程研究中心,北京100044 |
| |
| 基金项目： | 国家自然科学基金(U1434209)，中国铁路总公司科技研究开发计划课题(2015D002-B)，中央高校基本科研业务费专项资金(2016JBM007)，中国铁道科学研究院科研项目(1551ZJ0804)，交控科技设计创新学科发展基金(9907006510)National Natural Science of China(U1434209)，Science and Technology Research and Development Program of China Railway Corporation(2015D002-B)，Fundamental Research Funds for the Central Universities(2016JBM007)，Science and Research Program of China Academy of Railway Sciences(1551ZJ0804)，TCT Funding Program(9907006510) |
| |
| 摘 要： | 基于通信的列控(CBTC)系统使用基于IEEE 802.11系列的无线局域网实现车-地双向信息传输,但是无线局域网无法满足安全苛求列控系统在信息传输可靠性和安全性方面的需求.为了解决该问题,可以采用双网冗余的结构提高无线局域网信息传输的可靠性,再在无线局域网之上增加安全通信协议来保证信息传输的安全性.本文提出在双网冗余无线局域网基础之上增加安全通信协议形成列控-安全信息传输系统(China-Radio),使用随机Petri网建立了双网冗余结构的无线局域网的可靠性模型,并与单网结构进行了定量对比和形式化分析,验证了双网冗余结构可靠性的提升;使用有色Petri网对China-Radio系统建模,并采用模型检验的方法证明China-Radio系统的功能安全性,能够满足列控系统的需求.
|
| 关 键 词： | 列控-安全信息传输系统 Petri网 可靠性 安全性 模型检验 |
Formal analysis for reliability and safety of China-Radio in train control system |
| |
| GAO Ying,ZHANG Qi,CHEN Lijie,LIU Hongjie.Formal analysis for reliability and safety of China-Radio in train control system[J].JOURNAL OF BEIJING JIAOTONG UNIVERSITY,2018,42(2):61-68. |
| |
| Authors: | GAO Ying ZHANG Qi CHEN Lijie LIU Hongjie |
| |
| Abstract: | IEEE 802.11 based WLAN (Wireless Local Area Network) technology is the basis for bi-directional communication between on-board and wayside equipment in CBTC system,but it could not satisfy the reliability and safety requirements in safety-critical train control system.In order to solve this problem,dual redundant network is a common way to increase communication system reliability,and safety communication protocol is often used to improve the safety performance.A specific communication system is proposed for the reliable and safe data exchange in train control system,which is called China-Radio,where a safety protocol is applied based on a dual redundant WLAN.To evaluate the performance improvement,firstly we built the reliability model of the dual redundant WLAN using the stochastic Petri net,calculate formally and mathematically,and compare with the single network model,which proves a great improvement of the reliability performance.Then the China-Radio by colored Petri net is modelled,and the functional safety of the system by model checking method is formally validated,which shows that China-Radio satisfies the safety requirement of the CBTC system. |
| |
| Keywords: | |
| 本文献已被 CNKI 万方数据 等数据库收录！ |
|
