Quand : Le jeudi 9 février 2023, à 14h00
Où : En salle C06, à Télécom SudParis, 9 rue Charles Fourrier, Evry ou en webconf via le lien suivant https://webconf.imt.fr/frontend/ame-tii-q38-yx8
Titre : TASTD : Diagrammes états-transitions algébriques temporisés
Abstract :
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. Les ASTD permettent de décomposer une spécification complexe en plusieurs composants indépendants, ce qui facilite la modularization et la ré-utilisation.
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.
Short bio :
Marc Frappier est professeur au Département d’informatique de l’Université de Sherbrooke au Québec. Ses intérêts de recherche portent sur les méthodes formelles de développement de logiciels (spécification, conception, raffinement, validation et vérification). Il s’intéresse également à l’ingénierie dirigée par les modèles (i.e., model-driven engineering) et ses applications pour la génération automatique de code, le test du logiciel et la sécurité infomatique (contrôle d’accès, détection d’intrusion, test de vulnérabilité). Il a œuvré durant plus de 5 années en industrie à titre de consultant, analyste senior et gestionnaire de projets pour plusieurs entreprises.