Formalization of the AADL Run-Time Services with Time

TL;DR

This paper extends the formal semantics of AADL to explicitly include timing aspects, supporting reactive state machines and demonstrating an example implementation with BLESS.

Contribution

It introduces a formalization of AADL run-time services with time using modal logic and Kripke structures, expanding support for reactive state machines and providing a practical example.

Findings

Formal semantics of AADL with time using modal logic

Support for reactive state-transition machines in AADL RTS

Implementation example with BLESS and HAMR

Abstract

The Architecture Analysis & Design Language (AADL) is an architecture description language for design of cyber-physical systems--machines controlled by software. The AADL standard, SAE International AS5506D, describes Run-Time Services (RTS) to be provided to execute AADL models in accordance with semantics defined by the standard. The RTS of primary concern are transport services and timing services. Although, the study presented in [1] sets a foundation for the formal semantics of AADL, but without modeling time. This paper extends and simplifies this formalization using a modal logic defined by a Kripke structure, to explicitly include time. The RTS defined in the AADL standard are also expanded to support reactive state-transition machines of the Behavior Specification annex standard language (BA) and its closely-related, formally-defined counterpart, the Behavior Language for Embedded Systems with Software (BLESS). An example of AADL RTS with time, implemented by the High Assurance Modeling and Rapid Engineering for Embedded Systems (HAMR) for state-transition machine behavior written in BLESS, is also presented.