Les systèmes distribués sont le plus souvent basés sur l’échange asynchrone de messages entre des agents. La programmation par échanges de messages est largement utilisée en calcul haute performance, en programmation événementielle, dans les architectures orientées service, etc.
Malheureusement du fait de la variété des modèles de communication, des ambiguïtés dans les spécifications, de la portabilité limitée du code, ou encore de la difficulté à exécuter des tests, il est très difficile de vérifier les systèmes communicants.
Le model-checking de systèmes communicants vise à analyser des modèles formels de systèmes distribués et à détecter automatiquement des erreurs comme des pertes de messages ou des inter-blocages. Ces problèmes sont indécidables pour des systèmes à partir de deux machines, et plusieurs hypothèses restrictives ont été étudiées pour rendre les problèmes décidables.
Nous définissons dans cette thèse une nouvelle classe de systèmes : les systèmes réalisables avec des communications synchrones (RSC pour faire court). Les comportements de ces systèmes approximent des comportement synchrones, où les messages sont envoyés et reçus simultanément. Nous nous basons sur cette définition pour étudier la généralisation d’une autre classe de systèmes : les systèmes half-duplex. Un système à deux machines est half-duplex si lorsqu’une machine envoie des messages, l’autre ne peut pas lui en envoyer.
Nous étudions également un autre formalisme, permettant de raisonner sur les systèmes de manière globale : les chorégraphies. Ce formalisme décrit les exécutions de manière synchrone, et un des problèmes qui y est associé est de vérifier si la combinaison des comportements de chaque acteur qui y est décrit est conforme à la description globale. Nous proposons d’utiliser les propriétés des systèmes RSC pour traiter ce problème.