Research On Quantitative Analysis Of Dynamic Fault Tree Based On Probabilistic Model Checking

With the rapid development of computer technology,embedded systems,embedded dynamic systems especially,are widely used in safety-critical areas such as avionics,aerospace,and medical.How to guarantee safety and reliability of the embedded dynamic system has become an important research topic in the field of computer.Dynamic fault tree analysis is one of effective safety analysis method which is widely used in reliability analysis of dynamic systems.Dynamic fault tree introduces dynamic logic gate to enhance temporal logic relationship description for dynamic system.However,the process of establishing dynamic fault tree is not reliable because of the lack of precise semantics of dynamic fault tree,potential errors are difficult to be found,and this will lead to more errors in dynamic fault tree analysis phase.In the other hand,Because of the complicated dynamic characteristics of dynamic fault tree,the quantitative analysis method for dynamic fault tree still needs a lot of human labor and we lack accurate and efficient dynamic fault tree quantitative analysis methods and practical tools.For above problems,in this thesis,we present a method of establishing dynamic fault tree based on component,and specify dynamic fault tree by formal language,meanwhile,we present a quantitative analysis method to analysis dynamic fault tree by transforming the dynamic fault tree to PRISM language.Our method is accurate and efficient for dynamic fault tree quantitative analysis.The main contents of this paper include:(1)We present a method of establishing dynamic system based on component,and we present a method of dynamic fault tree automatically generated based on system model.(2)We extract and specify the dynamic fault tree base on Backus-Naur Form with its' probability attribute.Building the model for the quantitative analysis.(3)We transform dynamic fault tree to PRISM model firstly,and we use continuous stochastic logic(CSL)to describe system quantitative analysis properties,Finally,both of the model and properties are imported into PRISM for dynamic fault tree quantitative analysis.We design a model transformation tool——DFT2PRISM,for transforming dynamic fault tree to PRISM model.A case study of firefighting system is given,and it explains the feasibility and effectiveness of our method.Our approach provides a new idea for the software safety analysis.