Synthèse des systèmes réactifs : une approche formelle

Plusieurs travaux visant la description du comportement externe d'un système ont été inspiré du modèle de machines d'états finis. Un des nombreux exemples dans la littérature est celui des systèmes réactifs. Les systèmes réactifs sont des systèmes informatiques qui réagissent à des entrées provenant de façon répétitive de l'environnement en produisant eux-mêmes des sorties vers cet environnement. Le but principal de ce travail est de développer une base formelle pour la conception fiable et de haut niveau des systèmes réactifs. Cette base permet d'exprimer ces systèmes à partir des contraintes comportementales, en se servant de ses spécifications formelles à un niveau supérieur. Ces contraintes font état d'un comportement désirable d'un système inconnu en définissant son périmètre. Dans ce mémoire, nous présentons une méthode à la fois simple et efficace faisant preuve d'une méthode de synthèse d'une spécification formelle qui met l'accent sur les propriétés comportementales générales d'un système. Plus précisément, notre objectif est de traduire une spécification de haut niveau en spécification plus détaillée; ce passage montre une description opérationnelle explicite d'un système. L'algorithme de synthèse, développé ici, construit en premier un système à transitions d'états étiqueté du système réactif à développer puis produit la spécification du comportement de ce système. Il est basé sur les concepts formels de simulation des systèmes et de relations de priorités qui préviennent l'utilisateur de l'introduction de transitions indésirables dans un système qui réalise un fonctionnement particulier. Cette approche de synthèse est illustrée à l'aide d'exemples rencontrés dans la littérature