Die Besonderheit der drahtlosen Kommunikation gegenüber den drahtgebundenen Netzwerken liegt im drahtlosen Übertragungsmedium. Aufgrund der Broadcast-Eigenschaft des Übertragungsmediums werden Nachrichten potentiell von allen Netzwerkstationen empfangen, welche sich in der Übertragungsreichweite des Senders aufhalten. Als Konsequenz können bei einem unsynchronisierten Medienzugriff mehrere Nachrichten beim Empfänger kollidieren und nicht korrekt empfangen werden. Dieses Phänomen wird auch als Interferenz bezeichnet. Um solche Interferenzen zu vermeiden, wurden spezielle Protokolle für den Medienzugriff in drahtlosen Netzen entwickelt. Ein solcher Ansatz für drahtlose Maschennetze ist die verteilte Kanalzuweisung. Bei der verteilten Kanalzuweisung werden sich nicht-überlappende Kanäle im verfügbaren Frequenzspektrum für Übertragungen verwendet, die auf dem gleichen Kanal Interferenzen erzeugen würden. Dieser Ansatz ist möglich, da die verwendeten Funktechnologien, wie zum Beispiel IEEE 802.11 (WLAN), mehrere nicht-überlappende Kanäle bereitstellen. Aufgrund der großen Verbreitung von IEEE 802.11, ist eine hohe Dichte von privaten wie kommerziellen Netzen im urbanen Raum die Norm. Diese räumlich überlappenden Netze konkurrieren um den Medienzugriff. Daher ist es für die Leistung von Kanalzuweisungsalgorithmen von großer Bedeutung, die Aktivität der externen Netze mit einzubeziehen. Die Leistung der vorgelegten Arbeit umfasst das Design, die Implementierung und Validierung von Modellen und Algorithmen zur Reduzierung von Interferenzen in drahtlosen Maschennetzen. Die Arbeit beinhaltet die Entwicklung eines Messungs-basierten Interferenzmodells, mit dem Interferenzabhängigkeiten der Maschenrouter untereinander effizient bestimmt werden können. Weiterhin wurde ein Algorithmus für die verteilte Kanalzuweisung entwickelt, der die Aktivität von externen Netzen berücksichtigt. Die Gesamtlösung wurde in einem großen drahtlosen Maschennetz experimentell validiert. / Due to the broadcast nature of the shared medium, wireless transmissions are potentially received by all network stations in the communication range of the sender. With an unsynchronized medium access, multiple transmissions may be active at the same time and thus interfere with each other. In consequence, multiple transmissions may collide at the receiver side and cannot be properly decoded. For this reason, protocols have been developed on the MAC layer to synchronize the medium access and thus reduce interference effects. One of these approaches in wireless mesh networks is channel assignment. The idea of channel assignment is to minimize the network-wide interference by utilizing non-overlapping channels for otherwise interfering wireless transmissions. This is feasible, since wireless mesh routers are usually equipped with multiple radios and commonly used wireless network technologies, such as IEEE 802.11, provide multiple non-overlapping channels. Since IEEE 802.11 operates in the unlicensed frequency spectrum, the dense distribution of private and commercial network deployments of WLANs in urban areas poses a new challenge. Co-located networks compete for the wireless medium, thus decreasing the achievable network performance in terms of throughput and latency. Therefore, an important issue for efficient channel assignment is to also address external interference The contributions of this dissertation comprise the design, implementation, and validation of models and algorithms to enable wireless multi-hop networks to become interference-aware. This includes a measurement-based interference model suitable for large-scale network deployments. A distributed channel assignment algorithm has been developed that considers external sources of interference. The overall solution has been experimentally validated in a large-scale wireless multi-hop multi-radio testbed and has significantly increased the network performance with regard to the network capacity.

