A Semantics of AADL EMV2 and Its Application to Model-Based Fault Tree Generation

The Architecture Analysis & Design Language (AADL) is an SAE International standard for the design and analysis of both the software and hardware architecture of performance-critical real-time systems.

The Error Model Annex, Version 2 (EMV2), extends AADL with concepts to perform safety analyses, such as error types, error propagations, and the impact of errors propagated on components. EMV2 builds on AADL concepts of components and ports to define error propagations and error state machines. These definitions rely on a precise definition of the effect of an error being triggered in this system. The definitions of these concepts rely on powerful abstractions, yet they are mostly defined in plain text.

This report first proposes a formal semantics for EMV2. Then, it shows how to leverage this semantics to generate fault trees from an AADL model enriched with EMV2 information. Defining a formal semantics improves the understanding of the EMV2 model, and the precision of model transformation from EMV2 to analysis techniques.