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

Abstract. 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 work we present a formal real-time rewriting logic semantics for a behavioral sub-set of AADL which includes the essential aspects of its behavior annex. Our semantics is directly executable in Real-Time Maude and provides an AADL simulator and LTL model checking tool called AADL2Maude. AADL2Maude is integrated with OSATE, so that OSATE’s code gen-eration facility is used to automatically transform AADL models into their corresponding Real-Time Maude specifications. Such transformed models can then be executed and model checked by Real-Time Maude. We present our semantics, and two case studies in which safety-critical properties are verified in AADL2Maude.