Procédures de réduction pour les systèmes à base d'automates communicants (formalisation et mise en oeuvre)

Ce travail porte sur la formalisation de l'exécution symbolique de systèmes à base d'automates communicants et sa mise en oeuvre algorithmique en proposant des méthodes de réduction de l'espace des états atteignables préservant les équivalences usuelles. Nous avons proposé une formalisation des systèmes communicants dans un cadre très général inspiré par les graphes de transitions symboliques avec affectations (ou STGA). Nous en avons isolé une sous-classe particulière de ces derniers, que nous avons appelé STGA paramétrés (ou P-STGA) et établi en théorème de représentation de tout graphe dans cette sous classe via une relation de bisimulation forte. La démonstration de ce théorème nous a permis d'introduire l'exécution symbolique comme étant un moyen permettant de construire un représentant d'un STGA donné dans la classe des P-STGA qui sont des modèles du graphe de ses états atteignables. Lors de la mise en oeuvre algorithmique de l'exécution symbolique, pour faire face au problème d'explosion combinatoire de l'espace des états atteignables nous avons proposé des méthodes de réduction préservant les relations de bisimulation forte ou simple entre le STGA et son représentant dans la classe des P-STGA. Ses méthodes ont été implémentées avec succès dans le cadre d'une plate-forme de génération automatique de tests pour des spécifications formelles.This work deals with formalization of symbolic execution of systems based on concurrency automaton and his algorithmic implementation while proposing reduction methods for the graph of reachable states preserving the ordinary equivalences. We proposed a formalization of the communicating systems in a very general framework inspired by the symbolic transition graph with assignment, denoted by STGA. We some isolated an special part of the class of STGAs that we called parameterize STGA or P-STGA, and established a representative theorem of all graphs in this under classifies using a strong bisimulation relation. The proof of this theorem allowed us to introduce the symbolic execution as being a means building a representative of a given STGA in the class of the P-STGA which were models for his graph of reachable states. At the time of the algorithmic implementation of symbolic execution, reduction methods preserving the relations of strong or simple bisimulation between the STGA and his representative in the class of P-STGAs were proposed to limit the growth of the space of reachable states. Its methods were implemented with successes in an automatic tests generation tool for formals specifications.ORSAY-PARIS 11-BU Sciences (914712101) / SudocSudocFranceF