Atualmente, muitas redes com características dinâmicas estão em funcionamento (por exemplo MANETs, DTNs, redes oportunistas, etc). Neste trabalho, estudamos um modelo para estas redes chamado de Grafos Evolutivos, que permite expressar a dinamicidade das conexões entre nós por meio de uma simples extensão da estrutura comum de grafos. Esta modelagem é utilizada no arcabouço proposto por Casteigts et al. para definir algoritmos distribuídos em redes dinâmicas, que utiliza grafos evolutivos para representar a topologia da rede e renomeação de rótulos para expressar a comunicação entre os nós. Utilizamos esta abordagem para estudar o problema da exclusão mútua distribuída em redes dinâmicas e diversos algoritmos propostos para ele, a fim de definir e validar suas condições necessárias e suficientes de conectividade em redes dinâmicas. Além da formalização de algoritmos, o modelo de grafos evolutivos também pode ser utilizado para analisar redes dinâmicas. Rastros de redes dinâmicas reais são amplamente utilizados na literatura para estudos de algoritmos pois estes geram resultados mais realísticos do que redes simuladas com padrões de movimento. A partir dos detalhes de cada conexão entre nós de um destes rastros, é possível construir um grafo evolutivo, do qual se pode extrair dados como jornadas ótimas entre nós, variação da conectividade no tempo, estabilidade, e periodicidade. Com as informações mencionadas, um pesquisador pode observar com maior precisão as características do rastro, o que facilita na escolha da rede mais apropriada para sua necessidade. Além disso, o conhecimento prévio de tais características de uma rede auxilia no estudo do comportamento de algoritmos executados sobre ela e provém uma validação para suposições geralmente feitas pelos pesquisadores. Para fornecer estas informações, desenvolvemos uma ferramenta Web que analisa rastros de redes dinâmicas e agrega os dados em um formato de fácil visualização. Descrevemos, neste trabalho, a implementação e a utilidade de todos os serviços da ferramenta. / Lately, several networks with dynamic properties (for instance MANETs, DTNs, opportunistic networks, etc) are functioning. In this work, we studied a model for these networks called Evolving Graphs, which allows the expression of the dynamicity of the conections between nodes through a simple extension of the common graph structure. This model is used by the framework proposed by Casteigts et al. to define distributed algorithms in dynamic networks, which uses evolving graphs to represent the network topology and graph relabelling to express the communication between nodes. Using this approach, we study the distributed mutual exclusion problem in dynamic networks and several algorithms proposed to solve it, in order to define and validate their necessary and sufficient connectivity conditions. Apart from the formalization of algorithms, the evolving graphs model can also be used to analyze dynamic networks. Dynamic network traces are widely used in the literature in order to study algorithms, as they generate better results than simulated networks with movement patterns. From the details of every connection between nodes in a trace, it is possible to build an evolving graph, from which a large amount of information can be extracted, such as optimal journeys between nodes, variation of the conectivity over time, stability and periodicity. With the aforementioned information, a researcher might observe the characteristics of a trace more precisely, which facilitates the process of choosing the most appropriate trace for his needs. Furthermore, the early knowledge of such characteristics of a network helps in the study of the behavior of the algorithms exected over it and provides a validation for the assumptions usually made by the researchers. In order to provide this information, we developed a web tool which analyzes dynamic network traces and aggregates the data in an easily readable format. In this work, we describe the implementation and usefulness of every service in the tool.

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 / Growing diversity of agents in current communication networks and increasing capacitiesof concurrent technologies in the network environment has lead to the considerationof a novel distributed approach of the network management. In this evolvednetwork environment the increasing need for bandwidth and rare channel resources,opposes to reduction of the total energy consumption.This thesis focuses on application of distributed mechanisms and learning methodsto allow for more autonomy in the heterogeneous network, this in order to improveits performances. We are mainly interested in energy efficient stochastic mechanismsthat will operate in a distributed fashion by taking advantage of the computationalcapabilities of all the agents and entities of the network. We rely on application ofGame theory to study different types of complex systems in the distributed wirelessnetworks with dynamic interconnectivity.Specifically, we use the stochastic reinforcement learning tools to address issuessuch as, distributed user-network association that allows achieving an efficient dynamicand decentralized radio resource management. Then, we combine access selectionprocedures with distributed optimization to address the inter-cells interferencescoordination (ICIC) for LTE-advanced networks using dynamic power control and designof fractional frequency reuse mechanisms. Moreover we address in non-hierarchicalnetworks, more precisely in Delay Tolerant Networks (DTNs), decentralized methodsrelated to minimization of the end-to-end communication delay. In this framework weare interested, in addition to Nash equilibrium, to the notion of evolutionary stableequiliria in the different context of Evolutionary Games, Markov Decision EvolutionaryGames and Minority Games. As the major parts of our work includes testing andvalidations by simulations, eventually we present several implementations and integrationsmaterials for edition of simulation platforms and test beds

