Research On Automatic Generation Of Fault Tree For Integrated Avionics System Based On Model Checking

Avionics is one of the key systems of a flight.It's a typical safety critical system.The advanced Integrated Modular Avionics(IMA)brings great challenge to system safety analysis while enhancing the resource utilizat ion and operation efficiency of the system.Fault tree analysis is an effective method to improve system safety and reliability.However,traditional manual fault tree generation depends on the personal skills of safety analysis engineers and error-prone.It is difficult to solve the large scale and complexity of system.Based on the formal system models,the model-based system safety analysis techniques improve the accuracy and efficiency of the safety analysis through the automation analysis technology such as model checking.But the fault space is extremely large for the traditional safety analysis method.In the safety analysis of IMA,tradit ional safety analys is methods are difficult to deal with the complexity of the huge systems.We investigate about how to make use of model checking to automatically generate fault tree based on the idea of model-based safety analysis.The detail work is as below:We introduce the feature model from software product line engineering into safety analys is for modeling different system configurations.First,we build the system feature model through obtaining system features and the constraints among the features.The feature model describes the domain knowledge of safety analysis engineers and decreases the fault space.Then based on the s ystem feature model,we propose a framework for automatic generation of fault tree.The framework combines feature modeling and behavior modeling and makes use of model checking technology for automatic analysis.Based on the system feature model and behavior model,the model checker can analys is the behavior of different system configurations thus improving the efficiency of safety analysis.As for system behavior modeling,we propose Fault Labeled Transition System(FLTS)through extending the Kr ipke structure.FLTS maps system and fault behavior to the system features thus it can be used for modeling and analyzing the behavior of different system configurations.Then we transform the automatic generation of fault tree into the model checking problem on the FLTS.On the basis of proving the equal expressive ability of FLTS and featured transition system,we implement our automatic fault tree generation method by modifying the algorithm of SNIP model checker.Based on our fault tree generation method,we build the automat ic fault tree generation tool on the basis of the modified SNIP model checker.The tool can automatically generate the fault tree and show the feature model and fault tree graphically.At last,we apply our automatic fault tree generation method on the A320 hydraulic system to show the effectiveness of the method.