La propension des systèmes informatiques à subir des défaillances matérielles est à l'origine d'une recherche abondante afin de concevoir des systèmes dits tolérants aux pannes. Le procédé couramment retenu consiste à procéder à des réplications, donnant alors naissance à ce que l'on nomme un système distribué. La question se pose alors de savoir si l'on peut garantir que les multiples copies sont cohérentes entre elles. Ainsi, la recherche d'un accord devient-elle un problème à résoudre, à portée paradigmatique : le Consensus. Or, la complexité des algorithmes de Consensus rend la tache ardue : il n'est donc pas rare que l'on commette des erreurs lors de leur conception. De là découle l'idée, développée depuis plus de trente ans, de recourir à des procédés de vérification mécanique des algorithmes et de leurs preuves de correction. Ces procédés prennent place parmi ce que l'on désigne usuellement comme étant des méthodes formelles. C'est à la croisée des recherches en algorithmique distribuée et en méthodes formelles que se situent nos travaux. Plus spécifiquement, il s'agit de faire usage d'un logiciel de certification formelle, Isabelle/HOL, afin de garantir l'exactitude des preuves de correction d'algorithmes de Consensus exprimés dans un cadre formel uniforme du nom de Heard-Of, proposé en 2009 par Charron-Bost et Schiper. Nous montrons que, du fait de leur expression dans un même cadre formel, et du fait de leur proximité, suivant les cas, soit de conception (nombre de rondes, recours à des mécanismes de vote, ...) soit de forme syntaxique, soit d'hypothèses de fonctionnement (synchronisme partiel, ...), ces algorithmes présentent des preuves dont une part conséquente d?arguments sont communs. Cela permet de copier certains d'entre eux d'une preuve à l'autre, afin de réduire l'effort de certification : ces arguments peuvent alors être automatiquement évalués par la machine pour chacun d'entre eux, l'utilisateur n'ayant à intervenir que là où celle-ci est en peine, c'est-à-dire lorsque les différences algorithmiques induisent qu'il faille réviser les détails de l'argumentation. L'exposé que nous faisons de la certification que nous avons effectuée pour six algorithmes distribués dédiés à la résolution du problème du Consensus illustre cette démarche. Par conséquent, nous présentons d'abord les portions communes des démonstrations, puis détaillons ce qui est propre à chacune, l'objectif n'étant pas de permettre une lecture linéaire de chaque démonstration mais de mettre en évidence notre proposition / Computer systems fail. Whatever the reason of these failures, it has been a widespread approach to try and increase the faults-tolerance of a computer system through its replication. The resulting system is said to be a distributed one, in which replicas have to be kept consistent with each others. Hence, reaching agreement, and Consensus in particular, becomes the problem to solve - indeed, the paradigm. Solving Consensus (under various assumptions) is a hard task : algorithms designed on this purpose are subtle and proving their being correct is error-prone - whenever they are, which occasionally appears not to be the case. For more that thirty years, researchers interested in what is called Formal Methods have been working on mechanizing the verification process, in order to increase confidence in the correctness of (distributed) algorithms. The work we present here is at the intersection of distributed algorithms and formal methods. We use the Isabelle/HOL software to certify the correctness proof of various Consensus algorithms expressed in a uniform framework based on the Heard-Of Model, introduced by Charron-Bost and Schiper in 2009. Expressed in a common model, these algorithms, which, depending on the case, share some common mecanisms (number of steps, intermediate votes, ...), some elements of syntax, or types of assumptions (partial synchronism...), can be proved using some common arguments. As a consequence, the certification effort can be reduced by copying some intermediate lemmas from one proof to another and let the computer automatically parse them until some manual adaptation is required. This lead to the idea of certifying the correctness of multiple algorithms all together, instead of proving them one after the other, as one would do on paper in a traditional way. The effort of translation in the formal language of the proof assistant is then possibly reduced. Of course, each proof will also contain specific arguments, which will have to be isolated and translated into the software. Here, we illustrate this proposition through the presentation of formal certificates of correctness for six Consensus algorithms. As a consequence, on should not expect to find here a comprehensive linear presentation of each proof : we first show the arguments shared by multiple proofs, followed by those which are specific to each o them

