基于Petri网的通信协议性能分析与验证方法及在ETCS中的应用  

Application of Petri Based Verification Approach in Safety Communication Protocol for ETCS

作　　者：程林芳[1] 王菲[1] 赵显琼[1] 

机构地区：[1]中国铁道科学研究院通信信号研究所,北京市100081

出　　处：《现代交通（中英文版）》2013年第4期58-63,共6页Modern Transportation

基　　金：基金资助：受铁道部科技研究开发计划项目支持资助（2012X001）.

摘　　要：列车运行控制系统中，安全通信协议的性能直接影响到列车的行车安全。因此，对其进行性能分析和验证技术是保证行车安全的重要技术之一。本文以欧洲列车运行控制系统（ETCS）安全通信协议为验证对象，提出基于Petri网的安全通信协议性能分析和验证方法，首先用有色Petri网给建立模型，然后用形式化方法验证协议的有界性，活性和安全性。根据模型表示的状态和行为检查协议是否符合规范的要求。以上功能都是通过Petri网软件实现，包括Poseidon和CPNTools。As the performance of secure communication protocol directly affects the safety state of train in train operation control system, the performance analysis and verification is an important means to guarantee the train safety, secure communication protocol of ETCS is the subject of this paper; then performance analysis and verification are put forward based on Petri; by which model is developed by means of CPN （Colored Petri Net）; then boundedness, liveness, and safety of the protocol are investigated using formal method; further, based on the model state and action, whether the protocol agrees with standard is examined. The above mentioned functions are realized by Petri including Poseidon and CPN Tools.

关 键 词：ETCS 安全通信协议 PETRI网 

分 类 号：U40[交通运输工程—道路与铁道工程]