Polychronous Automata and their Use for Formal Validation of AADL Models

Thierry Gautier 1 Clément Guy 1 Alexandre Honorat 1 Paul Le Guernic 1 Jean-Pierre Talpin 1 Loïc Besnard 1
1 TEA - Tim, Events and Architectures
Inria Rennes – Bretagne Atlantique , IRISA_D4 - LANGAGE ET GÉNIE LOGICIEL
Abstract : This paper investigates how state diagrams can be best represented in the polychronous model of computation (MoC) and proposes to use this model for code validation of behavior specifications in AADL. In this relational MoC, the basic objects are signals, which are related through dataflow equations. Signals are associated with logical clocks, which provide the capability to describe systems in which components obey to multiple clock rates. We propose a model of finite-state automata, called polychronous automata, which is based on clock relations. A specificity of this model is that an automaton is submitted to clock constraints. This allows one to specify a wide range of control-related configurations, either reactive, or restrictive with respect to their control environment. A semantic model is defined for these polychronous automata, that relies on a Boolean algebra of clocks. Based on a previously defined modeling of AADL software architectures using the polychronous MoC, this model of polychronous automata is used as a formal model for the AADL Behavior Annex. This is illustrated with a case study which specifies an adaptive cruise control system.
Type de document :
Article dans une revue
Frontiers of Computer Science, Springer Verlag, 2018, 〈10.1007/s11704-017-6134-5〉
Liste complète des métadonnées

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

Contributeur : Thierry Gautier <>
Soumis le : mercredi 7 décembre 2016 - 11:56:27
Dernière modification le : jeudi 20 décembre 2018 - 01:30:45
Document(s) archivé(s) le : mardi 21 mars 2017 - 07:34:03


Fichiers produits par l'(les) auteur(s)



Thierry Gautier, Clément Guy, Alexandre Honorat, Paul Le Guernic, Jean-Pierre Talpin, et al.. Polychronous Automata and their Use for Formal Validation of AADL Models. Frontiers of Computer Science, Springer Verlag, 2018, 〈10.1007/s11704-017-6134-5〉. 〈hal-01411257〉



Consultations de la notice


Téléchargements de fichiers