No description available.

In this thesis, we study the power and limit of algorithms on various models, aiming at applications in distributed networks and databases. In distributed networks, graph algorithms are fundamental to many applications. We focus on computing random walks which are an important primitive employed in a wide range of applications but has always been computed naively. We show that a faster solution exists and subsequently develop faster algorithms by exploiting random walk properties leading to two immediate applications. We also show that this algorithm is optimal. Our technique in proving a lower bound show the first non-trivial connection between communication complexity and lower bounds of distributed graph algorithms. We show that this technique has a wide range of applications by proving new lower bounds of many problems. Some of these lower bounds show that the existing algorithms are tight. In database searching, we think of the database as a large set of multi-dimensional points stored in a disk and want to help the users to quickly find the most desired point. In this thesis, we develop an algorithm that is significantly faster than previous algorithms both theoretically and experimentally. The insight is to solve the problem on the streaming model which helps emphasize the benefits of sequential access over random disk access. We also introduced the randomization technique to the area. The results were complemented with a lower bound. We also initiat a new direction as an attempt to get a better query. We are the first to quantify the output quality using "user satisfaction" which is made possible by borrowing the idea of modeling users by utility functions from game theory and justify our approach through a geometric analysis.

Submitted by Milena Rubi (milenarubi@ufscar.br) on 2017-10-03T18:36:29Z No. of bitstreams: 1 REIS_Vinicius-2017.pdf: 1220818 bytes, checksum: 22e195232fbe4af89ae5ed34520da9b8 (MD5) / Approved for entry into archive by Milena Rubi (milenarubi@ufscar.br) on 2017-10-03T18:36:40Z (GMT) No. of bitstreams: 1 REIS_Vinicius-2017.pdf: 1220818 bytes, checksum: 22e195232fbe4af89ae5ed34520da9b8 (MD5) / Approved for entry into archive by Milena Rubi (milenarubi@ufscar.br) on 2017-10-03T18:36:49Z (GMT) No. of bitstreams: 1 REIS_Vinicius-2017.pdf: 1220818 bytes, checksum: 22e195232fbe4af89ae5ed34520da9b8 (MD5) / Made available in DSpace on 2017-10-03T18:36:56Z (GMT). No. of bitstreams: 1 REIS_Vinicius-2017.pdf: 1220818 bytes, checksum: 22e195232fbe4af89ae5ed34520da9b8 (MD5) Previous issue date: 2017-05-05 / Coordenação de Aperfeiçoamento de Pessoal de Nível Superior (CAPES) / A distributed system is a set of processes and links that is desgined to provide computing power and data persistency, even on the presence of failures. To encapsulate the abstraction of time and to determine which processes have currently failed, these distributed systems are based on unreliable failure detectors, which in its turn are used as a leader election service. Many works are dedicated to analyze the quality of service (QoS) of failure detectors, but a few of them has analyzed the QoS of a leader election algorithm. In this work, we present the NFD-L leader election algorithm, designed to work on crash-recovery distributed systems and to follow the QoS specification defined by Chen, Toueg e Aguilera (2002). We used NFD-L to elect Paxos coordinators for a replication framework and compared the observed QoS for NFD-L with the behavior of the framework native leader election algorithm that is not designed to explicitly meet any QoS requirement. / Um dos objetivos de um sistema distribuído é prover poder computacional e persistência de dados mesmo na presença de falhas de um subconjunto de enlaces e processos. Para determinar quais são os processos falhos deste sistema e abstrair o conceito de tempo, estes sistemas utilizam os serviços de um detector de falhas não confiável, encapsulado em um algoritmo de eleição de líder. Embora a literatura sobre a qualidade de serviço (QoS) oferecida por detectores de falhas seja abundante, ela é escassa quando se trata da QoS oferecida por algoritmos de eleição de líder. Neste trabalho propomos um algoritmo de eleição de líder para o modelo falha-e-recuperação denominado NFD-L, que segue as especificações de QoS originalmente apresentadas por Chen, Toueg e Aguilera (2002). Utilizamos NFD-L em uma aplicação para replicação, como mecanismo de eleição de coordenador para Paxos e apresentamos uma análise da QoS observada, comparando o seu comportamento com um algoritmo de eleição de líder que não foi projetado explicitamente para prover garantias de QoS.

