%0 Journal Article
%T 列控-安全信息传输系统可靠性及安全性的形式化分析<br>Formal analysis for reliability and safety of China-Radio in train control system
%A 高莺
%A 张琦
%A 陈黎洁
%A 刘宏杰
%J 北京交通大学学报
%D 2018
%R 10.11860/j.issn.1673-0291.2018.02.009
%X 摘要 基于通信的列控（CBTC）系统使用基于IEEE 802.11系列的无线局域网实现车-地双向信息传输，但是无线局域网无法满足安全苛求列控系统在信息传输可靠性和安全性方面的需求.为了解决该问题，可以采用双网冗余的结构提高无线局域网信息传输的可靠性，再在无线局域网之上增加安全通信协议来保证信息传输的安全性.本文提出在双网冗余无线局域网基础之上增加安全通信协议形成列控-安全信息传输系统（China-Radio），使用随机Petri网建立了双网冗余结构的无线局域网的可靠性模型，并与单网结构进行了定量对比和形式化分析，验证了双网冗余结构可靠性的提升；使用有色Petri网对China-Radio系统建模，并采用模型检验的方法证明China-Radio系统的功能安全性，能够满足列控系统的需求.<br>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.
%K 列控-安全信息传输系统
%K Petri网
%K 可靠性
%K 安全性
%K 模型检验&lt
%K br&gt
%K China-radio
%K Petri net
%K reliability
%K safety
%K model checking
%U http://jdxb.bjtu.edu.cn/CN/abstract/abstract3418.shtml