AADL-Based safety analysis using formal methods applied to aircraft digital systems

Model-based engineering tools are increasingly being used for system-level development of safety-critical systems. Architectural and behavioral models provide important information that can be leveraged to improve the system safety analysis process. Model-based design artifacts produced in early stage development activities can be used to perform system safety analysis, reducing costs, and providing accurate results throughout the system life-cycle. In this paper we describe an extension to the Architecture Analysis and Design Language (AADL) that supports modeling of system behavior under failure conditions. This safety annex enables the independent modeling of component failures and allows safety engineers to weave various types of fault behavior into the nominal system model. The accompanying tool support uses model checking to verify safety properties in the presence of faults and comprehensively enumerate all applicable fault combinations leading to failure conditions under quantitative objectives as part of the safety assessment process. The approach allows exploration of the effects of faulty component behavior on system level failure conditions without requiring explicit propagation specifications. It also supports a shared system model, a modeling language that can describe real-time embedded systems, and usable safety analysis artifacts.