Les récentes avancées technologiques en particulier dans le domaine de la miniaturisation de dispositifs robotiques laissent présager l'émergence de grands ensembles distribués de petits robots qui coopéreront en vue d'accomplir des tâches complexes (e.g., robotique modulaire, robots en essaims, microsystèmes électromécaniques distribués). Ces grands ensembles seront composés d'entités indépendantes, intelligentes et communicantes qui agiront comme un ensemble à part entière. Pour cela, elles s'auto-organiseront et collaboreront en vue d'accomplir des tâches complexes. Ces systèmes présenteront les avantages d'être plus polyvalents et plus robustes que les systèmes robotiques conventionnels tout en affichant un prix réduit. Ces ensembles formeront des systèmes distribués complexes dans lequel chaque entité sera un système embarqué à part entière avec ses propres capacités et ressources toute fois limitées. Coordonner de tels systèmes posent des défis majeurs et ouvrent de nouvelles opportunités dans l'algorithmique distribuée. Je défends la thèse qu'il faut d'ores et déjà identifier et implémenter des algorithmes distribués servant de primitives de base à la coordination de ces ensembles. Dans ce travail, nous nous focalisons sur une classe particulière de robots, à savoir les robots modulaires distribués formant de grands ensembles de modules fortement contraints en ressources (mémoire, calculs, etc.), placés dans une grille régulière et capables de communiquer entre voisins connexes uniquement. J'ai identifié et implémente trois primitives servant à la coordination de ces systèmes, à savoir l'élection d'un nœud central au réseau, la synchronisation temporelle ainsi que l'auto-reconfiguration. Dans ce manuscrit, je propose un ensemble d'algorithmes distribués réalisant ces primitives. J'ai évalué mes algorithmes en utilisant des expériences sur des modules matériels et en simulation sur des systèmes, composés de quelques dizaines à plus d'une dizaine de milliers de modules. Ces expériences montrent que nos algorithmes passent à l'échelle et sont adaptés aux grands ensembles distribués de systèmes embarqués avec des ressources fortement limités à la fois en mémoire et en calcul. / Technological advances especially in the miniaturization of robotic devices foreshadow the emergence of large-scale ensembles of small-size resource-constrained robots that distributively cooperate to achieve complex tasks (e.g., modular self-reconfigurable robots, swarm robotic systems, distributed microelectromechanical systems, etc.). These ensembles are formed from independent, intelligent and communicating units which act as a whole ensemble. These units cooperatively self-organize themselves to achieve common goals. These systems are tought to be more versatile and more robust than conventional robotic systems while having at the same time a lower cost.These ensembles form complex asynchronous distributed systems in which every unit is an embedded system with its own but limited capabilities. Coordination of such large-scale distributed embedded systems poses significant algorithmic issues and open for new opportunities in distributed algorithms. In my thesis, I defend the idea that distributed algorithmic primitives suitable for the coordination of these ensembles should be both identified and designed.In this work, we focus on a specific class of modular robotics systems, namely large-scale distributed modular robotic ensembles composed of resource-constrained modules that are organized in a lattice structure and which can only communicate with neighboring modules. We identified and implemented three building blocks, namely centrality-based leader election, time synchronization and self-reconfiguration.We propose a collection of distributed algorithms to realize these primitives. We evaluate them using both hardware experiments and simulations on systems ranging from a dozen of modules to more than a dozen of thousands of modules. We show that our algorithms scale well and are suitable for large-scale embedded distributed systems with scarce memory and computing resources.