L'idée directrice de ce travail est de montrer que bon nombre de requêtes peuvent être exprimées comme une navigation dans des graphes.

L'objectif de cette thèse est de produire un environnement permettant de raisonner formellement sur la correction de systèmes de calculs locaux, ainsi que sur l'expressivité de ce modèle de calcul. Pour ce faire, nous utilisons l'assistant de preuve Coq. Notre première contribution est la formalisation en Coq de la sémantique des systèmes de réétiquetage localement engendrés, ou calculs locaux. Un système de calculs locaux est un système de réétiquetage de graphe dont la portée est limitée. Nous proposons donc tout d'abord une implantation succincte de la théorie des graphes en Coq, et utilisons cette dernière pour définir les systèmes de réétiquetage de graphes localement engendrés. Nous avons relevé, dans la définition usuelle des calculs locaux, certaines ambiguïtés. Nous proposons donc une nouvelle définition, et montrons formellement que celle-ci capture toutes les sous-classes d'algorithmes étudiées. Nous esquissons enfin une méthodologie de preuve des systèmes de calculs locaux en Coq.Notre seconde contribution consiste en l'étude formelle de l'expressivité des systèmes de calculs locaux. Nous formalisons un résultat de D. Angluin (repris par la suite par Y. Métivier et J. Chalopin): l'inexistence d'un algorithme d'élection universelle. Nous proposons ensuite deux lemmes originaux concernant les calculs locaux sur les arêtes (ou systèmes LC0), et utilisons ceux-ci pour produire des preuves formelles d'impossibilité pour plusieurs problèmes: calcul du degré de chaque sommet, calcul d'arbre recouvrant, etélection. Nous proposons informellement une nouvelles classes de graphe pour laquelle l'élection est irréalisable par des calculs locaux sur les arêtes.Nous étudions ensuite les transformations de systèmes de calculs locaux et de leur preuves. Nous adaptons le concept de Forward Simulation de N. Lynch aux systèmes de calculs locaux et utilisons ce dernier pour démontrer formellement l'inclusion de deux modes de détection de terminaison dans le cas des systèmes LC0. La preuve de cette inclusion estsimplifiée par l'utilisation de transformations "standards" de systèmes, pour lesquels des résultats génériques ont été démontrés. Finalement, nous réutilisons ces transformations standards pour étudier, en collaboration avec M. Tounsi, deux techniques de composition des systèmes de réétiquetage LC0. Une bibliothèque Coq d'environ 50000 lignes, contenant les preuves formelles des théorèmes présentés dans le mémoire de thèse à été produite en collaboration avec Pierre Castéran (dont environ 40%produit en propre par V. Filou) au cours de cette thèse. / The goal of this work is to build a framework allowing the study, in aformal setting, of the correctness of local computations systems aswell as the expressivity of this model. A local computation system isa set of graph relabelling rules with limited scope, corresponding to a class of distributed algorithms.Our first contribution is the formalisation, in the Coq proofassistant, of a relationnal semantic for local computation systems.This work is based on an original formal graph theory for Coq.Ambiguities inherent to a "pen and paper" definition of local computations are corrected, and we prove that our definition captures all sub-classes of relabelling relations studied in the remainder. We propose a draft of a proof methodology for local computation systems in Coq. Our second contribution is the study of the expressivity of classes of local computations inside our framework. We provide,for instance, a formal proof of D. Angluin results on election and graph coverings. We propose original "meta-theorems" concerningthe LC0 class of local computation, and use these theorem to produce formal impossibility proofs.Finally we study possible transformations of local computation systemsand of their proofs. To this end, we adapt the notion of ForwardSimulation, originally formulated by N. Lynch, to localcomputations. We use this notion to define certified transformationsof LC0 systems. We show how those certified transformation can be useto study the expressivity of certain class of algorithm in ourframework. We define, as certified transformation, two notions ofcomposition for LC0 systems.A Coq library of ~ 50000 lines of code, containing the formal proofs of the theorems presented in the thesis has been produced in collaboration with Pierre Castéran.

