Towards a formal semantics for AADL execution model

Jean-François Rolland (1, 2) , Jean-Paul Bodeveix (1, 2) , David Chemouil (3) , M Filali (1, 4) , Dave Thomas (5)

1 IRIT-ACADIE - Assistance à la Certification d’Applications DIstribuées et Embarquées
2 UT3 - Université Toulouse III - Paul Sabatier
3 CNES - Centre National d'Études Spatiales [Toulouse]
4 CNRS - Centre National de la Recherche Scientifique
5 EADS Astrium SAS

In this paper, we present a specification in TLA+ of an AADL execution model. This formal specification is used forderiving a prototype verification tool for AADL the TOPCASED development environment.

Mots clés: dynamic properties; formal semantics; model checking; architecture description languages

Domaines: Systèmes embarqués

Jean-François Rolland, Jean-Paul Bodeveix, David Chemouil, M Filali, Dave Thomas. Towards a formal semantics for AADL execution model. 4th European Congress on Embedded Real Time Software and Systems (ERTS 2008), 3AF : Association Aéronautique et Astronautique de France; SEE : Société de l'électricité, de l'électronique et des technologies de l'information et de la communication, Jan 2008, Toulouse, France. ⟨hal-02269846⟩