Skip to Main content Skip to Navigation
Conference papers

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, AADL lacks 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 object-based real-time concurrent semantics for a behavioral subset of AADL in rewriting logic, 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 generation 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 analyzed in AADL2Maude.
Document type :
Conference papers
Complete list of metadata

Cited literature [12 references]  Display  Hide  Download
Contributor : Hal Ifip Connect in order to contact the contributor
Submitted on : Monday, August 11, 2014 - 4:22:17 PM
Last modification on : Thursday, August 1, 2019 - 2:12:06 PM
Long-term archiving on: : Wednesday, November 26, 2014 - 10:11:26 PM


Files produced by the author(s)


Distributed under a Creative Commons Attribution 4.0 International License



Peter Csaba Ölveczky, Artur Boronat, José Meseguer. Formal Semantics and Analysis of Behavioral AADL Models in Real-Time Maude. Joint 12th IFIP WG 6.1 International Conference on Formal Methods for Open Object-Based Distributed Systems (FMOODS) / 30th IFIP WG 6.1 International Conference on Formal Techniques for Networked and Distributed Systems (FORTE), Jun 2010, Amsterdam, Netherlands. pp.47-62, ⟨10.1007/978-3-642-13464-7_5⟩. ⟨hal-01055147⟩



Record views


Files downloads