Les graphes dynamiques sont un outil de plus en plus utilisé dans des contextes variés où il s'avère nécessaire de modéliser des environnements changeants ou incertains. Les modèles aujourd'hui proposés sont dédiés à ces applications précises. Il n'existe pas de modèle général reprenant, hors de tout contexte applicatif, ces caractéristiques. D'autre part la résolution de problèmes liés à ces environnements dynamiques et incertains est problématique. Nous proposons, ici, la formalisation d'un modèle général de graphe dynamique. <br /><br />Nous étudions la résolution de problèmes dans ces graphes à l'aide de méthodes inspirées de mécanismes d'intelligence collective. <br /><br />Les modèles proposés sont validés dans le contexte applicatif des réseaux mobiles ad hoc. Une approche originale de construction et de maintien de chemins de communication sous plusieurs contraintes est proposée. Le problème de la construction et du maintien d'une forêt couvrante dans un réseau mobile ad hoc est également étudié.

Dans le contexte des réseaux à grande échelle, la prise en compte des pannes est une nécessité évidente. Ce document s'intéresse à l'approche auto-stabilisante qui vise à concevoir des algorithmes se ''réparant d'eux-même ' en cas de fautes transitoires, c'est-à-dire de pannes impliquant la modification arbitraire de l'état des processus. Il se focalise sur deux contextes différents, couvrant la majeure partie de mes travaux de recherche ces dernières années. La première partie du document est consacrée à l'algorithmique auto-stabilisante pour les réseaux de processus. La seconde partie du document est consacrée quant à elle à l'algorithmique auto-stabilisante pour des entités autonomes (agents logiciels, robots, etc.) se déplaçant dans un réseau.

Les réseaux mobiles ad hoc sont par nature instables et imprévisibles. De ces caractéristiques découle la difficulté à concevoir et analyser des algorithmes distribués garantissant certaines propriétés. C'est sur ce point que porte la contribution majeure de cette thèse. Pour amorcer cette étude, nous avons étudié quelques problèmes fondamentaux de l'algorithmique distribuée dans ce type d'environnement. Du fait de la nature de ces réseaux, nous avons considéré des modèles de calculs locaux, où chaque étape ne fait collaborer que des n\oe uds directement voisins. Nous avons notamment proposé un nouveau cadre d'analyse, combinant réétiquetages de graphes dynamiques et graphes évolutifs (modèle combinatoire pour les réseaux dynamiques). Notre approche permet de caractériser les conditions de succès ou d'échec d'un algorithme en fonction de la dynamique du réseau, autrement dit, en fonction de conditions nécessaires et/ou suffisantes sur les graphes évolutifs correspondants. Nous avons également étudié la synchronisation sous-jacente aux calculs, ainsi que la manière dont une application réelle peut reposer sur un algorithme de réétiquetage. Un certain nombre de logiciels ont également été réalisés autour de ces travaux, notamment un simulateur de réétiquetage de graphes dynamiques et un vérificateur de propriétés sur les graphes évolutifs.

La diversité croissante des différents agents constituant les réseaux de communication actuels ainsi que la capacité accrue des technologies concurrentes dans l'environnement réseau a conduit à la prise en compte d'une nouvelle approche distribuée de la gestion du réseau. Dans cet environnement réseau évolué, le besoin en accroissement de la bande passante et en ressources rares, s'oppose à la réduction de la consommation énergétique globale.Dans notre travail nous nous intéressons à l'application de mécanismes distribués et de méthodes d'apprentissages visant à introduire d'avantage d'autonomie dans les réseaux hétérogènes, mobiles en particulier, tout en améliorant les performances par rapport aux débits et à la qualité de service. Notre étude se concentre principalement sur l'élaboration de mécanismes distribués stochastiques et énergétiquement efficaces en profitant des capacités de calcul de tous les agents et entités du réseau. Divers outils de la théorie des jeux nous permettent de modéliser et d'étudier différents types de systèmes dont la complexité est induite par la grande taille, l'hétérogénéité et le caractère dynamique des interconnexions. Plus spécifiquement, nous utilisons des outils d'apprentissage par renforcement pour aborder des questions telles que l'attachement distribué des utilisateurs permettant une gestion dynamique, décentralisée et efficace des ressources radio. Nous combinons ensuite les procédures de sélection d'accès à des méthodes d'optimisation distribuées du type gradient stochastique, pour adresser le problème de coordination des interférences intercellulaires (ICIC) dans les réseaux LTE-A. Cette approche se base sur un contrôle de puissance dynamique conduisant à une réutilisation fractionnaire des fréquences radios. Par ailleurs nous adressons dans les réseaux décentralisés non-hiérarchiques, plus précisément les réseaux tolérants aux délais (DTNs), des méthodes décentralisées liées à la minimisation du délai de transmission de bout en bout. Dans ce cadre nous nous intéressons, en outre des équilibres de Nash, à la notion d'équilibre évolutionnairement stables dans différents contextes de jeux évolutionnaires, jeux évolutionnaires décisionnels markoviens et jeux de minorité. Enfin, la majeure partie du travail effectué se rattachant aux tests et validations par simulations,nous présentons plusieurs éléments d'implémentations et d'intégrations liés à la mise en place de plateformes de simulations et d'expérimentations.

