24 octobre 2022

Marc Frappier

Les diagrammes états-transitions algébriques (Algebraic State-Transition Diagrams (ASTD)) permettent de combiner des machines à états hiérarchiques avec des opérateurs inspirés des algèbres de processus (séquence, choix, garde, fermeture de Kleene, synchronisation, flow, et versions quantifiés de ces opérateurs). Un état d’une machine peut être un ASTD quelconque, ce qui donne une approche entièrement compositionnelle pour la spécifications de systèmes complexes. Des actions pouvant modifier des attributs, d’un type quelconque, déclarés localement dans les ASTD permettent de modéliser les données complexes de manière modulaire.

Nous présenterons une extension temporisée des ASTD, qui permet de spécifier des contraintes temporelles sur le comportement des ASTD. Les nouveaux opérateurs temporels sont: Delay, Persistent Delay, Timeout, Persistent Timeout et Timed Interrupt. Ils sont définis avec deux nouveaux opérateurs ASTD (Persistent Guard et Interruption). Ils peuvent être arbitrairement combinés avec les opérateurs existants. L’extension est basée sur une horloge globale qui fait partie de l’état et qui représente l’horloge système. Un évènement particulièr appelé « step » (inspiré de Stateflow) permet de spécifier des transitions dans les machines à états qui sont déclenchées par l’écoulement du temps. L’évènement step est soumis par l’environnement à un ASTD, typiquement à intervalles réguliers suffisamment petits pour respecter la granularité des contraintes de temps visées.

TASTD est supporté par un éditeur graphique eASTD et un compilateur cASTD qui permet de générer un programme C++ implémentant le comportement spécifié dans un TASTD. Le mode simulation permet d’exécuter le programme généré en contrôlant l’écoulement du temps.