Software Failure Modes And Effect Analysis Methodology Using Model Checking

The scope and complexity of software system is increasing because of the globalinformatization. Together comes the problem of how to ensure software reliability to makesure of the safety of the corresponding system.Software failure modes and effect analysis (SFMEA) ensure the safety and reliabilityof a system by analyzing and acquiring the essential failure modes of the software system,as well as proposing some control measures to promote the software quality, which hasalready been broadly applied. However, the traditional software FMEA method needs toomuch manual work, while has low precision, poor objectivity and massive work load.Thus, this thesis proposed a software FMEA method combining model checking. Thenew method use a model checking tool (SPIN) to make it more accurate and complete ofthe analysis to the failure modes, and in this way we can improve the safety and reliabilityof the system.Firstly, this thesis introduced the procedure of traditional software FMEA method. Tocounter the defects of traditional SFMEA method, this thesis proposed a software FMEAmethod combining SPIN.Secondly, this thesis introduced the procedure of the new method in early softwaredesign stage and software implementation stage in the way of combining SPIN systemlevel and detail level software FMEA process. This thesis specially described how to setup the system frame and the code PROMELA model. The procedure of how tocomprehensively and accurately analyze the failure cause and failure effect with SPINmodel checker is also described.In the end, this thesis elaborated the entire procedure of our method through a casestudy of software FMEA to one aero engine electronic controller. The procedure anddetails of applying SFMEA method combining SPIN in projects is introduced in this thesis.From the result of the analysis, the feasibility of the new software FMEA methodcombining SPIN is proved.