Les graphes, outil mathématique pour modéliser les relations entre des entités, sont en augmentation constante du fait d'internet (par exemple les réseaux sociaux). La visualisation de graphe (aussi appelée dessin) permet d'obtenir immédiatement des informations sur le graphe. Les graphes issus d'internet sont généralement stockés de manière morcelée sur plusieurs machines connectées par un réseau. Cette thèse a pour but de développer des algorithmes de dessin de très grand graphes dans le paradigme MapReduce, utilisé pour le calcul sur cluster. Parmi les algorithmes de dessin, les algorithmes reposants sur un modèle physique sous-jacent pour réaliser le dessin permettent d'obtenir un bon dessin indépendamment de la nature du graphe. Nous proposons deux algorithmes par modèle de forces conçus dans le paradigme MapReduce. GDAD, le premier algorithme par modèle de force dans le paradigme MapReduce, utilise des pivots pour simplifier le calcul des interactions entre les nœuds du graphes. MuGDAD, le prolongement de GDAD, utilise une simplification récursive du graphe pour effectuer le dessin, toujours à l'aide de pivots. Nous comparons ces deux algorithmes avec les algorithmes de l'état de l'art pour évaluer leurs performances. / Graphs, usually used to model relations between entities, are continually growing mainly because of the internet (social networks for example). Graph visualization (also called drawing) is a fast way of collecting data about a graph. Internet graphs are often stored in a distributed manner, split between several machines interconnected. This thesis aims to develop drawing algorithms to draw very large graphs using the MapReduce paradigm, used for cluster computing. Among graph drawing algorithms, those which rely on a physical model to compute the node placement are generally considered to draw graphs well regardless of the type of graph. We developped two force-directed graph drawing algorithms in the MapReduce paradigm. GDAD, the fist distributed force-directed graph drawing algorithm ever, uses pivots to simplify computations of node interactions. MuGDAD, following GDAD, uses a recursive simplification to draw the original graph, keeping the pivots. We compare these two algorithms with the state of the art to assess their performances.

Les systèmes à grande échelle comme les Grilles ou les Nuages (Clouds) mettent à disposition pour les utilisateurs des ressources informatiques hétérogènes. Dans les Nuages, les accès aux ressources sont orchestrés par des contrats permettant de définir un niveau de qualité de service (temps de réponse, disponibilité ...) que le fournisseur doit respecter. Ma thèse a donc contribué à concevoir de nouveaux algorithmes distribués de verrouillage de ressources dans les systèmes large échelle en prenant en compte des notions de qualité de service. Dans un premier temps, mes travaux de thèse se portent sur des algorithmes distribués de verrouillage ayant des contraintes en termes de priorités et de temps. Deux algorithmes d'exclusion mutuelle ont été proposés : un algorithme prenant en compte les priorités des clients et un autre pour des requêtes avec des dates d'échéance. Dans un second temps, j'ai abordé le problème de l'exclusion mutuelle généralisée pour allouer de manière exclusive plusieurs types de ressources hétérogènes. J'ai proposé un nouvel algorithme qui réduit les coûts de synchronisation en limitant la communication entre processus non conflictuels. Tous ces algorithmes ont été implémentés et évalués sur la plateforme nationale Grid 5000. Les évaluations ont montré que nos algorithmes satisfaisaient bien les contraintes applicatives tout en améliorant de manière significative les performances en termes de taux d'utilisation et de temps de réponse. / Distributed large-scale systems such as Grids or Clouds provide large amounts of heterogeneous computing resources. Clouds manage ressource access by contracts that allow to define a quality of service (response time, availability, ...) that the provider has to respect. My thesis focuses on designing new distributed locking algorithms for large scale systems that integrate notions of quality of service. At first, my thesis targets distributed locking algorithms with constraints in terms of priorities and response time. Two mutual exclusion algorithms are proposed: a first algorithm takes into account client-defined priorities and a second one associates requests with deadlines. I then move on to a generalized mutual exclusion problem in order to allocate several types of heterogeneous resources in a exclusive way. I propose a new algorithm that reduces the cost of synchronization by limiting communication between non-conflicting processes.All algorithms have been implemented and evaluated over the national platform Grid 5000. Evaluations show that our algorithms satisfy applicative constraints while improving performance significatively in terms of resources use rate and response time.