Cette thèse porte sur des aspects structuraux et algorithmiques des graphes. Elle est divisée en deux parties, qui comportent deux études différentes : une partie sur des algorithmes centralisés-séquentiels, et une autre sur des algorithmes distribués. Dans la première partie, on étudie des aspects algorithmiques de deux structures de graphes appelés séparateurs minimaux et cliques maximales potentielles. Ces deux objets sont au coeur d'un méta-théorème dû à Fomin, Todinca and Villanger (SIAM J. Comput. 2015), qui affirme qu'une grande famille des problèmes d'optimisation peut être résolue en temps polynomial, si le graphe d'entrée contient un nombre polynomial de séparateurs minimaux. La contribution de cette partie consiste à prolonger le méta-théorème de Fomin et al. de deux manières : d'un côté, on l'adapte pour qu'il soit valide pour une plus grande famille des problèmes ; de l'autre, on étend ces résultats à des version paramétrées, pour certains paramètres des graphes. La deuxième partie de la thèse correspond à une étude du modèle appelé « Diffusion dans une Clique Congestionnée ». Dans ce modèle, les sommets d'un graphe communiquent entre eux dans des rondes synchrones, en diffusant un message de petite taille, visible par tout autre sommet. L'objectif ici est d'élaborer des protocoles qui reconnaissent des classes de graphes, en minimisant la taille des messages et le nombre de rondes. La contribution de cette partie est l'étude du rôle du hasard dans ce modèle, et la conception de protocoles pour la reconnaissance et la reconstruction des certaines classes des graphes. / This thesis is about structural and algorithmic aspects of graphs. It is divided in two parts, which are about two different studies: one part is about centralized-sequential algorithms, and the other part is about distributed algorithms. In the first part of the thesis we study algorithmic applications of two graph structures called minimal separators and potential maximal cliques. These two objects are in the core of a meta-theorem due to Fomin, Todinca and Villanger (SIAM J. Comput. 2015), which states that a large family of graph optimization problems can be solved in polynomial time, when the input is restricted to the family of graphs with polynomially many minimal separators. The contribution of this part of the thesis is to extend the meta-theorem of Fomin et al. in two ways. On one hand, we adapt it to be valid into a larger family of problems. On the other hand, we extend it into a parameterized version, for several graph parameters. In the second part of this thesis we study the broadcast congested clique model. In this model, the nodes of a graph communicate in synchronous rounds, broadcasting a message of small size visible to every other node. The goal is to design protocols that recognize graph classes minimizing the number of rounds and the message sizes. The contribution of this part is to explore the role of randomness on this model, and provide protocols for the recognition and reconstruction of some graph classes.

