Étude et implémentation d'une méthode de transformation des automates temporisés en automates à états finis

Abstract

Les systèmes à événements discrets (SED) sont des systèmes dont le fonctionnement se traduit par des séquences d'interactions.Les SED peuvent être décrits par leurs séquences possibles d'interactions ou événements. Un SED temps-réel est un SED dont le bon fonctionnement dépend non seulement de comment il interagit avec son environnement mais aussi à quels moments ces interactions se produisent. Le modèle automate temporisé (AT) permet de modéliser convenablement les SED temps-réel.Les ATs, qui utilisent un modèle continu du temps, induisent un espace d'états infini pour le système modélisé. Le modèle d'automates à états finis (AEF) par contre permet de représenter de manière finie l'espace des états d'un SED.Les AEFs se prêtent mieux à l'étude (analyse, test, conception, contrôle...) par des méthodes formelles des SED. Une approche standard pour l'étude des SED temps-réel consiste alors à transformer l'AT modélisant le SED en un AEF équivalent sur lequel on réalise l'étude. Dans ce projet, il s'agissait pour nous d'apporter notre contribution à l'élaboration d'une nouvelle méthode de transformation d'un AT en un AEF équivalent.--Résumé abrégé par UMI.