Formalization of the AADL Run-Time Services with Time

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.