Synchronizability for distributed systems

Les systèmes distribués sont omniprésents, cependant leur implémentation est complexe et sujette aux erreurs. Pour les vérifier, ils peuvent être modélisés en système d’automates communicants, où chaque automate représente le comportement d'un élément du système. Les propriétés liées à la vérification, telles que le problème de l'accessibilité, restent indécidables dans un tel modèle. En effet, un système d’automates communiquant de façon asynchrone est Turing équivalent. C’est pourquoi l'utilisation d'approximations est donc nécessaire. La k-synchronisabilité est l’une de ces approximations. Un système est k-synchronisable si pour toute exécution, il existe une exécution équivalente pouvant être divisée en phases, appelées k-échanges, contenant k messages. Dans cette thèse, nous nous intéressons à l'analyse des systèmes k-synchronisables : nous montrons que le problème de l’accessibilité est décidable et nous nous interrogeons sur la k-synchronisabilité d’un système donné. Pour ce deuxième point, nous regardons le cas où un k est passé en paramètre, et le cas où il faut trouver le k tel que le système est k- synchronisable. Nous prouvons que ces deux problèmes sont décidables lorsque le système communique en boîte aux lettres. Le premier problème est également décidable en pair-à-pair, mais, avec ce type de communication, le deuxième problème reste ouvert. Nous complétons cette étude en identifiant certaines implications contre-intuitives de la notion de k-synchronisabilité, celles-ci nous ont poussés à définir des variantes de la k-synchronisabilité. Une étude comparative de différentes classes de systèmes, soit étudiées ou définies dans cette thèse, soit provenant de la littérature, conclut nos travaux.Distributed systems are ubiquitous and their implementation is complex and error-prone. In order to check for errors, they can be modeled as systems of communicating automata, where each automaton represents the behavior of an element of the system. Verification problems such as reachability are undecidable in such a model. Indeed, a system of communicating automata is Turing-equivalent. For that, the use of approximations is necessary. k-synchronizability is one of these techniques. A system is k-synchronizable if, for all execution, there is an equivalent execution that can be divided into phases containing k messages. These phases are called k-exchanges. In this thesis, we analyse k-synchronizable systems: we show that reachability is decidable and we are interested in the membership problem, that is: given a system, decide whether it is k-synchronizable. We study both the case where k is an input of the problem, and the case where we have to guess the k such that the system is k-synchronizable. We study them according to the type of communication of the system. Either the system is in mailbox and so each process has only one buffer to store all received messages, or the system is in peer-to-peer, and each process has a buffer for each sender. Both problems are decidable when the system is communicating in mailbox. When the system is communicating in peer-to-peer, the first one is decidable and the second remains open. Finally, we point out some counter-intuitive cases of k-synchronizable systems that lead us to propose some variations to the definition of k-synchronizability. A comparative study of the state-of-art classes of systems and our new classes concludes our work