En algorithmique distribuée, le modèle asynchrone par envoi de messages et à pannes est connu et utilisé dans de nombreux articles de par son réalisme,par ailleurs il est suffisamment simple pour être utilisé et suffisamment complexe pour représenter des problèmes réels. Dans ce modèle, les n processus communiquent en s'échangeant des messages, mais sans borne sur les délais de communication, c'est-à-dire qu'un message peut mettre un temps arbitrairement long à atteindre sa destination. De plus, jusqu'à f processus peuvent tomber en panne, et ainsi arrêter définitivement de fonctionner. Ces pannes indétectables à cause de l'asynchronisme du système limitent les possibilités de ce modèle. Dans de nombreux cas, les résultats connus dans ces systèmes sont limités à une stricte minorité de pannes. C'est par exemple le cas de l'implémentation de registres atomiques et de la résolution du renommage. Cette barrière de la majorité de pannes, expliquée par le théorème CAP, s'applique à de nombreux problèmes, et fait que le modèle asynchrone par envoi de messages avec une majorité de pannes est peu étudié. Il est donc intéressant d'étudier ce qu'il est possible de faire dans ce cadre.Cette thèse cherche donc à mieux comprendre ce modèle à majorité de pannes, au travers de deux principaux problèmes. Dans un premier temps, on étudie l'implémentation d'objets partagés similaires aux registres habituels, en définissant les bancs de registres x-colorés et les α-registres. Dans un second temps, le problème du renommage est étendu en renommage k-redondant, dans ses versions à-un-coup et réutilisable, et de même pour les objets partagés diviseurs, étendus en k-diviseurs. / In distributed computing, asynchronous message-passing model with crashes is well-known and considered in many articles, because of its realism and it issimple enough to be used and complex enough to represent many real problems.In this model, n processes communicate by exchanging messages, but withoutany bound on communication delays, i.e. a message may take an arbitrarilylong time to reach its destination. Moreover, up to f among the n processesmay crash, and thus definitely stop working. Those crashes are undetectablebecause of the system asynchronism, and restrict the potential results in thismodel.In many cases, known results in those systems must verify the propertyof a strict minority of crashes. For example, this applies to implementationof atomic registers and solving of renaming. This barrier of a majority ofcrashes, explained by the CAP theorem, restricts numerous problems, and theasynchronous message-passing model with a majority of crashes is thus notwell-studied and rather unknown. Hence, studying what can be done in thiscase of a majority of crashes is interesting.This thesis tries to analyse this model, through two main problems. The first part studies the implementation of shared objects, similar to usual registers,by defining x-colored register banks, and α-registers. The second partextends the renaming problem into k-redundant renaming, for both one-shotand long-lived versions, and similarly for the shared objects called splitters intok-splitters.

Dans cette thèse, nous présentons des approches formelles permettant de simplifier la modélisation et la preuve du calcul distribué. Un système distribué est défini par une collection d’entités de calcul autonomes,qui communiquent ensemble pour accomplir une tâche commune. Chaque entité exécute localement son calcul et ne peut interagir qu’avec ses voisins.Le développement et la preuve du calcul distribué est un défi qui nécessite l’utilisation de méthodes et outils avancés. Dans nos travaux de thèse,nous étudions quelques problèmes fondamentaux du distribués, en utilisant Event-B, et nous proposons des schémas de preuve basés sur une approche“correct-par-construction”. Nous considérons un système distribué défini par réseau fiable, de processus anonymes et avec un modèle de communication basé sur l’échange de messages. Dans certains cas, nous faisons abstraction du modèle de communications en utilisant le modèle des calculs locaux. Nous nous focalisons d’abord sur le problème de détection de terminaison du calcul distribué. Nous proposons un patron formel permettant de transformer des algorithmes “avec détection de terminaison locale” en des algorithmes“avec détection de terminaison globale”. Ensuite, nous explicitons les preuves de correction d’un algorithme d’énumération. Nous proposons un développement formel qui servirait de point de départ aux calculs qui nécessitent l’hypothèse d’identification unique des processus. Enfin, nous étudions le problème du snapshot et du calcul d’état global. Nous proposons une solution basée sur une composition d’algorithmes existants. / In this work, we propose formal approaches for modeling andproving distributed algorithms. Such computations are designed to run oninterconnected autonomous computing entities for achieving a common task :each entity executes asynchronously the same code and interacts locally withits immediate neighbors. Correctness of distributed algorithms is a difficulttask and requires advancing methods and tools. In this thesis, we focus onsome basic problems of distributed computing, and we propose Event-B solutionsbased on the ”correct-by-construction” approach. We consider reliablesystems. We also assume that the network is anonymous and processes communicatewith asynchronous messages. In some cases, we refer to local computationsmodel to provide an abstraction of the distributed computations.We propose a formal framework enhancing the termination detection propertyof distributed algorithms. By relying on refinement and composition,we show that an algorithm specified with “local termination detection”, canbe reused in order to compute the same algorithm with “global terminationdetection”. We then focus on the enumeration problem : we start with anabstract initial specification of the problem, and we enrich it gradually bya progressive and incremental refinement. The computed result constitutesbasic initial steps of others distributed algorithms which assume that processeshave unique identifiers. We therefore focus on snapshot problems, andwe propose to investigate how existing algorithms can be composed, withrefinement, in order to compute a global state in an anonymous network.