Research For Aircraft System Deductive Safety Analysis Method Based On Formal Model Checking

Classical deductive safety analysis is implemented by safety engineers manually and mainlyanalysis methods are like fault tree analysis etc. However, there’re some drawbacks of traditionalsafety analysis techniques: highly subjective and dependent on the skill of the analysts, hardlyerror-free and complete. We hypothesize that by redirecting the effort to build models of the systemunder study and its fault model we can both reduce the effort involved and increase the quality of theanalysis. Formal verification techniques, such as model checking methods, have the ability of dealingwith systems of such highly complexity and overcoming these drawbacks to a certain extent.General safety assessment process and traditional safety analysis methods are summarized in thispaper. The fault tree analysis and reliability block diagrams are taken as examples for the introductionof deductive analysis method and the limitation of high requirements is indicated. Therefore this paperstudied on the formal model checking, introduced it into the field of aircraft systems safety analysis,and proposed a method of aircraft system deductive safety analysis based on formal model checking,given the detail analysis process. To deal with the reachable states printed by the model checking tool,a post-processing platform is developed. The Secondary Power System is analyzed as an example ofthis method, and qualitative results (fault tree, minimal cut sets) are obtained.