FTA Based Avionics Software Safety Verification Methodology

As embedded software is taking an important part in safety critical filed, how to ensure the safetyof safety-critical software has recently become a research focus. Fault Tree is a bottom-up causalchain which describes how a failure event occurs. Extracting the safety property of software fromfault tree can provide effective evidence to software safety analysis. But FTA (Fault Tree Analysis)itself can not verify the existence of these system failures. What’s more, it’s impossible to describe thesafety-critical system’s failure with temporal feature using the informal description method oftraditional FTA. Model checking canprecisely verify software system, but it still has technicalbottlenecks in extracting the properties to be verified.The paper proposes a method to verify the safety of embedded software based on FTA. The methodcombines advantages of the systematic of traditional FTA and precise description of model checking.Firstly, we extend traditional FTA and specify the fault tree with linear temporal logic (LTL) to get aLinear Temporal Fault Tree—LTFT, which can describe the safety-critical system’s failure withtemporal feature, and provide a set of LTFT reduction rules based on safety validation requirement.Secondly, according to the LTFT’s characteristics, we improve traditional fault tree’s cut set analysisalgorithm and propose a LTFT cut set analysis algorithm to extract the LTL formula which describesthe software safety property from LTFT. Then we use the extracted safety property to check whetherthe property, which is described in LTL formula, is satisfied in the software design. Finally, we dosafety analysis of a safety-critical software—“flap and slat control system”, using our own modelchecking tool—Espin, to demonstrate the method in detail and prove the method to be effective.