列车运行控制系统安全通信协议验证方法的研究
|
摘要
无线通信具有传输速率高、双向传输等优点,列车运行控制系统逐渐由传统的基于轨道电路的列车控制向基于通信的列车控制方向发展。列车运行控制系统作为安全苛求系统,要求列车与地面能够安全的通信,而无线通信本身存在重复(repetition)、删除(deletion)、插入(insertion)、乱序(resequence)恶化(corruption)、延时(delay)、伪装((?)nasquerade)等典型的安全隐患,不能保证数据传输的安全性,不能满足列车运行控制系统安全通信的要求,安全通信协议由此产生。安全通信协议运行于列车运行控制系统这种安全苛求系统中,而本质上又是一种通信协议,因此,该协议的验证既包括安全功能的验证,也包括协议性能的验证,这给该协议的验证带来了挑战。
论文针对列控系统安全通信协议的特性,在深入分析现有通信协议验证方法侧重点和局限性的基础上,将列控系统安全通信协议的验证内容归纳为功能和性能两个方面。论文提出将模型检验与仿真结合的方法验证安全通信协议,利用有色Petri网(Colored Petri Net, CPN)支持的模型检验功能验证安全通信协议的功能,利用CPN的仿真功能验证安全通信协议的性能。论文首先以欧洲列车运行控制系统(European Train Control System, ETCS)安全通信协议为背景,利用CPN的分层功能,建立安全通信协议模型。参考协议规范定义的安全通信协议的时序逻辑,利用CPN自带的基于计算树时序逻辑(Computational Tree Logic, CTL)的模型检验工具ASK-CTL验证协议逻辑功能的正确性,以及在理想条件下时间的正确性。验证结果符合预期效果,可以初步说明验证方法的合理性。论文进一步参考列车运行控制系统在实现过程中一些具体的技术指标,利用CPN的仿真功能仿真了随机条件下安全通信协议的时间特性,并且应用数理统计的知识对仿真结果进行评估,说明随机因素是如何影响安全通信协议的性能。
与国内外相关研究相比,论文的主要创新点如下：
(1)针对Petri网给复杂系统建模困难的问题,提出了分层建模方法,运用有色Petri网的分层能力首先建立安全通信协议的逻辑模型,然后在逻辑模型基础上增加时间描述模块形成时间模型,最后在时间模型上增加随机事件描述模块体现随机因素；
(2)针对既有通信协议验证方法的功能验证能力局限,即只能仿真协议的性能指标,不能验证协议的功能特性,提出用模型检验的方法验证安全通信协议的功能,针对既有基于Petri网的模型检验方法在描述事件发生次序方面困难的缺陷,利用有色Petri网自带模型检验工具ASK-CTL这一特点,提出用有色Petri网完成对安全通信协议的模型检验,得到基于ASK-CTL的协议的逻辑特性验证方法,提高了模型检验能力；
(3)针对模型检验无法表示系统具体性能指标的问题,提出基于有色Petri网的仿真方法得出安全通信协议的性能指标,用数理统计的方法对仿真结果进行定量的评估分析；
(4)针对目前安全苛求系统的验证方法没有考虑性能指标的问题,提出基于有色Petri网的模型检验与仿真结合的方法,针对安全通信协议功能与性能两方面的需求完成对协议的综合验证。
论文最后以北京交通大学自主研发的基于通信的列车运行控制系统(Communication Based Train Control System, CBTC)安全通信协议为例,采用ASK-CTL完成其功能的验证,通过验证协议的状态转换路径的唯一性、执行行为的偏序关系和可靠特性,对如何保证协议的确定性提出了建议；采用CPN和数理统计对协议的稳定性、失效率及其影响因素进行了分析,通过这样的分析结果直接为协议的设计提供依据,同时证明了论文提出方法的有效性。
As wireless communication has the advantages of high transmission speed, bidirectional transmission and so on, the train control systems have been gradually developing from track based train control to communication based train control. The train and trackside must communicate with each other safely, as the train control system is a safety-critical system. However, there are a series of threats in the wireless communication system, such as repetition, deletion, insertion, resequence, corruption, delay, and masquerade, which could not guarantee the safety of data transmission, meeting the requirements of safety communication in train control system. Safety communication protocol is induced in this situation. Safety communication protocol runs in a safety-criticial environment, and in essence it is one communication protocol. Therefore, the verification of this protocol includes not only safety function, but also protocol performance, which brings about challenges to verification of this protocol.
Based on the characteristics of safety communication protocol in train control system and the in-depth analysis of the focus and limitation of the existing verifying approaches for communication protocol, this paper has determined that the content of verification for safety communication protocol includes function and performance. This paper integrates model checking and simulation to verify safety communication protocol, making used of model checking and simulation supported by Colored Petri Net (CPN). On the basis of the hierarchy architecture of communication system in the European Train Control System (ETCS) specified in the ETCS protocol specification, the thesis establish the models of safety communication protocol, viz. safety layer, application layer, and channel respectively, making use of the hierarchical function of Colored Petri Nets (CPN). Referenced from the temporal logic of safety communication protocol defined in the protocol specification, the correctness for the logic, as well as the time under ideal condition of the protocol are verified with ASK-CTL, which is a model checking tool based on Computational Tree Logic (CTL) supported by CPN. The results of verification could meet the expected results, preliminary showing that the verification method is reasonable. Furthermore, on the basis of some specific technical indicators in the train control system during the implementation, the timed characteristics of the protocol in a stochastical environment are simulated with CPN, and the results of simulation are assessed with mathematical statistics, to reflect how the random factors to affect the performance of the protocol.
The main innovation of the thesis is as follow, compared to the related research domestic and abroad:
(1) Focus on the limitation of Petri net for modeling of complex systems, the thesis proposes the method of modeling hierarchically. Making use of the capability of hierarchical modeling of Colored Petri Net, the logic model of safety communication protocol is established first, then the timed model is established with module of description for time based on the logic model, and finally, module of description for random events is added to reflect the random factors;
(2) Against traditional verification methods for communication protocol cannot verify the function, the thesis proposes model checking to verify the function of safety communication protocol. Focuses on the limitation of Petri net for description of sequence of events, the thesis proposes to apply ASK-CTL, supported by Colored Petri Net, to implement model checking for logic of safety communication protocol;
(3) Against model checking cannot represent specific performance, the thesis proposes simulation to obtain the performance of safety communication protocol by Colored Petri Net, and assess the simulation results through mathematical statistics;
(4) Against method of verification for safety-critical system does not consider performance, the thesis proposes combination of model checking and simulation with Colored Petri Net, to implement the verification of safety communication protocol for both function and performance.
The thesis ends with an accomplishment of the verification for the safety communication protocol in the Communication Based Train Control system (CBTC). Model checking with ASK-CTL and simulation with Colored Petri Net are used to verify the function and performance of the protocol, which could not only prove the rationality of the verification method in the thesis, but also guide the development of the protocol.
论文针对列控系统安全通信协议的特性,在深入分析现有通信协议验证方法侧重点和局限性的基础上,将列控系统安全通信协议的验证内容归纳为功能和性能两个方面。论文提出将模型检验与仿真结合的方法验证安全通信协议,利用有色Petri网(Colored Petri Net, CPN)支持的模型检验功能验证安全通信协议的功能,利用CPN的仿真功能验证安全通信协议的性能。论文首先以欧洲列车运行控制系统(European Train Control System, ETCS)安全通信协议为背景,利用CPN的分层功能,建立安全通信协议模型。参考协议规范定义的安全通信协议的时序逻辑,利用CPN自带的基于计算树时序逻辑(Computational Tree Logic, CTL)的模型检验工具ASK-CTL验证协议逻辑功能的正确性,以及在理想条件下时间的正确性。验证结果符合预期效果,可以初步说明验证方法的合理性。论文进一步参考列车运行控制系统在实现过程中一些具体的技术指标,利用CPN的仿真功能仿真了随机条件下安全通信协议的时间特性,并且应用数理统计的知识对仿真结果进行评估,说明随机因素是如何影响安全通信协议的性能。
与国内外相关研究相比,论文的主要创新点如下：
(1)针对Petri网给复杂系统建模困难的问题,提出了分层建模方法,运用有色Petri网的分层能力首先建立安全通信协议的逻辑模型,然后在逻辑模型基础上增加时间描述模块形成时间模型,最后在时间模型上增加随机事件描述模块体现随机因素；
(2)针对既有通信协议验证方法的功能验证能力局限,即只能仿真协议的性能指标,不能验证协议的功能特性,提出用模型检验的方法验证安全通信协议的功能,针对既有基于Petri网的模型检验方法在描述事件发生次序方面困难的缺陷,利用有色Petri网自带模型检验工具ASK-CTL这一特点,提出用有色Petri网完成对安全通信协议的模型检验,得到基于ASK-CTL的协议的逻辑特性验证方法,提高了模型检验能力；
(3)针对模型检验无法表示系统具体性能指标的问题,提出基于有色Petri网的仿真方法得出安全通信协议的性能指标,用数理统计的方法对仿真结果进行定量的评估分析；
(4)针对目前安全苛求系统的验证方法没有考虑性能指标的问题,提出基于有色Petri网的模型检验与仿真结合的方法,针对安全通信协议功能与性能两方面的需求完成对协议的综合验证。
论文最后以北京交通大学自主研发的基于通信的列车运行控制系统(Communication Based Train Control System, CBTC)安全通信协议为例,采用ASK-CTL完成其功能的验证,通过验证协议的状态转换路径的唯一性、执行行为的偏序关系和可靠特性,对如何保证协议的确定性提出了建议；采用CPN和数理统计对协议的稳定性、失效率及其影响因素进行了分析,通过这样的分析结果直接为协议的设计提供依据,同时证明了论文提出方法的有效性。
As wireless communication has the advantages of high transmission speed, bidirectional transmission and so on, the train control systems have been gradually developing from track based train control to communication based train control. The train and trackside must communicate with each other safely, as the train control system is a safety-critical system. However, there are a series of threats in the wireless communication system, such as repetition, deletion, insertion, resequence, corruption, delay, and masquerade, which could not guarantee the safety of data transmission, meeting the requirements of safety communication in train control system. Safety communication protocol is induced in this situation. Safety communication protocol runs in a safety-criticial environment, and in essence it is one communication protocol. Therefore, the verification of this protocol includes not only safety function, but also protocol performance, which brings about challenges to verification of this protocol.
Based on the characteristics of safety communication protocol in train control system and the in-depth analysis of the focus and limitation of the existing verifying approaches for communication protocol, this paper has determined that the content of verification for safety communication protocol includes function and performance. This paper integrates model checking and simulation to verify safety communication protocol, making used of model checking and simulation supported by Colored Petri Net (CPN). On the basis of the hierarchy architecture of communication system in the European Train Control System (ETCS) specified in the ETCS protocol specification, the thesis establish the models of safety communication protocol, viz. safety layer, application layer, and channel respectively, making use of the hierarchical function of Colored Petri Nets (CPN). Referenced from the temporal logic of safety communication protocol defined in the protocol specification, the correctness for the logic, as well as the time under ideal condition of the protocol are verified with ASK-CTL, which is a model checking tool based on Computational Tree Logic (CTL) supported by CPN. The results of verification could meet the expected results, preliminary showing that the verification method is reasonable. Furthermore, on the basis of some specific technical indicators in the train control system during the implementation, the timed characteristics of the protocol in a stochastical environment are simulated with CPN, and the results of simulation are assessed with mathematical statistics, to reflect how the random factors to affect the performance of the protocol.
The main innovation of the thesis is as follow, compared to the related research domestic and abroad:
(1) Focus on the limitation of Petri net for modeling of complex systems, the thesis proposes the method of modeling hierarchically. Making use of the capability of hierarchical modeling of Colored Petri Net, the logic model of safety communication protocol is established first, then the timed model is established with module of description for time based on the logic model, and finally, module of description for random events is added to reflect the random factors;
(2) Against traditional verification methods for communication protocol cannot verify the function, the thesis proposes model checking to verify the function of safety communication protocol. Focuses on the limitation of Petri net for description of sequence of events, the thesis proposes to apply ASK-CTL, supported by Colored Petri Net, to implement model checking for logic of safety communication protocol;
(3) Against model checking cannot represent specific performance, the thesis proposes simulation to obtain the performance of safety communication protocol by Colored Petri Net, and assess the simulation results through mathematical statistics;
(4) Against method of verification for safety-critical system does not consider performance, the thesis proposes combination of model checking and simulation with Colored Petri Net, to implement the verification of safety communication protocol for both function and performance.
The thesis ends with an accomplishment of the verification for the safety communication protocol in the Communication Based Train Control system (CBTC). Model checking with ASK-CTL and simulation with Colored Petri Net are used to verify the function and performance of the protocol, which could not only prove the rationality of the verification method in the thesis, but also guide the development of the protocol.
引文
[1]IEEE 1474.1-1999. IEEE Standard for Communications-Based Train Control (CBTC) Performance and Functional Requirements [S]. IEEE Vehicular Technology Society.
[2]IEEE 1474.2-2003. IEEE Standard for User Interface Requirements in Communication-Based Train Control (CBTC) Systems [S]:IEEE Vehicular Technology Society.
[3]IEEE 1474.3-2008. IEEE Recommended Practice for Communications-Based Train Control (CBTC) System Design and Functional Allocations [S]:IEEE Vehicular Technology Society.
[4]范丽君.ETCS技术在列控系统中应用的探讨[J].中国铁道科学,2003,24(3)：11-16.
[5]Neil Storey. Safety-Critical Computer Systems [M]. Addison-Wesley,1996.
[6]CENELEC. EN 50159-2 Railway Applications-Safety related communication in open transmission systems [S],2001.
[7]XU TianHua, TANG Tao, GAO ChunHai, CAI BaiGen. Dependability analysis of the data communication system in train control system [J]. Science in China Series E:Technological Sciences,2009,52 (9):2605-2618.
[8]ERTMS. Euroradio FIS:class 1 requirements [S].2003.
[9]CENELEC. EN 50126 Railway Applications-Specification and demonstration of reliability, availability, maintainability and safety (RAMS) [S],2001.
[10]ALSTOM. FSFB/2 Safety Protocol Requirements Specification.1999.
[11]A. A. Group, "PROFIsafe:Networked Safely for Process and Factory Automation [S].2006.
[12]ANSALDO SIGNAL-CSEE Transport, BDU-CC Interface Definition [S].2006.
[13]Suzana Andova, Cas Cremers, Kristian Gj(?)steen, Sjouke Mauw, Stig F. Mj(?)lsnes, Sasa Radomirovi'c. A framework for compositional verification of security protocols [J]. Information and Computation,2008,206 (2):425-459.
[14]Antonio Izquierdo, Jose M. Sierra, Joaquin Torres. An analysis of conformance issues in implementations of standardized security protocols [J]. Computer Standards & Interfaces,2009,31 (1):246-251.
[15]Alfredo Pironti, Riccardo Sisto. Provably correct Java implementations of Spi Calculus security protocols specifications [J]. Computers & security,2010,29 (3):302-314.
[16]唐涛,徐田华,赵林.列车运行控制系统规范建模与验证[M].北京：中国铁道出版社,2010.
[17]朱力,宁滨.基于802.11g的CBTC车地通信子系统建模与分析[J].铁道学报,2011,33(5)：72-77.
[18]Matthew J. Morley. Safety-level communication in railway interlockings [J]. Science of Computer Programming,1997,29 (1):147-170.
[19]Esposito Rosaria, Lazzaro Armando, Marmo Pietro,et al. Formal Verification of ERTMS EURORADIO Safety Critical Protocol [R]. Ansaldo Segnalamento Ferroviario S.p.A,2005.
[20]Jason J. Scarlett, Robert W. Brennan. Evaluating a new communication protocol for real-time distributed control [J]. Robotics and Computer-Integrated Manufacturing,2011,27 (3):627-635.
[21]Cheng HoTing, Shan Hangguan, Zhuang Weihua. Infotainment and road safety service support in vehicular networking:From a communication perspective [J]. Mechanical Systems and Signal Processing,2011,25 (6):2020-2038.
[22]Marco Di Felice, Luca Bedogni, Luciano Bononi. Group communication on highways:An evaluation study of geocast protocols and applications [J]. Ad Hoc Networks,2012.
[23]Man Cheol Kim, Jinkyun Park, Wondea Jung, Hanjeom Kim, Yoon Joong Kim. Development of a standard communication protocol for an emergency situation management in nuclear power plants [J]. Annals of Nuclear Energy,2010,37 (6):888-893.
[24]Wen Chien Liu, Chyan Goei Chung. Path-based protocol verification approach [J]. Information and Software Technology,2000,42 (4):229-244.
[25]Alwyn E. Goodloe*, Cesar A. Munoz. Compositional verification of a communication protocol for a remotely operated aircraft [J]. In Press, Corrected Proof, Available online 17 November 2011.
[26]陈黎洁,唐涛,吕继东.CBTC中越区切换中断时间分析[J].中国铁道科学,2010,31(5)：125-129.
[27]CHEN Lijie, TANG Tao. Research on the Influence of Communication Delay on Safety Location Of Train in Communication Based Train Control (CBTC) [C].2009 IEEE Intelligent Vehicles Symposium.
[28]刘宏杰,陈黎洁.CBTC列车安全定位中通信中断时间的研究[J].铁道学报,2012,34(6)：40-45.
[29]Gerard. J. Holzmann. Protocol design:redefining the state of the art [J]. IEEE Software,1992,9 (1):17-22.
[30]Paul. W. King. Formalization of Protocol engineering concepts [J]. IEEE Transactions on Computers,1991.40 (4):387-403.
[31]E. Gunawan, T. P. Tong, Shi. Nansi. Survey of formal description techniques (FDTs) for protocol converter design [C]. In Proceedings of IEEE Region 10 Conference on Computer, Communication, Control and Power Engineering.1993.
[32]彭磊.面向服务的WSN体系结构、R&D方法与应用研究[D].博士,电子科技大学,成都,2009.
[33]Carl Adam Petri. Kommunikation mit automaten [D]. PhD dissertation, University of Bonn, Bonn,1962.
[34]罗军舟,沈俊,顾冠群.从Petri网到形式描述技术和协议工程[J].软件学报,2000,11(5)：606-615.
[35]Armin Zimmermann, G"unter Hommel. A train control system case study in model-based real time system design [C]. Proceedings of the International Parallel and Distributed Processing Symposium (IPDPS'03),2003.
[36]陈黎洁,唐涛.基于随机Petri网的GSM-R建模与性能分析[J].铁道学报,2012,34(3)：75-82.
[37]Aladdin Masri, Thomas Bourdeaud'huy, Armand Toguyeni. Performance Analysis of IEEE 802.11b Wireless Networks with Object Oriented Petri Nets [J]. Electronic Notes in Theoretical Computer Science,2009,242 (2):73-85.
[38]Mohamed Bettaz, Mourad Maouche, Moussa Soualmi, Madani Boukebeche. On reusing ATNet modules in protocol specification [J]. Journal of Systems and Software,1994,27 (2):119-128.
[39]Lee. Jong-Kun and Lee. Kwang-Hui. Modeling of the multicast transport protocols using Petri nets [C]. Networks,1995. Theme:Electrotechnology 2000:Communications and Networks, in conjunction with the] International Conference on Information Engineering, Proceedings of IEEE Singapore International.
[40]董存祥.应急事件处置流程建模及其过程协同研究[D].博士,计算机科学与技术学院,天津大学,天津,2010.
[41]J. Wan. Timed Petri Nets:Theory and Application [M]. Springer,1998.
[42]W. M. Zuberek. Timed Petri nets definitions, Properties, and applications [J]. Microelectronics Reliability,1991,31 (4):627-644.
[43]C. Ramehandani. Analysis of Asynchronous Concurrent Systems by Timed Petri Nets [D]. Doctor, Massachusetts Institute of Technology, USA,1973.
[44]P. Merlin and D. Farber. Recoverability of Communication Protocols-Implications of a Theoretical Study [J]. IEEE Transactions on Communications,1976,24 (9):1036-1043.
[45]P. M. Merlin, David J. Farber. A Study of the Recoverability of Computing Systems [D]. Doctor, University of California, Irvine, USA,1974.
[46]G. Jiroveanu, R. K. Boel. A distributed approach for fault detection and diagnosis based on Time Petri Nets [J]. Mathematics and Computers in Simulation,2006,70 (5):287-313.
[47]Richard Lai, Tony Tsang. Timed verification of the reliable adaptive multicast protocol [J]. Journal of Systems and Software,2007,80 (2):224-239.
[48]Franco Cicirelli, Angelo Furfaro, Libero Nigro. Model checking time-dependent system specifications using Time Stream Petri Nets and Uppaal [J]. Applied Mathematics and Computation, 2012,218 (16):8160-8186.
[49]Natkin. Les Reseaux de Petri Stochastiques et Leur Application 1'evaluation des Systmes Informatiques [D]. Doctor, CNAM, FRANCE,1980.
[50]G. Balbo. Introduction to Stochastic Petri Nets [M]. Berlin Heidelberg:Springer-Verlag,2001.
[51]G. Florin, C. Fraize, S. Natkin. Stochastic Petri nets:Properties, applications and tools [J]. Microelectronics Reliability,1991,31 (4):669-697.
[52]G. Bucci, L. Sassoli, E. Vicario. Correctness verification and performance analysis of real-time systems using stochastic preemptive time Petri nets [J]. IEEE Transactions on Software Engineering, 2005,31 (11):913-927.
[53]M. Gribaudo, R. Gaeta. Efficient steady-state analysis of second-order fluid stochastic Petri nets [J]. Performance Evaluation,2006,63 (9):1032-1047.
[54]R. German, A. Heindl. Performance evaluation of IEEE 802.11 wireless LANs with stochastic Petri nets [C]. The 8th International Workshop on Petri Nets and Performance Models,1999:44-53.
[55]Armin Zimmermann, Gunter Hommel. Towards modeling and evaluation of ETCS real-time communication and operation [J]. Journal of Systems and Software,2005,77 (1):47-54.
[56]徐田华,唐涛.列车控制系统中数据通信子系统的帧丢失概率[J].中国铁道科学,2008,29(3)：110-114.
[57]J. Trowitzsch, A. Zimmermann. Using UML State Machines and Petri Nets for the Quantitative Investigation of ETCS [C]. Proceedings of the 1st international conference on Performance evaluation methodologies and tools,2006.
[58]曹源,牛儒,唐涛,穆建成.基于SPN的越区切换模型分析[J].铁道学报,2009,31(4)： 104-107.
[59]L. Mokdad, M. Sene, A. Boukerche. Call Admission Control Performance Analysis in Mobile Networks Using Stochastic Well-Formed Petri Nets. IEEE Transactions on Parallel and Distributed Systems,2011,22 (8):1332-1341.
[60]Osama S. Youness, Wail S. El-Kilani, Waiel F. Abd El-Waned. A behavior and delay equivalent petri net model for performance evaluation of communication protocols [J]. Computer Communications,2008,31 (10):2210-2230.
[61]German R. Performance Analysis of Communication Systems-Modeling with Non-Markovian Stochastic Petri Nets [M]. Chichester:John Wiley & Sons,2000:36-57.
[62]Kurt Jensen. Coloured petri nets and the invariant-method [J]. Theoretical Computer Science, 1981,14 (3):317-336.
[63]K. Jensen. Colored Petri Nets. Basic Concepts, Analysis Methods and Practical Use [M]. Berlin, Heidelberg, New York:Springer-Verlag,1997.
[64]门鹏.基于Petri网的Web服务组合相关技术研究[D].博士,西安电子科技大学,西安,2009.
[65]C. Lawrence, Paulson,柯韦.ML程序设计教程[M].北京：机械工业出版社,2005.
[66]徐田华,唐涛.基于有色Petri网的ETCS通信系统与列车间隔时间分析[J].系统仿真学报,2007,19(21)：5038-5041.
[67]徐田华,赵红礼,唐涛.基于有色Petri网的ETCS无线通信可靠性分析[J].铁道学报,2008,30(1)：38-42.
[68]W. Mata, A. Gonzalez, R. Aquino, A. Crespo, I. Ripoll, M. Capel. A Wireless Networked Embedded System with a New Real-Time Kernel-PaRTiKle [C]. Electronics, Robotics and Automotive Mechanics Conference,2007. CERMA 2007,21-26.
[69]XU Tianhua, TANG Tao. The modeling and Analysis of Data Communication System (DCS) in Communication Based Train Control (CBTC) with Colored Petri Nets [C], Eighth International Symposium on Autonomous Decentralized Systems,2007. ISADS'07,83-92.
[70]Mohammad Abdollahi Azgomi, Ali Khalili. Performance Evaluation of Sensor Medium Access Control Protocol Using Coloured Petri Nets [J]. Electronic Notes in Theoretical Computer Science, 2009,242 (2):31-42.
[71]CHEN Lijie, SHAN Zhenyu, TANG Tao, LIU Hongjie. Performance analysis and verification of safety communication protocol in train control system [J]. Computer Standards & Interfaces,2011, 33 (5):505-518.
[72]CHEN Lijie, TANG Tao, ZHAO Xianqiong, Eckehard Schnieder. Verification of the safety communication protocol in train control system using colored Petri net [J]. Reliability Engineering & System Safety,2012,100:8-18.
[73]L. Mokdad, J. Ben-Othman, B. Yahya, S. Niagne. Performance evaluation tools for QoS MAC protocol for wireless sensor networks [J]. Ad Hoc Networks,2012.
[74]Bellavista, P.; Cinque, M.; Cotroneo, D.; Foschini, L. Self-Adaptive Handoff Management for Mobile Streaming Continuity [J]. IEEE Transactions on Network and Service Management,2009,6 (2):80-94.
[75]A. Sen, V. K. Garg. Formal Verification of Simulation Traces Using Computation Slicing [J]. IEEE Transactions on Computers,2007,56 (4):511-527.
[76]B. Akbarpour, S. Tahar. An approach for the formal verification of DSP designs using Theorem proving [J]. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems,2006, 25 (8):1441-1457.
[77]T. Kropf. Introduction to formal hardware verification [M]. Springer,1999.
[78]W. Denman, M. H. Zaki, S. Tahar. Formal verification of bond graph modeled analogue circuits [J]. Circuits, Devices & Systems, IET,2011,5 (3):243-255.
[79]T. Murata. Petri nets:Properties, analysis and applications [C]. Proceedings of the IEEE,1989, 77:541-580.
[82]J. Peterson. Petri net theory and the modeling of systems [M]. Englewood Cliffs, N J: Practice-Hall,1981.
[81]S. C. Cheung, J. Kramer. Enhancing compositional reachability analysis with context constraints [J]. ACM Software Engineering Notes,1993,18 (5):115-125.
[82]A. Finkel. The minimal coverability graph for Petri nets [R]. LNCS,1993,674:210-243.
[83]Alexander Fronk, Britta Kehden. State space analysis of Petri nets with relation-algebraic methods [J]. Journal of Symbolic Computation,2009,44 (1):15-47.
[84]Richard M. Karp, Raymond E. Miller. Parallel program schemata [J]. Journal of Computer and System Sciences,1969,3 (2):147-195.
[85]R. Kodikara, S. Ling, A. Zaslavsky. Evaluating Cross-layer Context Exchange in Mobile Ad-hoc Networks with Colored Petri Nets [C]. IEEE International Conference on Pervasive Services, 2007,173-176.
[86]L. Liu and J. Billington. Verification of the Capability Exchange Signaling protocol [J]. International Journal on Software Tools for Technology Transfer,2007,9:305-326.
[87]Jae-Ho Lee, Jong-Gyu Hwang, Gwi-Tae Park. Performance evaluation and verification of communication protocol for railway signaling systems [J]. Computer Standards & Interfaces,2005, 27 (3):207-219.
[88]Jae-Dong Lee, Jae-I1 Jung, Jae-Ho Lee, Jong-Gyu Hwang, Jin-Ho Hwang, Sung-Un Kim. Verification and conformance test generation of communication protocol for railway signaling systems [J]. Computer Standards & Interfaces,2007,29 (2):143-151.
[89]Jae-Ho Lee, Jong-Gyu Hwang, Ducko Shin, Kang-Mi Lee, Sung-Un Kim. Development of verification and conformance testing tools for a railway signaling communication protocol [J]. Computer Standards & Interfaces,2009,31 (2):362-371.
[90]Amir Pnueli. The temporal semantics of concurrent programs [J]. Theoretical Computer Science, 1981,13(1):45-60.
[91]Kristin Y. Rozier. Linear Temporal Logic Symbolic Model Checking [J]. Computer Science Review,2011,5 (2):163-203.
[92]Xin He, Ram Kumar, Liping Mu, Terje Gj(?)e(?)ter, Frank Y. Li. Formal verification of a Cooperative Automatic Repeat reQuest MAC protocol [J]. Computer Standards & Interfaces,2012, 34 (4):343-354.
[93]E. M. Clarke, E. A. Emerson, A. P. Sistla. Automatic verification of finite state concurrent system using temporal logical specification [J]. ACM Transaction on Programming Language and Systems,1986,8:244-263.
[94]Pedro Baltazar, Paulo Mateus, Rajagopal Nagarajan, Nikolaos Papanikolaou. Exogenous Probabilistic Computation Tree Logic [J]. Electronic Notes in Theoretical Computer Science,2007, 190 (3):95-110.
[95]J. C. Sloan, T. M. Khoshgoftaar. From Web Service Artifact to a Readable and Verifiable Model [J]. IEEE Transactions on Services Computing,2009,2 (4):277-288.
[96]A. Cheng, S. Christensen, K. H. Mortensen. Model Checking Colored Petri Nets Exploiting Strongly Connected Components [C]. International Workshop on Discrete Event Systems, U. K, 1996,169-177.
[97]Panagiotis Katsaros. A roadmap to electronic payment transaction guarantees and a Colored Petri Net model checking approach [J]. Information and Software Technology,2009,51 (2):235-257.
[98]E. Guralnik, M. Aharoni, A. J. Birnbaum, A. Koyfman. Simulation-Based Verification of Floating-Point Division [J]. IEEE Transactions on Computers,2011,60 (2):176-188.
[99]Jose Machado, Eurico Seabra, Jose C. Campos, Filomena Soares, Celina P. Leao. Safe controllers design for industrial automation systems [J]. Computers & Industrial Engineering,2011, 60 (4):635-653.
[100]K. Radecka, Z. Zilic. Design verification by test vectors and arithmetic transform universal test set [J]. IEEE Transactions on Computers,2004,53 (5):628-640.
[101]Qiang Ye, Mike H. MacGregor. Using simulation to test formally verified protocols in complex environments [J]. Mathematical and Computer Modeling,2011,53 (3):538-551.
[102]R. J. Haines, G. R. Clemo, A. T. D. Munro. Petri-nets for formal verification of MAC protocols [J]. Software, IET,2007,1 (2):39-47.
[103]W. K. Lam. Hardware Design Verification Simulation and Formal Method Based Approaches [M]. Prentice Hall PTR,2005.
[104]高妍妍ASIP体系结构形式化建模与验证方法研究[D].博士,中国科学技术大学,合肥,2009.
[105]Hong-Zhong Huang, Xu Zu. Hierarchical Timed Colored Petri Nets Based Product Development Process Modeling [A]. CSCWD 2004[C]:378-387.
[106]E. Nemeth, T. Bartha, Cs. Fazekas, K.M. Hangos. Verification of a primary-to-secondary leaking safety procedure in a nuclear power plant using colored Petri nets [J]. Reliability Engineering & System Safety,2009,94 (5):942-953.
[107]Euroradio FFFIS:class 1 requirements[S]. http://www. aeif. org//db/docs/ccm/SUBSET-052 v200. PDF,2000.
[108]张曙光CTCS-3级列控系统技术创新总体方案[M]：北京：中国铁道出版社,2008.
[109]Wille R. Restructuring Lattice Theory:An Approach Based on Hierarchies of Concepts [M]. Ordered Sets,1982:445-470.
[110]牛儒,曹源,唐涛ETCS-2级列控系统RBC交接协议的形式化分析[J].铁道学报,2009,31(4)：52-58.
[111]D. Dubois, H. Prade. Processing Fuzzy Temporal Knowledge [J]. IEEE Transactions on System, Man, Cybern.1989,19 (4):729-744.
[112]成飞飞.建筑产品设计过程建模与仿真研究[D].博士论文,哈尔滨工业大学,2009.
[113]D. Dubois, H. Prade. Possibility Theory:an Approach to Computerized Processing of Uncertainty [M]. Plenum:New York.1988.
[114]盛骤,谢式千,潘承毅.概率论与数理统计[M].高等教育出版社.
[115]舒安洁,李开成.CBTC系统信息安全传输的研究[J].微计算机信息.2006.22(3).44-46.
[116]刘雨.CBTC系统通信协议的设计和形式化分析[D].硕士学位论文,北京交通大学,2008.
[117]藤竹.基于EFSM的CBTC通信协议一致性测试的研究[D].硕士学位论文,北京交通大学,2008.
[118]朱俊.基于Petri网的Web服务组合的交互模型及其应用机理的研究[D].博士学位论文,国防科学技术大学,2011.
[119]谢雨飞,徐田华,唐涛.概率模型检验的CBTC系统通信协议的形式化验证[J].北京交通大学学报,2009,33(5)：35-39.
[2]IEEE 1474.2-2003. IEEE Standard for User Interface Requirements in Communication-Based Train Control (CBTC) Systems [S]:IEEE Vehicular Technology Society.
[3]IEEE 1474.3-2008. IEEE Recommended Practice for Communications-Based Train Control (CBTC) System Design and Functional Allocations [S]:IEEE Vehicular Technology Society.
[4]范丽君.ETCS技术在列控系统中应用的探讨[J].中国铁道科学,2003,24(3)：11-16.
[5]Neil Storey. Safety-Critical Computer Systems [M]. Addison-Wesley,1996.
[6]CENELEC. EN 50159-2 Railway Applications-Safety related communication in open transmission systems [S],2001.
[7]XU TianHua, TANG Tao, GAO ChunHai, CAI BaiGen. Dependability analysis of the data communication system in train control system [J]. Science in China Series E:Technological Sciences,2009,52 (9):2605-2618.
[8]ERTMS. Euroradio FIS:class 1 requirements [S].2003.
[9]CENELEC. EN 50126 Railway Applications-Specification and demonstration of reliability, availability, maintainability and safety (RAMS) [S],2001.
[10]ALSTOM. FSFB/2 Safety Protocol Requirements Specification.1999.
[11]A. A. Group, "PROFIsafe:Networked Safely for Process and Factory Automation [S].2006.
[12]ANSALDO SIGNAL-CSEE Transport, BDU-CC Interface Definition [S].2006.
[13]Suzana Andova, Cas Cremers, Kristian Gj(?)steen, Sjouke Mauw, Stig F. Mj(?)lsnes, Sasa Radomirovi'c. A framework for compositional verification of security protocols [J]. Information and Computation,2008,206 (2):425-459.
[14]Antonio Izquierdo, Jose M. Sierra, Joaquin Torres. An analysis of conformance issues in implementations of standardized security protocols [J]. Computer Standards & Interfaces,2009,31 (1):246-251.
[15]Alfredo Pironti, Riccardo Sisto. Provably correct Java implementations of Spi Calculus security protocols specifications [J]. Computers & security,2010,29 (3):302-314.
[16]唐涛,徐田华,赵林.列车运行控制系统规范建模与验证[M].北京：中国铁道出版社,2010.
[17]朱力,宁滨.基于802.11g的CBTC车地通信子系统建模与分析[J].铁道学报,2011,33(5)：72-77.
[18]Matthew J. Morley. Safety-level communication in railway interlockings [J]. Science of Computer Programming,1997,29 (1):147-170.
[19]Esposito Rosaria, Lazzaro Armando, Marmo Pietro,et al. Formal Verification of ERTMS EURORADIO Safety Critical Protocol [R]. Ansaldo Segnalamento Ferroviario S.p.A,2005.
[20]Jason J. Scarlett, Robert W. Brennan. Evaluating a new communication protocol for real-time distributed control [J]. Robotics and Computer-Integrated Manufacturing,2011,27 (3):627-635.
[21]Cheng HoTing, Shan Hangguan, Zhuang Weihua. Infotainment and road safety service support in vehicular networking:From a communication perspective [J]. Mechanical Systems and Signal Processing,2011,25 (6):2020-2038.
[22]Marco Di Felice, Luca Bedogni, Luciano Bononi. Group communication on highways:An evaluation study of geocast protocols and applications [J]. Ad Hoc Networks,2012.
[23]Man Cheol Kim, Jinkyun Park, Wondea Jung, Hanjeom Kim, Yoon Joong Kim. Development of a standard communication protocol for an emergency situation management in nuclear power plants [J]. Annals of Nuclear Energy,2010,37 (6):888-893.
[24]Wen Chien Liu, Chyan Goei Chung. Path-based protocol verification approach [J]. Information and Software Technology,2000,42 (4):229-244.
[25]Alwyn E. Goodloe*, Cesar A. Munoz. Compositional verification of a communication protocol for a remotely operated aircraft [J]. In Press, Corrected Proof, Available online 17 November 2011.
[26]陈黎洁,唐涛,吕继东.CBTC中越区切换中断时间分析[J].中国铁道科学,2010,31(5)：125-129.
[27]CHEN Lijie, TANG Tao. Research on the Influence of Communication Delay on Safety Location Of Train in Communication Based Train Control (CBTC) [C].2009 IEEE Intelligent Vehicles Symposium.
[28]刘宏杰,陈黎洁.CBTC列车安全定位中通信中断时间的研究[J].铁道学报,2012,34(6)：40-45.
[29]Gerard. J. Holzmann. Protocol design:redefining the state of the art [J]. IEEE Software,1992,9 (1):17-22.
[30]Paul. W. King. Formalization of Protocol engineering concepts [J]. IEEE Transactions on Computers,1991.40 (4):387-403.
[31]E. Gunawan, T. P. Tong, Shi. Nansi. Survey of formal description techniques (FDTs) for protocol converter design [C]. In Proceedings of IEEE Region 10 Conference on Computer, Communication, Control and Power Engineering.1993.
[32]彭磊.面向服务的WSN体系结构、R&D方法与应用研究[D].博士,电子科技大学,成都,2009.
[33]Carl Adam Petri. Kommunikation mit automaten [D]. PhD dissertation, University of Bonn, Bonn,1962.
[34]罗军舟,沈俊,顾冠群.从Petri网到形式描述技术和协议工程[J].软件学报,2000,11(5)：606-615.
[35]Armin Zimmermann, G"unter Hommel. A train control system case study in model-based real time system design [C]. Proceedings of the International Parallel and Distributed Processing Symposium (IPDPS'03),2003.
[36]陈黎洁,唐涛.基于随机Petri网的GSM-R建模与性能分析[J].铁道学报,2012,34(3)：75-82.
[37]Aladdin Masri, Thomas Bourdeaud'huy, Armand Toguyeni. Performance Analysis of IEEE 802.11b Wireless Networks with Object Oriented Petri Nets [J]. Electronic Notes in Theoretical Computer Science,2009,242 (2):73-85.
[38]Mohamed Bettaz, Mourad Maouche, Moussa Soualmi, Madani Boukebeche. On reusing ATNet modules in protocol specification [J]. Journal of Systems and Software,1994,27 (2):119-128.
[39]Lee. Jong-Kun and Lee. Kwang-Hui. Modeling of the multicast transport protocols using Petri nets [C]. Networks,1995. Theme:Electrotechnology 2000:Communications and Networks, in conjunction with the] International Conference on Information Engineering, Proceedings of IEEE Singapore International.
[40]董存祥.应急事件处置流程建模及其过程协同研究[D].博士,计算机科学与技术学院,天津大学,天津,2010.
[41]J. Wan. Timed Petri Nets:Theory and Application [M]. Springer,1998.
[42]W. M. Zuberek. Timed Petri nets definitions, Properties, and applications [J]. Microelectronics Reliability,1991,31 (4):627-644.
[43]C. Ramehandani. Analysis of Asynchronous Concurrent Systems by Timed Petri Nets [D]. Doctor, Massachusetts Institute of Technology, USA,1973.
[44]P. Merlin and D. Farber. Recoverability of Communication Protocols-Implications of a Theoretical Study [J]. IEEE Transactions on Communications,1976,24 (9):1036-1043.
[45]P. M. Merlin, David J. Farber. A Study of the Recoverability of Computing Systems [D]. Doctor, University of California, Irvine, USA,1974.
[46]G. Jiroveanu, R. K. Boel. A distributed approach for fault detection and diagnosis based on Time Petri Nets [J]. Mathematics and Computers in Simulation,2006,70 (5):287-313.
[47]Richard Lai, Tony Tsang. Timed verification of the reliable adaptive multicast protocol [J]. Journal of Systems and Software,2007,80 (2):224-239.
[48]Franco Cicirelli, Angelo Furfaro, Libero Nigro. Model checking time-dependent system specifications using Time Stream Petri Nets and Uppaal [J]. Applied Mathematics and Computation, 2012,218 (16):8160-8186.
[49]Natkin. Les Reseaux de Petri Stochastiques et Leur Application 1'evaluation des Systmes Informatiques [D]. Doctor, CNAM, FRANCE,1980.
[50]G. Balbo. Introduction to Stochastic Petri Nets [M]. Berlin Heidelberg:Springer-Verlag,2001.
[51]G. Florin, C. Fraize, S. Natkin. Stochastic Petri nets:Properties, applications and tools [J]. Microelectronics Reliability,1991,31 (4):669-697.
[52]G. Bucci, L. Sassoli, E. Vicario. Correctness verification and performance analysis of real-time systems using stochastic preemptive time Petri nets [J]. IEEE Transactions on Software Engineering, 2005,31 (11):913-927.
[53]M. Gribaudo, R. Gaeta. Efficient steady-state analysis of second-order fluid stochastic Petri nets [J]. Performance Evaluation,2006,63 (9):1032-1047.
[54]R. German, A. Heindl. Performance evaluation of IEEE 802.11 wireless LANs with stochastic Petri nets [C]. The 8th International Workshop on Petri Nets and Performance Models,1999:44-53.
[55]Armin Zimmermann, Gunter Hommel. Towards modeling and evaluation of ETCS real-time communication and operation [J]. Journal of Systems and Software,2005,77 (1):47-54.
[56]徐田华,唐涛.列车控制系统中数据通信子系统的帧丢失概率[J].中国铁道科学,2008,29(3)：110-114.
[57]J. Trowitzsch, A. Zimmermann. Using UML State Machines and Petri Nets for the Quantitative Investigation of ETCS [C]. Proceedings of the 1st international conference on Performance evaluation methodologies and tools,2006.
[58]曹源,牛儒,唐涛,穆建成.基于SPN的越区切换模型分析[J].铁道学报,2009,31(4)： 104-107.
[59]L. Mokdad, M. Sene, A. Boukerche. Call Admission Control Performance Analysis in Mobile Networks Using Stochastic Well-Formed Petri Nets. IEEE Transactions on Parallel and Distributed Systems,2011,22 (8):1332-1341.
[60]Osama S. Youness, Wail S. El-Kilani, Waiel F. Abd El-Waned. A behavior and delay equivalent petri net model for performance evaluation of communication protocols [J]. Computer Communications,2008,31 (10):2210-2230.
[61]German R. Performance Analysis of Communication Systems-Modeling with Non-Markovian Stochastic Petri Nets [M]. Chichester:John Wiley & Sons,2000:36-57.
[62]Kurt Jensen. Coloured petri nets and the invariant-method [J]. Theoretical Computer Science, 1981,14 (3):317-336.
[63]K. Jensen. Colored Petri Nets. Basic Concepts, Analysis Methods and Practical Use [M]. Berlin, Heidelberg, New York:Springer-Verlag,1997.
[64]门鹏.基于Petri网的Web服务组合相关技术研究[D].博士,西安电子科技大学,西安,2009.
[65]C. Lawrence, Paulson,柯韦.ML程序设计教程[M].北京：机械工业出版社,2005.
[66]徐田华,唐涛.基于有色Petri网的ETCS通信系统与列车间隔时间分析[J].系统仿真学报,2007,19(21)：5038-5041.
[67]徐田华,赵红礼,唐涛.基于有色Petri网的ETCS无线通信可靠性分析[J].铁道学报,2008,30(1)：38-42.
[68]W. Mata, A. Gonzalez, R. Aquino, A. Crespo, I. Ripoll, M. Capel. A Wireless Networked Embedded System with a New Real-Time Kernel-PaRTiKle [C]. Electronics, Robotics and Automotive Mechanics Conference,2007. CERMA 2007,21-26.
[69]XU Tianhua, TANG Tao. The modeling and Analysis of Data Communication System (DCS) in Communication Based Train Control (CBTC) with Colored Petri Nets [C], Eighth International Symposium on Autonomous Decentralized Systems,2007. ISADS'07,83-92.
[70]Mohammad Abdollahi Azgomi, Ali Khalili. Performance Evaluation of Sensor Medium Access Control Protocol Using Coloured Petri Nets [J]. Electronic Notes in Theoretical Computer Science, 2009,242 (2):31-42.
[71]CHEN Lijie, SHAN Zhenyu, TANG Tao, LIU Hongjie. Performance analysis and verification of safety communication protocol in train control system [J]. Computer Standards & Interfaces,2011, 33 (5):505-518.
[72]CHEN Lijie, TANG Tao, ZHAO Xianqiong, Eckehard Schnieder. Verification of the safety communication protocol in train control system using colored Petri net [J]. Reliability Engineering & System Safety,2012,100:8-18.
[73]L. Mokdad, J. Ben-Othman, B. Yahya, S. Niagne. Performance evaluation tools for QoS MAC protocol for wireless sensor networks [J]. Ad Hoc Networks,2012.
[74]Bellavista, P.; Cinque, M.; Cotroneo, D.; Foschini, L. Self-Adaptive Handoff Management for Mobile Streaming Continuity [J]. IEEE Transactions on Network and Service Management,2009,6 (2):80-94.
[75]A. Sen, V. K. Garg. Formal Verification of Simulation Traces Using Computation Slicing [J]. IEEE Transactions on Computers,2007,56 (4):511-527.
[76]B. Akbarpour, S. Tahar. An approach for the formal verification of DSP designs using Theorem proving [J]. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems,2006, 25 (8):1441-1457.
[77]T. Kropf. Introduction to formal hardware verification [M]. Springer,1999.
[78]W. Denman, M. H. Zaki, S. Tahar. Formal verification of bond graph modeled analogue circuits [J]. Circuits, Devices & Systems, IET,2011,5 (3):243-255.
[79]T. Murata. Petri nets:Properties, analysis and applications [C]. Proceedings of the IEEE,1989, 77:541-580.
[82]J. Peterson. Petri net theory and the modeling of systems [M]. Englewood Cliffs, N J: Practice-Hall,1981.
[81]S. C. Cheung, J. Kramer. Enhancing compositional reachability analysis with context constraints [J]. ACM Software Engineering Notes,1993,18 (5):115-125.
[82]A. Finkel. The minimal coverability graph for Petri nets [R]. LNCS,1993,674:210-243.
[83]Alexander Fronk, Britta Kehden. State space analysis of Petri nets with relation-algebraic methods [J]. Journal of Symbolic Computation,2009,44 (1):15-47.
[84]Richard M. Karp, Raymond E. Miller. Parallel program schemata [J]. Journal of Computer and System Sciences,1969,3 (2):147-195.
[85]R. Kodikara, S. Ling, A. Zaslavsky. Evaluating Cross-layer Context Exchange in Mobile Ad-hoc Networks with Colored Petri Nets [C]. IEEE International Conference on Pervasive Services, 2007,173-176.
[86]L. Liu and J. Billington. Verification of the Capability Exchange Signaling protocol [J]. International Journal on Software Tools for Technology Transfer,2007,9:305-326.
[87]Jae-Ho Lee, Jong-Gyu Hwang, Gwi-Tae Park. Performance evaluation and verification of communication protocol for railway signaling systems [J]. Computer Standards & Interfaces,2005, 27 (3):207-219.
[88]Jae-Dong Lee, Jae-I1 Jung, Jae-Ho Lee, Jong-Gyu Hwang, Jin-Ho Hwang, Sung-Un Kim. Verification and conformance test generation of communication protocol for railway signaling systems [J]. Computer Standards & Interfaces,2007,29 (2):143-151.
[89]Jae-Ho Lee, Jong-Gyu Hwang, Ducko Shin, Kang-Mi Lee, Sung-Un Kim. Development of verification and conformance testing tools for a railway signaling communication protocol [J]. Computer Standards & Interfaces,2009,31 (2):362-371.
[90]Amir Pnueli. The temporal semantics of concurrent programs [J]. Theoretical Computer Science, 1981,13(1):45-60.
[91]Kristin Y. Rozier. Linear Temporal Logic Symbolic Model Checking [J]. Computer Science Review,2011,5 (2):163-203.
[92]Xin He, Ram Kumar, Liping Mu, Terje Gj(?)e(?)ter, Frank Y. Li. Formal verification of a Cooperative Automatic Repeat reQuest MAC protocol [J]. Computer Standards & Interfaces,2012, 34 (4):343-354.
[93]E. M. Clarke, E. A. Emerson, A. P. Sistla. Automatic verification of finite state concurrent system using temporal logical specification [J]. ACM Transaction on Programming Language and Systems,1986,8:244-263.
[94]Pedro Baltazar, Paulo Mateus, Rajagopal Nagarajan, Nikolaos Papanikolaou. Exogenous Probabilistic Computation Tree Logic [J]. Electronic Notes in Theoretical Computer Science,2007, 190 (3):95-110.
[95]J. C. Sloan, T. M. Khoshgoftaar. From Web Service Artifact to a Readable and Verifiable Model [J]. IEEE Transactions on Services Computing,2009,2 (4):277-288.
[96]A. Cheng, S. Christensen, K. H. Mortensen. Model Checking Colored Petri Nets Exploiting Strongly Connected Components [C]. International Workshop on Discrete Event Systems, U. K, 1996,169-177.
[97]Panagiotis Katsaros. A roadmap to electronic payment transaction guarantees and a Colored Petri Net model checking approach [J]. Information and Software Technology,2009,51 (2):235-257.
[98]E. Guralnik, M. Aharoni, A. J. Birnbaum, A. Koyfman. Simulation-Based Verification of Floating-Point Division [J]. IEEE Transactions on Computers,2011,60 (2):176-188.
[99]Jose Machado, Eurico Seabra, Jose C. Campos, Filomena Soares, Celina P. Leao. Safe controllers design for industrial automation systems [J]. Computers & Industrial Engineering,2011, 60 (4):635-653.
[100]K. Radecka, Z. Zilic. Design verification by test vectors and arithmetic transform universal test set [J]. IEEE Transactions on Computers,2004,53 (5):628-640.
[101]Qiang Ye, Mike H. MacGregor. Using simulation to test formally verified protocols in complex environments [J]. Mathematical and Computer Modeling,2011,53 (3):538-551.
[102]R. J. Haines, G. R. Clemo, A. T. D. Munro. Petri-nets for formal verification of MAC protocols [J]. Software, IET,2007,1 (2):39-47.
[103]W. K. Lam. Hardware Design Verification Simulation and Formal Method Based Approaches [M]. Prentice Hall PTR,2005.
[104]高妍妍ASIP体系结构形式化建模与验证方法研究[D].博士,中国科学技术大学,合肥,2009.
[105]Hong-Zhong Huang, Xu Zu. Hierarchical Timed Colored Petri Nets Based Product Development Process Modeling [A]. CSCWD 2004[C]:378-387.
[106]E. Nemeth, T. Bartha, Cs. Fazekas, K.M. Hangos. Verification of a primary-to-secondary leaking safety procedure in a nuclear power plant using colored Petri nets [J]. Reliability Engineering & System Safety,2009,94 (5):942-953.
[107]Euroradio FFFIS:class 1 requirements[S]. http://www. aeif. org//db/docs/ccm/SUBSET-052 v200. PDF,2000.
[108]张曙光CTCS-3级列控系统技术创新总体方案[M]：北京：中国铁道出版社,2008.
[109]Wille R. Restructuring Lattice Theory:An Approach Based on Hierarchies of Concepts [M]. Ordered Sets,1982:445-470.
[110]牛儒,曹源,唐涛ETCS-2级列控系统RBC交接协议的形式化分析[J].铁道学报,2009,31(4)：52-58.
[111]D. Dubois, H. Prade. Processing Fuzzy Temporal Knowledge [J]. IEEE Transactions on System, Man, Cybern.1989,19 (4):729-744.
[112]成飞飞.建筑产品设计过程建模与仿真研究[D].博士论文,哈尔滨工业大学,2009.
[113]D. Dubois, H. Prade. Possibility Theory:an Approach to Computerized Processing of Uncertainty [M]. Plenum:New York.1988.
[114]盛骤,谢式千,潘承毅.概率论与数理统计[M].高等教育出版社.
[115]舒安洁,李开成.CBTC系统信息安全传输的研究[J].微计算机信息.2006.22(3).44-46.
[116]刘雨.CBTC系统通信协议的设计和形式化分析[D].硕士学位论文,北京交通大学,2008.
[117]藤竹.基于EFSM的CBTC通信协议一致性测试的研究[D].硕士学位论文,北京交通大学,2008.
[118]朱俊.基于Petri网的Web服务组合的交互模型及其应用机理的研究[D].博士学位论文,国防科学技术大学,2011.
[119]谢雨飞,徐田华,唐涛.概率模型检验的CBTC系统通信协议的形式化验证[J].北京交通大学学报,2009,33(5)：35-39.