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.
Type de document :
Communication dans un congrès
John Hatcliff; Elena Zucca. 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. Springer, Lecture Notes in Computer Science, LNCS-6117, pp.47-62, 2010, Formal Techniques for Distributed Systems. 〈10.1007/978-3-642-13464-7_5〉
Liste complète des métadonnées

Littérature citée [12 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-01055147
Contributeur : Hal Ifip <>
Soumis le : lundi 11 août 2014 - 16:22:17
Dernière modification le : vendredi 11 août 2017 - 16:16:31
Document(s) archivé(s) le : mercredi 26 novembre 2014 - 22:11:26

Fichier

aadl-paper.pdf
Fichiers produits par l'(les) auteur(s)

Licence


Distributed under a Creative Commons Paternité 4.0 International License

Identifiants

Citation

Peter Csaba Ölveczky, Artur Boronat, José Meseguer. Formal Semantics and Analysis of Behavioral AADL Models in Real-Time Maude. John Hatcliff; Elena Zucca. 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. Springer, Lecture Notes in Computer Science, LNCS-6117, pp.47-62, 2010, Formal Techniques for Distributed Systems. 〈10.1007/978-3-642-13464-7_5〉. 〈hal-01055147〉

Partager

Métriques

Consultations de la notice

256

Téléchargements de fichiers

327