TY - GEN
T1 - Formal semantics and analysis of behavioral AADL models in real-time Maude
AU - Ölveczky, Peter Csaba
AU - Boronat, Artur
AU - Meseguer, José
PY - 2010
Y1 - 2010
N2 - 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.
AB - 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.
UR - http://www.scopus.com/inward/record.url?scp=77954654118&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=77954654118&partnerID=8YFLogxK
U2 - 10.1007/978-3-642-13464-7_5
DO - 10.1007/978-3-642-13464-7_5
M3 - Conference contribution
AN - SCOPUS:77954654118
SN - 3642134637
SN - 9783642134630
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 47
EP - 62
BT - Formal Techniques for Distributed Systems - Joint 12th IFIP WG 6.1 International Conference, FMOODS 2010, and 30th IFIP WG 6.1 International Conference, FORTE 2010, Proceedings
T2 - Joint 12th IFIP WG 6.1 International Conference, FMOODS 2010
Y2 - 7 June 2010 through 9 June 2010
ER -