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

Danielle Stewart, Jing (Janet) Liu, Darren Cofer, Mats Heimdahl, Michael W. Whalen, Michael Peterson

Research output: Contribution to journalArticlepeer-review

23 Scopus citations


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.

Original languageEnglish (US)
Article number107649
JournalReliability Engineering and System Safety
StatePublished - Sep 1 2021

Bibliographical note

Funding Information:
This research was funded by NASA, United States of America contract NNL16AB07T and the University of Minnesota College of Science and Engineering, United States of America Graduate Fellowship.

Publisher Copyright:
© 2021


  • AADL
  • Fault analysis
  • Fault injection
  • Model-based safety analysis
  • Model-based systems engineering
  • Safety engineering


Dive into the research topics of 'AADL-Based safety analysis using formal methods applied to aircraft digital systems'. Together they form a unique fingerprint.

Cite this