Formal Semantics and Analysis of Behavioral AADL Models in Real-Time Maude

Date Added: Feb 2010
Format: PDF

AADL is a standard for modeling embedded systems that is widely used in avionics and other safety-critical applications. However, the AADL standard lacks at present a formal semantics, and this severely limits both unambiguous communication among model developers, and the development of simulators and formal analysis tools. In this paper, the authors present a formal real-time rewriting logic semantics for a behavioral subset of AADL which includes the essential aspects of its behavior annex. Their semantics is directly executable in Real-Time Maude and provides an AADL simulator and LTL model checking tool called AADL2Maude.