Le projet scientifique dans lequel s’inscrit ma thèse a pour objectif l’élaboration d’algorithmes distribués et efficaces pour les réseaux informatiques. Ce projet vise une catégorie particulière des algorithmes distribués, dits auto-stabilisants. Il s’agit d’algorithmes ayant pour propriété de retrouver un comportement correct suite à une panne dans le réseau et ce, sans aucune intervention humaine. Le travail effectué en collaboration avec mes directeurs de thèse s’est concentré, plus précisément, autour des problèmes de couplage, de cliques et des paradigmes de publications-souscriptions dans ce domaine de l’informatique théorique. Dans un premier temps on a traité le problème du couplage maximal dans sa version anonyme, en fournissant un algorithme auto-stabilisant probabiliste et efficace. Ces travaux sont parus dans le journal PPL. De plus, on s’est intéressé au problème du couplage dans sa version maximum identifiée. Son travail améliore le dernier algorithme présent dans la littérature pour l’approximation de ce type de couplage au 2/3 de la solution optimale. Ces travaux sont parus dans une conférence internationale OPODIS. Par ailleurs, j'ai eu l’opportunité de collaborer en Allemagne avec Prof. Volker Turau au sein du groupe de télématique de l’Université technique de Hambourg. Le cadre de cette collaboration a été les algorithmes auto-stabilisants pour les paradigmes de publication-souscription. Cela a abouti à un algorithme efficace pour la version en canal de ce problème, introduisant la notion de raccourci pour le routage de messages dans ces paradigmes. Les résultats ont fait l’objet d’un Brief Announcement et d’un papier, publiés dans des conférences internationales, SSS et NetSyS. J'ai aussi bénéficié d’une collaboration avec Mr. Gerry Siegemund qui a été accueilli au laboratoire d’Informatique de l’École Polytechnique. Il a été question de trouver un algorithme efficace et auto-stabilisant pour la partition d’un réseau en cliques. Cette collaboration a eu pour résultat un algorithme pour le problème améliorant le dernier en date. Ce résultat est en cours de rédaction pour soumission à une conférence internationale. / The main focus of my thesis is the design of an efficient kind of distributed algorithms, known as: Self-stabilizing. These algorithms have the property to recover from faults in the environment they're executed in, and this without any human intervention. Recovering here, means converging toward a pre-defined, correct configuration. In this setting, I was mainly interested by the problems of matching in graphs, clique partitions and publication subscription paradigms. For the maximal version of the matching problem in anonymous graphs, we achieved a more efficient randomized, self-stabilizing algorithm. This work is published in a journal version in PPL. The maximum version of the same problem, but in an identified setting, led to the design of an efficient self-stabilizing algorithm that approximates the optimal solution up to the 2/3. This result was published at OPODIS. During a research visit at TUHH, Hamburg, Germany. Together with Pr. Volker Turau we tackled the problem of self-stabilizing publish/subscribe paradigms. This led to an algorithm introducing the new notion of short-cuts in this type of structures and was published under a brief announcement and a regular paper at SSS and NetSyS. In collaboration with Mr. Siegemund, then a visiting researcher at LIX, École Polytechnique, we worked on an efficient self-stabilizing algorithm for clique partitions. This work is still in progress and in preparation for an eventual publication.