Modélisation et validation des algorithmes non-déterministes de synchronisation des horloges

This thesis addresses the problem of analyzing and designing non-deterministic clock synchronization algorithms in distributed systems. Non-deterministic algorithms are a promising solution to the clock synchronization problem, which can be testified by the attention they have received in recent years. Non-determinist dock synchronization algorithms use statistical or probabilistic techniques and they allow a better precision than with deterministic ones; the price to pay is a small probability that the system will fail to synchronize to the desired precision. This probability of failure can be made as small as desired by sending a sufficiently large number of messages. Unfortunately, assessing different algorithms is a difficult task, especially because we lack a common ground to establish comparisons. We propose an analytical model for the behaviour of non-deterministic dock synchronization algorithms. The aim is to find an expression that the distributed systems designer can use to estimate the required number of messages, in order to guarantee that a certain algorithm will synchronize to the desired precision and probability of success. This result is a Sufficient Condition for Synchronization, which states the conditions that must be fulfilled in order to guarantee the desired precision and probability of success. This condition is based on local parameters and on system parameters that are easily computed, such as the number of sites and the description of the delay as a random variable. The underlying assumptions are experimentally verified. For this purpose, we developed a test-bed based on the Controller Area Network. The results validate the assumptions used for the model.Cette thèse traite le problème d'analyse et de conception des algorithmes de synchronisation non déterministes dans les systèmes répartis. Les algorithmes non-déterministes constituent une solution intéressante pour le problème de la synchronisation des horloges, ce qui est témoigné par l'intérêt qui leur a été porté pendant les dernières années. Les algorithmes de synchronisation non-déterministes utilisent des techniques statistiques ou probabilistes et permettent d'obtenir une meilleure précision par rapport aux algorithmes déterministes, le prix à payer étant la probabilité que le système ne réussisse pas à se synchroniser avec la précision souhaitée. Cette probabilité d'échec tend vers zéro avec le nombre de messages échangés et elle peut être réduite à une valeur aussi petite qu'on le souhaite avec un nombre de messages suffisamment grand. Malheureusement, l'évaluation des différentes propositions publiées dans la littérature est difficile, principalement à cause de l'inexistence d'une base commune pour établir les comparaisons. Nous proposons un modèle analytique pour le fonctionnement des algorithmes de synchronisation non-déterministes. Le but est de trouver une expression que le concepteur d'un système distribué puisse utiliser pour calculer le nombre de messages requis pour un certain algorithme, de façon à fournir la synchronisation avec la précision et la probabilité spécifiées. Ce résultat est la Condition de Garantie de Synchronisation, qui définit une condition suffisante qui garantit le succès de la synchronisation non-déterministe sous les conditions spécifiées. Cette condition est établie à partir de paramètres locaux d'un site et de paramètres du système qui sont facilement calculables, tels que le nombre de sites et les paramètres qui décrivent le délai comme une variable aléatoire. Les conditions sous-jacentes au modèle proposé sont vérifiées expérimentalement à l'aide d'une plate-forme basée sur le réseau CAN que nous avons développée. Le test des algorithmes sur cette plate-forme a permis de vérifier la validité des hypothèses qui sont associées au modèle