Integrated modular avionics system safety analysis based on model checking

Integrated Modular Avionics (IMA), which is the novel concept of avionics architecture, can effectively improve the efficiency of system while reducing resource allocation. However, integration also increases system complexity such as function correlations, the interaction of software and hardware. And it makes the system failure spread to other system in the process of synthesis, has great impact on system safety. Traditional system safety analysis methods (such as Fault Tree Analysis Failure Modes and Effects Analysis), mainly depend on the engineering experience and the personal skills of analyzers, have the limitation of neglecting system failure states and misunderstanding failure effects. To resolve this problem, we introduce a new safety analysis method for integrated modular avionics system in this paper. Model checking, by using a traversing algorithm, can search all system status in a methodical, mathematical way. Use of this analysis process can be automated and the requirement of human experience can be reduced. Finally, it is demonstrated that the method is practical in making safety analysis on the integrated modular avionics system. The analysis process is given based on system requirements specification. With the aid of model checking tool NuSMV, we perform safety analysis. We can automatically identify the minimum failure combination which cause the top event and achieve the purpose of traditional fault tree analysis. The results indicate practicality of this method.