一种基于失效传播模型的安全分析方法的研究
|
摘要
对于一旦出现异常就有可能造成生命财产损失或环境破坏的安全苛求系统来说,安全是永恒的主题,采用科学、系统的安全分析方法对系统危险进行辨识、控制、跟踪是这一类系统的设计开发不可缺少的环节。进入21世纪后计算机系统正朝着深度融合计算、通信和控制技术,形成可控、可信的网络化物理设备系统的方向发展,系统的复杂性、动态性和混杂性特征显著增强,已经远远超出了人类对计算机控制系统的行为特征以及设计理论的认识程度,给系统安全分析带来了极大的挑战。
论文针对新一代安全苛求信息物理系统(Cyber Physical System, CPS)的特点,在深入分析了系统偏差行为的时序规律的基础上,定义了基于线性时间的失效传播时序逻辑(Failure Temporal Logic, FTL)系统。并将FTL系统引入失效传播转化符号(Failure Propagation Transformation Notation, FPTN)模型中,提出了Temporal-FPTN模型描述语言及其定性求解方法,为系统危险致因机理及演化规律的分析提供了更加准确、高效的分析方法。论文进一步研究了安全苛求CPS系统的行为、结构动态特征,提出了基于Temporal-FPTN模型的分层模块化动态安全分析(Hierarchical Component Based Dynamic Analysis, HiCBD)框架,从而有效降解了系统功能、结构的复杂性,同时也能够更好地契合系统开发生命周期的主要阶段。
论文的主要创新点如下：
(1)针对传统安全分析方法对偏差行为时序特性描述的不足,提出了基于线性时间概念的FTL系统,用于偏差事件的时序关系描述。在此基础上深入研究并证明了FTL公式的约简法则。
(2)在传统安全分析方法FPTN模型中引入FTL系统,提出了Temporal-FPTN模型。并给出了Temporal-FPTN的高级文本描述,摆脱了模糊图形化描述对失效传播模型自动分析求解限制。
(3)提出了基于零压缩二元判决图(Zero-suppressed Binary Decision Diagrams, ZBDDs)的最小割集序列迭代(Minimal Cut Sequence, MCSQ)求解算法。利用ZBDD有效压缩了割集运算所需要的存储空间,提高了MCSQ搜索迭代的收敛速度。
(4)针对CPS系统功能和行为的复杂性问题,提出了一种基于Temporal-FPTN模型的分层安全分析框架——HiCBD框架,将平面Temporal-FPTN模型发展为分层模型。
论文最后以典型的安全苛求CPS系统——基于通信的列车运行控制(Communication Based Train Control, CBTC)系统为应用对象,采用HiCBD方法完成了CBTC系统的安全分析,得到了系统危险致因的MCSQ,并对于CBTC系统的开发提出了安全相关建议,为CBTC系统的安全设计提供依据。
Safety is an ever-lasting topic for safety system in which any anomaly will result in serious damage to both life and property, as well as destruction of environment. It is therefore indispensable for the design and development of the system of this type to identify, control and trace the hazard events of the system, by means of scientific and systemic safety analysis. However, computer system, since the beginning of the 21st century, tends to coordinate computation, communication and automotive technology to construct a controllable and reliable system with a network of physical equipments. Consequently, the complexity, dynamics and hybridity of the system is increasing dramatically, such that it surpasses human beings'apprehension of the behavior and the principles for the design of the controlling computer systems, and brings about a challenge for safety analysis of the system.
The thesis, on the basis of the specification of the sequence rule of the deviant behavior of the system, defines the Failure Temporal Logic (FTL) for linear time, with respect to the characterization of Safety Critical Cyber Physical System (CPS). It provides the descriptive language and qualitative solution method for Temporal-FPTN model, and a more accurate and effective analysis of the motivation for the harm of the system and the generalization of the evolution of the system. Furthermore, the present study explores the dynamic feature of the behavior and the structure of CPS, and establishes a Hierarchical Component Based Dynamic Analysis Framework (hence, HiCBD), based on Temporal-FPTN model, thus decompounding the function and structure complexity of the system, accommodating the lifecycle of the system.
The innovation of the thesis is as follows:
(1) The study proposes a FTL system depending on linear time which is applied to the characterization of sequential relation of deviant events, and establishes a framework for the transformation of FTL into LTL, on the basis of which a reduction rule for the formula of FTL is demonstrated.
(2) The study, through the addition of the FTL system into Failure Propagation Transformation Notation (hence, FPTN), offers a description of Temporal-FPTN in advanced text, effectively avoids the constraints on the automatic analysis of the Failure Propagation Model with the vague graphics description.
(3) The study, based on ZBDDs, presents a resolution method for Minimum Cut Set seQuence (MCSQ). The application of ZBDD compress the storage space for the computation of cut-set, and simultaneously increases the convergence rate of the iterative search for MCSQ.
(4) The study also forms a framework of Hierarchical Component Based Dynamic Analysis (hence, HiCBD) on the basis of Temporal-FPTN, transforming the Temporal-FPTN model into a hierarchical model.
The thesis ends with an accomplishment of the safety analysis of a kind of typical safety-critical CPS-CBTC system by means of HiCBD. And the MCSQ of each system level hazards has been calculated. The achievements of this study prove to be a reinforcement of the design of CBTC in China.
论文针对新一代安全苛求信息物理系统(Cyber Physical System, CPS)的特点,在深入分析了系统偏差行为的时序规律的基础上,定义了基于线性时间的失效传播时序逻辑(Failure Temporal Logic, FTL)系统。并将FTL系统引入失效传播转化符号(Failure Propagation Transformation Notation, FPTN)模型中,提出了Temporal-FPTN模型描述语言及其定性求解方法,为系统危险致因机理及演化规律的分析提供了更加准确、高效的分析方法。论文进一步研究了安全苛求CPS系统的行为、结构动态特征,提出了基于Temporal-FPTN模型的分层模块化动态安全分析(Hierarchical Component Based Dynamic Analysis, HiCBD)框架,从而有效降解了系统功能、结构的复杂性,同时也能够更好地契合系统开发生命周期的主要阶段。
论文的主要创新点如下：
(1)针对传统安全分析方法对偏差行为时序特性描述的不足,提出了基于线性时间概念的FTL系统,用于偏差事件的时序关系描述。在此基础上深入研究并证明了FTL公式的约简法则。
(2)在传统安全分析方法FPTN模型中引入FTL系统,提出了Temporal-FPTN模型。并给出了Temporal-FPTN的高级文本描述,摆脱了模糊图形化描述对失效传播模型自动分析求解限制。
(3)提出了基于零压缩二元判决图(Zero-suppressed Binary Decision Diagrams, ZBDDs)的最小割集序列迭代(Minimal Cut Sequence, MCSQ)求解算法。利用ZBDD有效压缩了割集运算所需要的存储空间,提高了MCSQ搜索迭代的收敛速度。
(4)针对CPS系统功能和行为的复杂性问题,提出了一种基于Temporal-FPTN模型的分层安全分析框架——HiCBD框架,将平面Temporal-FPTN模型发展为分层模型。
论文最后以典型的安全苛求CPS系统——基于通信的列车运行控制(Communication Based Train Control, CBTC)系统为应用对象,采用HiCBD方法完成了CBTC系统的安全分析,得到了系统危险致因的MCSQ,并对于CBTC系统的开发提出了安全相关建议,为CBTC系统的安全设计提供依据。
Safety is an ever-lasting topic for safety system in which any anomaly will result in serious damage to both life and property, as well as destruction of environment. It is therefore indispensable for the design and development of the system of this type to identify, control and trace the hazard events of the system, by means of scientific and systemic safety analysis. However, computer system, since the beginning of the 21st century, tends to coordinate computation, communication and automotive technology to construct a controllable and reliable system with a network of physical equipments. Consequently, the complexity, dynamics and hybridity of the system is increasing dramatically, such that it surpasses human beings'apprehension of the behavior and the principles for the design of the controlling computer systems, and brings about a challenge for safety analysis of the system.
The thesis, on the basis of the specification of the sequence rule of the deviant behavior of the system, defines the Failure Temporal Logic (FTL) for linear time, with respect to the characterization of Safety Critical Cyber Physical System (CPS). It provides the descriptive language and qualitative solution method for Temporal-FPTN model, and a more accurate and effective analysis of the motivation for the harm of the system and the generalization of the evolution of the system. Furthermore, the present study explores the dynamic feature of the behavior and the structure of CPS, and establishes a Hierarchical Component Based Dynamic Analysis Framework (hence, HiCBD), based on Temporal-FPTN model, thus decompounding the function and structure complexity of the system, accommodating the lifecycle of the system.
The innovation of the thesis is as follows:
(1) The study proposes a FTL system depending on linear time which is applied to the characterization of sequential relation of deviant events, and establishes a framework for the transformation of FTL into LTL, on the basis of which a reduction rule for the formula of FTL is demonstrated.
(2) The study, through the addition of the FTL system into Failure Propagation Transformation Notation (hence, FPTN), offers a description of Temporal-FPTN in advanced text, effectively avoids the constraints on the automatic analysis of the Failure Propagation Model with the vague graphics description.
(3) The study, based on ZBDDs, presents a resolution method for Minimum Cut Set seQuence (MCSQ). The application of ZBDD compress the storage space for the computation of cut-set, and simultaneously increases the convergence rate of the iterative search for MCSQ.
(4) The study also forms a framework of Hierarchical Component Based Dynamic Analysis (hence, HiCBD) on the basis of Temporal-FPTN, transforming the Temporal-FPTN model into a hierarchical model.
The thesis ends with an accomplishment of the safety analysis of a kind of typical safety-critical CPS-CBTC system by means of HiCBD. And the MCSQ of each system level hazards has been calculated. The achievements of this study prove to be a reinforcement of the design of CBTC in China.
引文
[1]Neil Storey. Safety Critical Computer Systems [M]. Addison Wesley Publishing Countries, 1996
[2]蒋本珊.计算机组成原理[M].北京：清华大学出版社,2008.
[3]孟庆宇.尼崎事故的反思[J].铁道知识.2006(4)：24-25.
[4]Rogers Commission. Report of the Presidential Commission on the Space Shuttle Challenger Accident [J/OL]. http://history.nasa.gov/rogersrep/v1ch9.htm.
[5]何积车.Cyber-Physical Systems [J].中国计算机学会通讯.2010.6(1)：25-29.
[6]Kyong-Don Kang,Sang H. Son. Real-Time Data Services for Cyber Physical Systems: 28th International Conference on Distributed Computing Systems Workshops (ICDCS'08) [C],2008,483-488.
[7]John A. Stankovic, Insup Lee, Aloysius Mok. Opportunities and obligations for physical computing systems [J]. Computer.2005.38(11):23-31.
[8]Insup Lee, George Pappas, Rance Cleaveland. High-confidence medical device software and systems [J]. Computer.2005.38(11):33-38.
[9]Edward A. Lee. Cyber Physical Systems:Design Challenges, Technical Report No. UCB/EECS-2008-8 [R]2008.
[10]员春欣.铁路信号容错技术[M].北京：中国铁道出版社,1997.
[11]樊运晓,罗云.系统安全工程[M].北京：化学工业出版社,2009.
[12]Kletz T. HAZOP and HAZAN:Identifying and Accessing Process Industry Standards [M]. 3rd Edition:Hemisphere Publisher,1992.
[13]European Organization for Civil Aviation Equipment.ED-12B/DO-178B——1994. Software Considerations in Airborne Systems and Equipment Certification.17 rue Hamelin 75783-Paris CEDEX 16 France:EUROCAE.
[14]Vesely W. E.. Fault Tree Handbook, US Nuclear Regulatory Committee Report NUREG-0492 [R].US NRC,1981:X.15-18.
[15]Villemeur A. Reliability Availability Maintainability and Safety Assessment [M]. John Willey and Sons,1992.
[16]Nicolas Dulac,N G Leveson. An Approach to Design for Safety in Complex Systems: International Conference on System Engineering (INCOSE'04) [C], Toulouse,2004.
[17]Peter Fenelon, Barry Hebron. Applying HAZOP to Software Engineering Models:Risk Management And Critical Protective Systems:Proceedings of SARSS [C],1994.
[18]O'Connor P. D. T., Fundamental Limitations of Reliability Prediction and Modeling, in Practical Reliability Engineering, O'Connor P. D. T., Editor.1991, John Willey and Sons. 111-117.
[19]Cepin M., Mavko B.. A dynamic fault tree [J]. Reliability Engineering & System Safety. 2002.75:83-91.
[20]Amati S., Dill G., Howald E.. A new approach to solve dynamic fault trees:Reliability and Maintainability Symposium [C],2003.
[21]Wijayarathna P.G., Maekawa. M. Extending Fault Trees with an AND-THEN gate:11th International Symp. on Software Reliability Engineering [C],2000.
[22]Sullivan K., Dugan J., Coppit D.. The Galileo fault tree analysis tool:IEEE International Symp. of Fault Tolerant Computing [C],1999,232-235.
[23]Manian R., Dugan J.B., D. Coppit, et al. Combining various solution techniques for dynamic fault tree analysis of computer systems:The 3rd IEEE International High-Assurance Systems Engineering Symposium [C], Washington DC,1998,21-28.
[24]Y. Dutuit, A. Rauzy. A linear-time algorithm to find modules of fault trees [J]. IEEE Transactions on Reliability.1996.45(3):422-425.
[25]Gulati R., Dugan J.B.. A modular approach for analyzing static and dynamic fault trees: Proceedings of the Annual Reliability and Maintainability Symposium [C], Pennsylvania, 1997,57-63.
[26]Palshikar G. K.. Temporal fault trees [J]. Information and Software Technology.2002.44: 137-150.
[27]Marco Bozzano, Adolfo Villafiorita. Integrating Fault Tree Analysis with Event Ordering Information:European Safety and Reliability Conference [C], Maastricht, the Netherlands, 2003.
[28]Milica Barjaktarovic. The State-of-the-Art in Formal Methods, WetStone Technologies [R]1998.
[29]McMillan K. L.. Symbolic Model Checking. Boston [M]. American Kluwer Academic Publishers,1993.
[30]Gerard Holzmann. The Spin model checker [J]. IEEE Transactions on Software Engineering. 1997.23(5):279-295.
[31]David John Puffery. The Principled Design of Computer System Safety Analyses [D]. University of York,1999.
[32]林闯.随机Petri网和系统性能评价[M].第2版：清华大学出版社,2005.
[33]Henley J., Kumamoto H. Reliability Engineering and Risk Assessment [M].Englewood Clift, NJ:Prentice Hall,1981.
[34]Hassle. Advanced Concept in Fault Tree Analysis System Safety Symposium:Boeing/UW System Safety Symposium [C], A B Means,1965.
[35]Fussell J. B. Synthetic Tree Model, Report ANCR 1098 Aerojet Nuclear Company [R] 1973.
[36]W. E. Vesely. Fault Tree Handbook, US Nuclear Regulatory Committee Report NUREG-0492 [R].US NRC,1981:X.15-18.
[37]Sardella R. A Review of Knowledge-Based Systems for Fault Tree/Event Tree Construction,Tech. Note No.1.95.21 [R].European Commission,1995.
[38]Dugan J. B., Bavuso S. J., Boyd M. A. Fault Trees and Sequence Dependencies: Proceedings of Reliability and Maintainability Symposium [C],1990. IEEE,286-293.
[39]Dugan J. B., Bavuso S. J., Boyd M. A. Dynamic Fault-Tree Models for Fault-Tolerant Computer Systems [J]. IEEE Transactions on Reliability.1992.41(3):363-376.
[40]Leveson N G, Harvey P R. Analyzing Software Safety [J]. IEEE Transactions on Software Engineering.1983. SE-9(5):569-579.
[41]Leveson N G, Harvey P R. Software Fault Tree Analysis [J]. Journal of Systems and Software.1983.3:173-181.
[42]Retch J. L. Systems safety analysis:Failure mode and effect [J]. National Safety News. 1966.
[43]Bussolini J. J. High Reliability Design Techniques Applied to the Lunar Module, Lecture Series No.47 on Reliability on Avionics System [R]1971.
[44]King C. K., Rudd D. F. Design and Maintenance of Economical failure-tolerant process [J]. American Institute Chemical Engineering Journal.1971.18(1):257-269.
[45]Lees P. Less' Loss Prevention in the Process Industries [M]. Elsevier,2005.
[46]Yamada K. Reliability Activities at Toyota Motor Company [J]. JUSE.1977.24(3).
[47]Lawley H. G Operability Study and Hazard Analysis [J]. Chemical Industry Progress.1974. 70:45-56.
[48]Lawley S. Size up plant hazard this way [J]. Hydrocarbon Processing.1976:247-261.
[49]Bondavalli A., Summonsing L. Failure Classification with Respect to Detection:Second Workshop on Future Trends of Distributed Computing Systems [C], Cairo, Egypt,1990, 47-53.
[50]Earthy J. V. Hazard and Operability Studies as an approach to Software Safety Assessment [J]. IEE Computing and Control Division Colloquium on Hazard Analysis Digest.1992.198: 5/1-5/3.
[51]Burns D.J., Piebald R.M. A Modified HAZOP Methodology for Safety Critical System Assessment in Directions in Safety-critical Systems:The Safety Critical System Symposium [C],1993,232-245.
[52]Churlish M. Hazard Analysis Using HAZOP:A Case Study:the 12th International Conference on Computer Safety Reliability and Security (SAFECOMP'93) [C], Poznan-Kiekrz, Poland,1993,99-108.
[53]Zuberek W M. Performance evaluation using unbound timed Petri nets:The Third International Workshop on Petri Nets and Performance Models [C], Kyoto, Japan,1989, 180-186.
[54]N.G. Leveson, J.L. Stolzy. Safety Analysis Using Petri Nets [J]. IEEE Transactions on Software Engineering.1987. SE-13(3):386-397.
[55]Genrich H J. Predicate/Transition Nets:Lecture Notes in Computer Science [C], Berlin, 1987,207-247.
[56]Genrich H J, Hanisch H M, Wollhaf K. Verification of recipe-based control procedures of means of predicate/transition nets:Lecture Notes in Computer Science [C], Berlin,1994, 278-297.
[57]Hanisch H.M. On the use of Petri nets for design, verification and optimization of control procedures for batch processes:IEEE International Conference on Systems, Man and Cybernetics [C], San Antonio,1994,326-330.
[58]Gerzson M., Csaki Z., Hangos K M. Qualitative model based verification of operating procedures by high level Petri nets [J]. Computers & Chemical Engineering.1994.18: S565-S569.
[59]Zimmermand A,Gunter H. A train control system case study in model-based real time system design:International parallel and distributed processing symposium (IPDPS) [C], France,2003,118-126.
[60]Eriksson L. H. Formal Method in development and testing of safety-critical system: Railway Interlocking System:SAFECOMP'96 [C],1999,35-41.
[61]V. H. Garmhausen, S. Campos, A. Cimatti. Verification of a safety-critical railway interlocking system with real-time constraints [J]. Science of computer programming.2000. 36:53-64.
[62]D. Clarke, H. B. Abdallah, I. Lee. An integrated graphical and textual toolset for the specification and analysis of resource-bounded real-time system:In:Proc. Of the 1996 workshop on computer-aided verification [C], Berlin,1996,402-405.]
[63]Law a M, Kelton W D. Simulation Modeling and Analysis [M]. Third Edition. Boston: McGraw-Hill,2002:400-410.
[64]Fishwick P A. Simulation Model Design and Execution:Building Digital Worlds [M].New Jersey:Prentice Hall,1995:350-370.
[65]Cassandras C. Discrete Event Systems:Modeling and Performance Analysis [M]. Irwin Inc and Aksen Associates,1993.
[66]Michael M. Modeling and Simulation of Train Control Systems using Petri Nets:FM'99 Formal Methods. World Congress on Formal Methods in the Development of Computing Systems [C], Berlin,1999.
[67]Alain Griffault and Aymeric Vincent. The Mec 5 model-checker. In Proceedings of the 16th International Conference on Computed Aided Verification (CAV 2004) [C], Boston, MA, USA, July 13-17,2004.
[68]A. Hinton, M. Z. Kwiatkowska, G Norman, et al. PRISM:A Tool for Automatic Verification of Probabilistic Systems:TACAS 2006 [C],2006,441-444.
[69]Fenelon P, Mcdermid J.A. Integrated Techniques for Software Safety Analysis:IEE Computing and Control Division Colloquium on Hazard Analysis Digest [C], London,1992, 211-216.
[70]Fenelon P., Mcdermid J.A. An Integrated Toolset For Software Safety Analysis [J]. Journal of Systems and Software.1993:2/1-2/16.
[71]Papadopoulos Y., Mcdermid J. A. A new method for Safety Analysis and the Mechanical Synthesis of Fault Trees in Complex Systems:ICSSEA'99,12th International Conference on Software and Systems Engineering and their Applications [C], Paris,1999,1-9.
[72]Papadopoulos Y, Mcdermid J. A. Hierarchically Performed Hazard Origin and Propagation Studies:18th International Conference on Computer Safety, Reliability and Security SAFECOMP'99 [C], Toulouse France,1999,139-152.
[73]Martin Walker,Yiannis Papadopoulos. Synthesis and analysis of temporal fault trees with PANDORA The time of Priority AND gates [J]. Nonlinear Analysis:Hybrid Systems. 2008(2):368-382.
[74]Martin Walker,Yiannis Papadopoulos. PANDORA 2:THE TIME OF PRIORITY-OR GATES:IFAC Workshop on Dependable Control of Discrete Event Systems DCDS'07 [C], Paris,2007.
[75]Fussel, J.B., Aber, et al. On quantitative analysis of PAND failure logic [J]. IEEE Trans. on Reliability.1976.25(5):324-326.
[76]W. E. Vesely, W.E., Stamatelatos, et al.2002. Fault Tree Handbook with Aerospace Applications[S]:NASA Office of Safety and Mission Assurance.
[77]Martin Walker, Leonardo Bottaci, Yiannis Papadopoulos. Compositional Temporal Fault Tree Analysis:SAFECOMP 2007 26th International Conference on Computer Safety, Reliability, and Security [C], Nuremberg,2007,106-119.
[78]Michael Huth, Mark Ryan.面向计算机科学的数理逻辑系统建模与推理[M].第2版.北京：机械工业出版社,2005：175-186.
[79]曾声奎,赵廷弟.系统可靠性分析教程[M].北京：北京航空航天大学出版社,2004.
[80]IEC 62280-1——2002. Railway applications-Communication, signaling and processing systems-Part1:Safety-related communication in closed transmission systems [S].Switzerland:IEC.
[81]IEC 62280-2——2002. Railway applications-Communication, signaling and processing systems-Part2:Safety-related communication in open transmission systems [S].Switzerland:Iec.
[82]IEC 61508-1——1998. Functional safety of electrical/electronic/programmable electronic safety-related systems-Part 1:General requirements [S]:Iec.
[83]IEC 61508-2——2002. Functional safety of electrical/electronic/programmable electronic safety-related systems-Part 2:Requirements for electrical/electronic/programmable electronic safety-related systems [S]:Iec.
[84]IEC 61508-3——2002. Functional safety of electrical/electronic/programmable electronic safety-related systems-Part 3:Software requirements [S]:Iec.
[85]IEC 61508-4——1998. Functional safety of electrical/electronic/programmable electronic safety-related systems-Part 4:Definitions and abbreviations [S]:Iec.
[86]IEC61508-5——2002. Functional safety of electrical/electronic/programmable electronic safety-related systems-Part 5:Example of methods for the determination of safety integrity levels [S]:Iec.
[87]IEC 61508-6——2002. Functional safety of electrical/electronic/programmable electronic safety-related systems-Part 6:Guidelines on the application of IEC 61508-2 and IEC 61508-3 [S]:Iec.
[88]IEC 61508-7——2002. Functional safety of electrical/electronic/programmable electronic safety-related systems-Part 7:Overview of techniques and measures [S]:Iec.
[89]ED-12B/DO-178B——1994. Software Considerations in Airborne Systems and Equipment Certification [S].17 rue hamelin 75783-Paris CEDEX 16 France:European Organization for Civil Aviation Equipment.
[90]EN 50126——1999. Railway applications-The specification and demonstration of Reliability, Availability, Maintainability and Safety (RAMS) [S].UK:Cenelec.
[91]EN 50128——2001. Railway application-Communications, signaling and processing systems-Software for railway control and protection systems [S].UK:Cenelec.
[92]EN 50129——2003. Railway applications-Communication, signaling and processing systems-Safety related electronic systems for signaling [S].UK:Cenelec.
[93]Minato S. Zero—suppressed BDDS for Set Manipulation in Combinatorial problems:IEEE Design Automation Conference [C],1993.
[94]Alam M., Al-Saga U. M. Quantitative Reliability Evaluation of Repairable Phased-Mission System Using the Markov Approach [J]. IEEE Trans. on Reliability.1986:498-503.
[95]燕飞.轨道交通列车运行控制系统的形式化建模和模型检验方法的研究[D].北京：北京交通大学,2007.
[96]牛儒,唐涛.基于CPN的CBTC地面数据通信系统仿真和分析[J].系统仿真学报.2008.20(17)：4744-4747.
[97]王俊峰.基于通信的新型列车控制系统理论分析及在青藏线应用研究[D].北京：北京交通大学,2002.1-2
[98]IEEE 1471.1——1999. IEEE Standard for Communications-Based Train Control (CBTC) Performance and Functional Requirements [S]:IEEE Vehicular Technology Society.
[99]IEEE 1474.2——2003. IEEE Standard for User Interface Requirements in Communication-Based Train Control (CBTC) Systems [S]:IEEE Vehicular Technology Society.
[100]IEEE 1474.3——2008. IEEE Recommended Practice for Communications-Based Train Control (CBTC) System Design and Functional Allocations [S]:IEEE Vehicular Technology Society.
[101]徐田华.概率模型检验的研究及其在列车运行控制系统中的应用[D].北京：北京交通大学,2007.73-75
[102]Nancy Leveson. Software:System Safety And Computers [M]. Addison-Wesley Professional,1995
[103]曾天翔,朱美娴,周鸣岐等.可靠性维修性保障性术语集[M].北京：国防工业出版社,2002
[104]古天龙,徐周波.有序二叉决策图及应用[M].北京：科学出版社,2009：58-87
[105]Edmund M. Clarke, Jr., Orna Grumberg, et. Model checking [M]. Cambridge:MIT Press, 1999.
[106]Arjan van der Schaft, Hans Schumacher.混成动态系统引论[M].北京：清华大学出版社,2007.
[2]蒋本珊.计算机组成原理[M].北京：清华大学出版社,2008.
[3]孟庆宇.尼崎事故的反思[J].铁道知识.2006(4)：24-25.
[4]Rogers Commission. Report of the Presidential Commission on the Space Shuttle Challenger Accident [J/OL]. http://history.nasa.gov/rogersrep/v1ch9.htm.
[5]何积车.Cyber-Physical Systems [J].中国计算机学会通讯.2010.6(1)：25-29.
[6]Kyong-Don Kang,Sang H. Son. Real-Time Data Services for Cyber Physical Systems: 28th International Conference on Distributed Computing Systems Workshops (ICDCS'08) [C],2008,483-488.
[7]John A. Stankovic, Insup Lee, Aloysius Mok. Opportunities and obligations for physical computing systems [J]. Computer.2005.38(11):23-31.
[8]Insup Lee, George Pappas, Rance Cleaveland. High-confidence medical device software and systems [J]. Computer.2005.38(11):33-38.
[9]Edward A. Lee. Cyber Physical Systems:Design Challenges, Technical Report No. UCB/EECS-2008-8 [R]2008.
[10]员春欣.铁路信号容错技术[M].北京：中国铁道出版社,1997.
[11]樊运晓,罗云.系统安全工程[M].北京：化学工业出版社,2009.
[12]Kletz T. HAZOP and HAZAN:Identifying and Accessing Process Industry Standards [M]. 3rd Edition:Hemisphere Publisher,1992.
[13]European Organization for Civil Aviation Equipment.ED-12B/DO-178B——1994. Software Considerations in Airborne Systems and Equipment Certification.17 rue Hamelin 75783-Paris CEDEX 16 France:EUROCAE.
[14]Vesely W. E.. Fault Tree Handbook, US Nuclear Regulatory Committee Report NUREG-0492 [R].US NRC,1981:X.15-18.
[15]Villemeur A. Reliability Availability Maintainability and Safety Assessment [M]. John Willey and Sons,1992.
[16]Nicolas Dulac,N G Leveson. An Approach to Design for Safety in Complex Systems: International Conference on System Engineering (INCOSE'04) [C], Toulouse,2004.
[17]Peter Fenelon, Barry Hebron. Applying HAZOP to Software Engineering Models:Risk Management And Critical Protective Systems:Proceedings of SARSS [C],1994.
[18]O'Connor P. D. T., Fundamental Limitations of Reliability Prediction and Modeling, in Practical Reliability Engineering, O'Connor P. D. T., Editor.1991, John Willey and Sons. 111-117.
[19]Cepin M., Mavko B.. A dynamic fault tree [J]. Reliability Engineering & System Safety. 2002.75:83-91.
[20]Amati S., Dill G., Howald E.. A new approach to solve dynamic fault trees:Reliability and Maintainability Symposium [C],2003.
[21]Wijayarathna P.G., Maekawa. M. Extending Fault Trees with an AND-THEN gate:11th International Symp. on Software Reliability Engineering [C],2000.
[22]Sullivan K., Dugan J., Coppit D.. The Galileo fault tree analysis tool:IEEE International Symp. of Fault Tolerant Computing [C],1999,232-235.
[23]Manian R., Dugan J.B., D. Coppit, et al. Combining various solution techniques for dynamic fault tree analysis of computer systems:The 3rd IEEE International High-Assurance Systems Engineering Symposium [C], Washington DC,1998,21-28.
[24]Y. Dutuit, A. Rauzy. A linear-time algorithm to find modules of fault trees [J]. IEEE Transactions on Reliability.1996.45(3):422-425.
[25]Gulati R., Dugan J.B.. A modular approach for analyzing static and dynamic fault trees: Proceedings of the Annual Reliability and Maintainability Symposium [C], Pennsylvania, 1997,57-63.
[26]Palshikar G. K.. Temporal fault trees [J]. Information and Software Technology.2002.44: 137-150.
[27]Marco Bozzano, Adolfo Villafiorita. Integrating Fault Tree Analysis with Event Ordering Information:European Safety and Reliability Conference [C], Maastricht, the Netherlands, 2003.
[28]Milica Barjaktarovic. The State-of-the-Art in Formal Methods, WetStone Technologies [R]1998.
[29]McMillan K. L.. Symbolic Model Checking. Boston [M]. American Kluwer Academic Publishers,1993.
[30]Gerard Holzmann. The Spin model checker [J]. IEEE Transactions on Software Engineering. 1997.23(5):279-295.
[31]David John Puffery. The Principled Design of Computer System Safety Analyses [D]. University of York,1999.
[32]林闯.随机Petri网和系统性能评价[M].第2版：清华大学出版社,2005.
[33]Henley J., Kumamoto H. Reliability Engineering and Risk Assessment [M].Englewood Clift, NJ:Prentice Hall,1981.
[34]Hassle. Advanced Concept in Fault Tree Analysis System Safety Symposium:Boeing/UW System Safety Symposium [C], A B Means,1965.
[35]Fussell J. B. Synthetic Tree Model, Report ANCR 1098 Aerojet Nuclear Company [R] 1973.
[36]W. E. Vesely. Fault Tree Handbook, US Nuclear Regulatory Committee Report NUREG-0492 [R].US NRC,1981:X.15-18.
[37]Sardella R. A Review of Knowledge-Based Systems for Fault Tree/Event Tree Construction,Tech. Note No.1.95.21 [R].European Commission,1995.
[38]Dugan J. B., Bavuso S. J., Boyd M. A. Fault Trees and Sequence Dependencies: Proceedings of Reliability and Maintainability Symposium [C],1990. IEEE,286-293.
[39]Dugan J. B., Bavuso S. J., Boyd M. A. Dynamic Fault-Tree Models for Fault-Tolerant Computer Systems [J]. IEEE Transactions on Reliability.1992.41(3):363-376.
[40]Leveson N G, Harvey P R. Analyzing Software Safety [J]. IEEE Transactions on Software Engineering.1983. SE-9(5):569-579.
[41]Leveson N G, Harvey P R. Software Fault Tree Analysis [J]. Journal of Systems and Software.1983.3:173-181.
[42]Retch J. L. Systems safety analysis:Failure mode and effect [J]. National Safety News. 1966.
[43]Bussolini J. J. High Reliability Design Techniques Applied to the Lunar Module, Lecture Series No.47 on Reliability on Avionics System [R]1971.
[44]King C. K., Rudd D. F. Design and Maintenance of Economical failure-tolerant process [J]. American Institute Chemical Engineering Journal.1971.18(1):257-269.
[45]Lees P. Less' Loss Prevention in the Process Industries [M]. Elsevier,2005.
[46]Yamada K. Reliability Activities at Toyota Motor Company [J]. JUSE.1977.24(3).
[47]Lawley H. G Operability Study and Hazard Analysis [J]. Chemical Industry Progress.1974. 70:45-56.
[48]Lawley S. Size up plant hazard this way [J]. Hydrocarbon Processing.1976:247-261.
[49]Bondavalli A., Summonsing L. Failure Classification with Respect to Detection:Second Workshop on Future Trends of Distributed Computing Systems [C], Cairo, Egypt,1990, 47-53.
[50]Earthy J. V. Hazard and Operability Studies as an approach to Software Safety Assessment [J]. IEE Computing and Control Division Colloquium on Hazard Analysis Digest.1992.198: 5/1-5/3.
[51]Burns D.J., Piebald R.M. A Modified HAZOP Methodology for Safety Critical System Assessment in Directions in Safety-critical Systems:The Safety Critical System Symposium [C],1993,232-245.
[52]Churlish M. Hazard Analysis Using HAZOP:A Case Study:the 12th International Conference on Computer Safety Reliability and Security (SAFECOMP'93) [C], Poznan-Kiekrz, Poland,1993,99-108.
[53]Zuberek W M. Performance evaluation using unbound timed Petri nets:The Third International Workshop on Petri Nets and Performance Models [C], Kyoto, Japan,1989, 180-186.
[54]N.G. Leveson, J.L. Stolzy. Safety Analysis Using Petri Nets [J]. IEEE Transactions on Software Engineering.1987. SE-13(3):386-397.
[55]Genrich H J. Predicate/Transition Nets:Lecture Notes in Computer Science [C], Berlin, 1987,207-247.
[56]Genrich H J, Hanisch H M, Wollhaf K. Verification of recipe-based control procedures of means of predicate/transition nets:Lecture Notes in Computer Science [C], Berlin,1994, 278-297.
[57]Hanisch H.M. On the use of Petri nets for design, verification and optimization of control procedures for batch processes:IEEE International Conference on Systems, Man and Cybernetics [C], San Antonio,1994,326-330.
[58]Gerzson M., Csaki Z., Hangos K M. Qualitative model based verification of operating procedures by high level Petri nets [J]. Computers & Chemical Engineering.1994.18: S565-S569.
[59]Zimmermand A,Gunter H. A train control system case study in model-based real time system design:International parallel and distributed processing symposium (IPDPS) [C], France,2003,118-126.
[60]Eriksson L. H. Formal Method in development and testing of safety-critical system: Railway Interlocking System:SAFECOMP'96 [C],1999,35-41.
[61]V. H. Garmhausen, S. Campos, A. Cimatti. Verification of a safety-critical railway interlocking system with real-time constraints [J]. Science of computer programming.2000. 36:53-64.
[62]D. Clarke, H. B. Abdallah, I. Lee. An integrated graphical and textual toolset for the specification and analysis of resource-bounded real-time system:In:Proc. Of the 1996 workshop on computer-aided verification [C], Berlin,1996,402-405.]
[63]Law a M, Kelton W D. Simulation Modeling and Analysis [M]. Third Edition. Boston: McGraw-Hill,2002:400-410.
[64]Fishwick P A. Simulation Model Design and Execution:Building Digital Worlds [M].New Jersey:Prentice Hall,1995:350-370.
[65]Cassandras C. Discrete Event Systems:Modeling and Performance Analysis [M]. Irwin Inc and Aksen Associates,1993.
[66]Michael M. Modeling and Simulation of Train Control Systems using Petri Nets:FM'99 Formal Methods. World Congress on Formal Methods in the Development of Computing Systems [C], Berlin,1999.
[67]Alain Griffault and Aymeric Vincent. The Mec 5 model-checker. In Proceedings of the 16th International Conference on Computed Aided Verification (CAV 2004) [C], Boston, MA, USA, July 13-17,2004.
[68]A. Hinton, M. Z. Kwiatkowska, G Norman, et al. PRISM:A Tool for Automatic Verification of Probabilistic Systems:TACAS 2006 [C],2006,441-444.
[69]Fenelon P, Mcdermid J.A. Integrated Techniques for Software Safety Analysis:IEE Computing and Control Division Colloquium on Hazard Analysis Digest [C], London,1992, 211-216.
[70]Fenelon P., Mcdermid J.A. An Integrated Toolset For Software Safety Analysis [J]. Journal of Systems and Software.1993:2/1-2/16.
[71]Papadopoulos Y., Mcdermid J. A. A new method for Safety Analysis and the Mechanical Synthesis of Fault Trees in Complex Systems:ICSSEA'99,12th International Conference on Software and Systems Engineering and their Applications [C], Paris,1999,1-9.
[72]Papadopoulos Y, Mcdermid J. A. Hierarchically Performed Hazard Origin and Propagation Studies:18th International Conference on Computer Safety, Reliability and Security SAFECOMP'99 [C], Toulouse France,1999,139-152.
[73]Martin Walker,Yiannis Papadopoulos. Synthesis and analysis of temporal fault trees with PANDORA The time of Priority AND gates [J]. Nonlinear Analysis:Hybrid Systems. 2008(2):368-382.
[74]Martin Walker,Yiannis Papadopoulos. PANDORA 2:THE TIME OF PRIORITY-OR GATES:IFAC Workshop on Dependable Control of Discrete Event Systems DCDS'07 [C], Paris,2007.
[75]Fussel, J.B., Aber, et al. On quantitative analysis of PAND failure logic [J]. IEEE Trans. on Reliability.1976.25(5):324-326.
[76]W. E. Vesely, W.E., Stamatelatos, et al.2002. Fault Tree Handbook with Aerospace Applications[S]:NASA Office of Safety and Mission Assurance.
[77]Martin Walker, Leonardo Bottaci, Yiannis Papadopoulos. Compositional Temporal Fault Tree Analysis:SAFECOMP 2007 26th International Conference on Computer Safety, Reliability, and Security [C], Nuremberg,2007,106-119.
[78]Michael Huth, Mark Ryan.面向计算机科学的数理逻辑系统建模与推理[M].第2版.北京：机械工业出版社,2005：175-186.
[79]曾声奎,赵廷弟.系统可靠性分析教程[M].北京：北京航空航天大学出版社,2004.
[80]IEC 62280-1——2002. Railway applications-Communication, signaling and processing systems-Part1:Safety-related communication in closed transmission systems [S].Switzerland:IEC.
[81]IEC 62280-2——2002. Railway applications-Communication, signaling and processing systems-Part2:Safety-related communication in open transmission systems [S].Switzerland:Iec.
[82]IEC 61508-1——1998. Functional safety of electrical/electronic/programmable electronic safety-related systems-Part 1:General requirements [S]:Iec.
[83]IEC 61508-2——2002. Functional safety of electrical/electronic/programmable electronic safety-related systems-Part 2:Requirements for electrical/electronic/programmable electronic safety-related systems [S]:Iec.
[84]IEC 61508-3——2002. Functional safety of electrical/electronic/programmable electronic safety-related systems-Part 3:Software requirements [S]:Iec.
[85]IEC 61508-4——1998. Functional safety of electrical/electronic/programmable electronic safety-related systems-Part 4:Definitions and abbreviations [S]:Iec.
[86]IEC61508-5——2002. Functional safety of electrical/electronic/programmable electronic safety-related systems-Part 5:Example of methods for the determination of safety integrity levels [S]:Iec.
[87]IEC 61508-6——2002. Functional safety of electrical/electronic/programmable electronic safety-related systems-Part 6:Guidelines on the application of IEC 61508-2 and IEC 61508-3 [S]:Iec.
[88]IEC 61508-7——2002. Functional safety of electrical/electronic/programmable electronic safety-related systems-Part 7:Overview of techniques and measures [S]:Iec.
[89]ED-12B/DO-178B——1994. Software Considerations in Airborne Systems and Equipment Certification [S].17 rue hamelin 75783-Paris CEDEX 16 France:European Organization for Civil Aviation Equipment.
[90]EN 50126——1999. Railway applications-The specification and demonstration of Reliability, Availability, Maintainability and Safety (RAMS) [S].UK:Cenelec.
[91]EN 50128——2001. Railway application-Communications, signaling and processing systems-Software for railway control and protection systems [S].UK:Cenelec.
[92]EN 50129——2003. Railway applications-Communication, signaling and processing systems-Safety related electronic systems for signaling [S].UK:Cenelec.
[93]Minato S. Zero—suppressed BDDS for Set Manipulation in Combinatorial problems:IEEE Design Automation Conference [C],1993.
[94]Alam M., Al-Saga U. M. Quantitative Reliability Evaluation of Repairable Phased-Mission System Using the Markov Approach [J]. IEEE Trans. on Reliability.1986:498-503.
[95]燕飞.轨道交通列车运行控制系统的形式化建模和模型检验方法的研究[D].北京：北京交通大学,2007.
[96]牛儒,唐涛.基于CPN的CBTC地面数据通信系统仿真和分析[J].系统仿真学报.2008.20(17)：4744-4747.
[97]王俊峰.基于通信的新型列车控制系统理论分析及在青藏线应用研究[D].北京：北京交通大学,2002.1-2
[98]IEEE 1471.1——1999. IEEE Standard for Communications-Based Train Control (CBTC) Performance and Functional Requirements [S]:IEEE Vehicular Technology Society.
[99]IEEE 1474.2——2003. IEEE Standard for User Interface Requirements in Communication-Based Train Control (CBTC) Systems [S]:IEEE Vehicular Technology Society.
[100]IEEE 1474.3——2008. IEEE Recommended Practice for Communications-Based Train Control (CBTC) System Design and Functional Allocations [S]:IEEE Vehicular Technology Society.
[101]徐田华.概率模型检验的研究及其在列车运行控制系统中的应用[D].北京：北京交通大学,2007.73-75
[102]Nancy Leveson. Software:System Safety And Computers [M]. Addison-Wesley Professional,1995
[103]曾天翔,朱美娴,周鸣岐等.可靠性维修性保障性术语集[M].北京：国防工业出版社,2002
[104]古天龙,徐周波.有序二叉决策图及应用[M].北京：科学出版社,2009：58-87
[105]Edmund M. Clarke, Jr., Orna Grumberg, et. Model checking [M]. Cambridge:MIT Press, 1999.
[106]Arjan van der Schaft, Hans Schumacher.混成动态系统引论[M].北京：清华大学出版社,2007.