Formalization of the AADL Run-Time Services

The Architecture and Analysis Definition Language (AADL) is an industry standard modeling language distinguished by its emphasis on strong semantics for modeling real-time embedded systems. These features have led to AADL being used in many formal-methods-oriented projects addressing critical systems. With regard to future directions in programming and systems engineering in general, questions naturally arise regarding how modeling language definitions should be documented so that the meaning of modeled systems can be made clear to all stakeholders. For example, the AADL standard describes Run-Time Services (RTS) that code generation frameworks can implement to realize AADL’s standards-based semantics for thread dispatch and port-based communication. The documentation of these semantics in the AADL standard is semi-formal, allowing for divergent interpretations and thus contradictions when implementing analysis or code generation capabilities. In this paper, we illustrate how key semantic elements of the AADL standard may be documented via a rule-based formalization of key aspects of the AADL RTS as well as additional services and support functions for realistic, interoperable, and assurable implementations. This contribution provides a basis for (a) a more rigorous semantic presentation in upcoming versions of the standard, (b) a common approach to assess compliance of AADL code generation and analysis tools, (c) a foundation for further formalization and mechanization of AADL’s semantics, and (d) a more intuitive documentation of a system’s AADL description via simulation and automatically generated execution scenarios.