安全关键系统通信协议调研报告（2015.4.12）1 调研题目安全关键系统通信协议的建模与分析2 任务说明1) 查阅国外的相关文献；2) 补充通信协议中的具体网络；3) 阅读标准EN50159；3 关键字检索词：CBTC；安全关键系统；安全通信协议；EN50159；safety communication protocol检索策略：无线*通信；总线*通信；以太网*通信；CBTC*communication protocol；safety*protocol；verification/ test/ model / simulation / design / analysis *(safety) communication protocol;4 检索范围中国知网百度httpweb of science(SCIE) /IEEESpringer LINKELSEVIER ScienceDirect(SDOL)在不同关键词组合下，检索范围内，近三年的文献总数5 主要的检索文献[1] BS EN50159 Railway applications—Communication, signaling and processing systems- Safety- related communication in transmission systems[S].[2] 安全通信与安全通信标准EN50159[J]. 铁路通信信号工程技术，2014.[3] Performance evaluation and verification of communication protocol for railway signaling systems [J]. Computer Standards & Interfaces, 2005.[4] Verification and conformance test generation of communication protocol for railway signaling systems [J]. Computer Standards & Interfaces, 2007.[5] Development of verification and conformance testing tools for a railway signaling communication protocol [J]. Computer Standards & Interfaces, 2009.[4] Group communication on highways: An evaluation study of geocast protocols and applications[J].Ad Hoc Networks, 2013.[6] Compositional verification of a communication protocol for a remotely operated aircraft[C]. Science of Computer Programming, 2013.[7] Verification of the safety communication protocol in train control system using colored Petri net[J].Reliability Engineering and System Safety, 2012.(国内-陈黎洁)[8]Simulation and verification of RSSP-II safety communication protocol[C].2012 Second International Conference on Business Computing and Global Information, 2012.(国内-许孟华) [9] Formal verification of safety protocol in train control system [J]. Technological Sciences, 2011 (国内-北交团队)[10] 无线传感器网络安全通信协议研究与设计[D].硕士，大连理工大学，2006.[11] 安全关键实时通信协议研究[D].博士，兰州大学，2011.[12] 基于ZigBee的无线传感器网络通信协议栈设计与实现[D].硕士，电子科技大学，2009.[13] 基于工业以太网的列车通信网络研究[D].硕士，北京交通大学，2011.6 检索结果摘要汇总根据以上检索范围与检索关键词，其中部分检索结果5篇，摘述如下：【篇名】安全通信与安全通信标准EN50159【作者】杨剑【期刊名称】铁路通信信号工程技术【年份】2014年2月，第11卷第1期【摘要】EN50159是欧洲铁路通信信号领域信息传输系统中安全通信标准。
对安全通信基本知识进行一般介绍，对最新版本EN50159:2010标准内容进行简单解读，并结合自身实践，对安全通信协议软件开发相关经验要点进行介绍。
【篇名】Development of verification and conformance testing tools for a railway signaling communication protocol【作者】Jae-Ho Lee, Jong-Gyu Hwang, Ducko Shin, Kang-Mi Lee, Sung-Un Kim【期刊名称】Computer Standards & Interfaces【年份】2009【摘要】Verification and conformance testing for protocol specification, the key part of the protocol development process, are complementary technologies employed to increase confidence that a system will function as stated in its specifications. In this paper, we verify the safety and liveness of the protocol specified for the Labeled Transition System (LTS) by usingmodel-checking method and implementing the testing tool, which experimentally demonstrates the presence of deadlock and reachability from the initial state to a random state. Implementing the testing tool can use modal mu-calculus to assess whether protocol model properties, presented by modal logic, meet protocol specifications. In addition, we propose a conformance testing toolto check correct implementation of sequences that have been derived by the UIO method from the specification of the protocol being verified. This generating tool uses the C++ language in the Microsoft Windows NT environment.【篇名】Compositional verification of a communication protocol for a remotely operated aircraft 【作者】Alwyn E. Goodloe, César A. Mu?oz【期刊类型】Science of Computer Programming【年份】2013【摘要】This paper presents the formal specification and verification of a communication protocol between a ground station and a remotely operated aircraft. The protocol can be seen as the vertical composition of protocol layers, where each layer performs input and output message processing, and the horizontal composition of different processes concurrently inhabiting the same layer, where each process should satisfy a distinct delivery requirement. A compositional technique is used to formally prove that the protocol satisfies these requirements. Although the protocol itselfis not novel, the methodology employed in its verification extends existing techniques by automating the tedious and usually cumbersome part of the proof, thereby making the iterative design process of protocols feasible.【篇名】基于工业以太网的列车通信网络研究【作者】张建斌【学位类型】硕士【授予单位】北京交通大学【导师】谭南林【年份】2011【摘要】:传统以太网通信的非实时和非确定性限制了其在列车通信网络中应用。