Vérification et Spécification des Systèmes Distribués

The framework of this work is the automatic verification of distributed systems. One first studies the specification problem for such systems, which consists in defining a logical formalism to describe properties of system behaviors. It should be easy to express usual system properties (such as reachability, safety, mutual exclusion, liveness, etc.). Verification algorithms for these properties should also be easy. One thus has to find a compromise between expressiveness and ease of use. In the second part, we look at the modeling problem for concurrent systems, again looking for a compromise between realism of models and ease of verification. The models studied in this work are asynchronous automata, which represent concurrent processes communicating by shared memory. The thesis finally tackles the controller synthesis problem. Given an incompletely specified system (which is hence non-deterministic) interacting with an environment, we want to automatically compute how to restrict its behavior so that it meets a given specification, no matter the environment behaves. This problem can be formulated in terms of games. In the distributed case, these games involve several players. This usually leads to undecidability for the existence of a controller. This thesis shows that some properties of the communication architecture guarantee decidability for any regular specification.Cette thèse se place dans le cadre de la vérification automatique des systèmes distribués. Elle aborde le problème de la spécification pour de tels systèmes, qui consiste à définir un formalisme logique pour décrire des propriétés des comportements de systèmes. On en attend qu'il soit facile d'exprimer les propriétés courantes (accessibilité, sûreté, exclusion mutuelle, vivacité, etc.). On souhaite par ailleurs que la vérification de ces propriétés soient aisée. Il s'agit donc de trouver un compromis entre pouvoir d'expression et simplicité d'utilisation.On s'intéresse ensuite à la modélisation des systèmes concurrents, en recherchant à nouveau un compromis entre réalisme des modèles et facilité de vérification. Les modèles étudiés dans ce travail sont les automates asynchrones, qui modélisent des processus concurrents communiquant par mémoire partagée.La thèse s'intéresse enfin au problème de la synthèse de contrôleur. Étant donné un système spécifié de façon incomplète, donc non-déterministe, en interaction avec un environnement, il s'agit de calculer de manière automatique comment restreindre son comportement afin qu'il vérifie une spécification donnée (quelles que soient les actions de l'environnement). Ce problème se formule entermes de jeux. Dans le cas distribué, les jeux ont naturellement plusieurs joueurs. Dans ce cadre, la plupart des résultats sont négatifs : il est indécidable de savoir si on peut ou non contrôler un tel système. Cette thèse prouve que certaines propriétés de l'architecture de communication garantissent décidabilité pour toute spécification régulière