Les réseaux de capteurs sans fil (RCSFs) déterminent un axe de recherche en plein essor, puisqu’ils sont utilisés aujourd’hui dans de nombreuses applications qui diffèrent par leurs objectifs et leurs contraintes individuelles.Toutefois, le dénominateur commun de toutes les applications de réseaux de capteurs reste la vulnérabilité des nœuds capteurs en raison de leurs caractéristiques et aussi de la nature des données générées.En effet, les RCSFs génèrent une grande masse de données en continue à des vitesses élevées, hétérogènes et provenant d’emplacements répartis. Par ailleurs, la nécessité de traiter et d’extraire des connaissances à partir de ces grandes quantités de données nous ont motivé à explorer l’une des techniques conçues pour traiter efficacement ces ensembles de données et fournir leurs modèles de représentation. Cependant, parmi les techniques utilisées pour la gestion des données, nous pouvons utiliser les techniques de Data mining. Néanmoins, ces méthodes ne sont pas directement applicables aux RCSFs à cause des contraintes des noeuds capteurs. Il faut donc répondre à un double objectif : l’efficacité d’une solution tout en offrant une bonne adaptation des méthodes de Data mining classiques pour l’analyse de grosses masses de données des RCSFs en prenant en compte les contraintes des noeuds capteurs, et aussi l’extraction du maximum de connaissances afin de prendre des décisions meilleures. Les contributions de cette thèse portent principalement sur l’étude de plusieurs algorithmes distribués qui répondent à la nature des données et aux contraintes de ressources des noeuds capteurs en se basant sur les techniques de Data mining. Chaque noeud favorise un traitement local des techniques de Data mining et ensuite échange ses informations avec ses voisins, pour parvenir à un consensus sur un modèle global. Les différents résultats obtenus montrent que les approches proposées réduisent considérablement la consommation d’énergie et les coûts de consommation, ce qui étend la durée de vie du réseau.Les résultats obtenus indiquent aussi que les approches proposées sont extrêmement efficaces en termes de calcul du modèle, de latence, de réduction de la taille des données, d’adaptabilité et de détection des événements. / Recently, Wireless Sensor Networks (WSNs) have emerged as one of the most exciting fields. However, the common challenge of all sensor network applications remains the vulnerability of sensor nodes due to their characteristics and also the nature of the data generated which are of large volume, heterogeneous, and distributed. On the other hand, the need to process and extract knowledge from these large quantities of data motivated us to explore Data mining techniques and develop new approaches to improve the detection accuracy, the quality of information, the reduction of data size, and the extraction of knowledge from WSN datasets to help decision making. However, the classical Data mining methods are not directly applicable to WSNs due to their constraints.It is therefore necessary to satisfy the following objectives: an efficient solution offering a good adaptation of Data mining methods to the analysis of huge and continuously arriving data from WSNs, by taking into account the constraints of the sensor nodes which allows to extract knowledge in order to make better decisions. The contributions of this thesis focus mainly on the study of several distributed algorithms which can deal with the nature of sensed data and the resource constraints of sensor nodes based on the Data mining algorithms by first using the local computation at each node and then exchange messages with its neighbors, in order to reach consensus on a global model. The different results obtained show that the proposed approaches reduce the energy consumption and the communication cost considerably which extends the network lifetime.The results also indicate that the proposed approaches are extremely efficient in terms of model computation, latency, reduction of data size, adaptability, and event detection.

Les systèmes distribués sont de plus en plus grands et complexes, alors que leur utilisation s'étend à de nombreux domaines (par exemple, les communications, la domotique, la surveillance, le ``cloud''). Par conséquent, les contextes d'exécution des systèmes distribués sont très divers. Dans cette thèse, nous nous focalisons sur des contextes incertains, autrement dit, le contexte n'est pas complètement connu au départ ou il est changeant. Plus précisément, nous nous focalisons sur deux principaux types d'incertitudes : une identification incomplète des processus et la présence de fautes. L'absence d'identification est fréquente dans de grands réseaux composés d'appareils produits et déployés en masse. De plus, l'anonymat est souvent une demande pour la sécurité et la confidentialité. De la même façon, les grands réseaux sont exposés aux pannes comme la panne définitive d'un processus ou une perte de connexion sans fil. Néanmoins, le service fourni doit rester disponible.Cette thèse est composée de quatre contributions principales. Premièrement, nous étudions le problème de l'élection de leader dans les anneaux unidirectionnels de processus homonymes (les processus sont identifiés mais leur ID n'est pas forcément unique). Par la suite, nous proposons un algorithme d'élection de leader silencieux et autostabilisant pour tout réseau connecté. Il s'agit du premier algorithme fonctionnant sous de telles conditions qui stabilise en un nombre polynomial de pas de calcul. La troisième contribution est une nouvelle propriété de stabilisation conçue pour les réseaux dynamiques qui garantit des convergences rapides et progressives après des changements topologiques. Nous illustrons cette propriété avec un algorithme de synchronisation d'horloges. Finalement, nous considérons la question de la concurrence dans les problèmes d'allocation de ressources. En particulier, nous étudions le niveau de concurrence qui peut être atteint dans une grande classe de problèmes d'allocation de ressources, l'allocation de ressources locales. / Distributed systems become increasingly wide and complex, while their usage extends to various domains (e.g., communication, home automation, monitoring, cloud computing). Thus, distributed systems are executed in diverse contexts. In this thesis, we focus on uncertain contexts, i.e., the context is not completely known a priori or is unsettled. More precisely, we consider two main kinds of uncertainty: processes that are not completely identified and the presence of faults. The absence of identification is frequent in large networks composed of massively produced and deployed devices. In addition, anonymity is often required for security and privacy. Similarly, large networks are exposed to faults (e.g, process crashes, wireless connection drop), but the service must remain available.This thesis is composed of four main contributions. First, we study the leader election problem in unidirectional rings of homonym processes, i.e., processes are identified but their ID is not necessarily unique. Then, we propose a silent self-stabilizing leader election algorithm for arbitrary connected network. This is the first algorithm under such conditions that stabilizes in a polynomial number of steps. The third contribution is a new stabilizing property designed for dynamic networks that ensures fast and gradual convergences after topological changes. We illustrate this property with a clock synchronizing algorithm. Finally, we consider the issue of concurrency in resource allocation problems. In particular, we study the level of concurrency that can be achieved in a wide class of resource allocation problem, i.e., the local resource allocation.

Les microrobots MEMS sont des éléments miniaturisés qui peuvent capter et agir sur l'environnement. Leur taille est de l'ordre du millimètre et ils ont une faible capacité de mémoire et une capacité énergétique limitée. Les microrobots MEMS continuent d'accroître leur présence dans notre vie quotidienne. En effet, ils peuvent effectuer plusieurs missions et tâches dans une large gamme d'applications telles que la localisation d'odeur, la lutte contre les incendies, le service médical, la surveillance, le sauvetage et la sécurité. Pour faire ces taches et missions, ils doivent appliquer des protocoles de redéploiement afin de s'adapter aux conditions du travail. Ces algorithmes doivent être efficaces, évolutifs, robustes et ils doivent utiliser de préférence des informations locales. Le redéploiement pour les microrobots MEMS mobiles nécessite actuellement un système de positionnement et une carte (positions prédéfinies) de la forme cible. La solution traditionnelle de positionnement comme l'utilisation d'un GPS consommerait trop d'énergie. De plus, l'utilisation de solutions de positionnement algorithmique avec les techniques de multilatération pose toujours des problèmes à cause des erreurs dans les coordonnées obtenues.Dans la littérature, si nous voulons une auto-reconfiguration de microrobots vers une forme cible constituée de P positions, chaque microrobot doit avoir une capacité mémoire de P positions pour les sauvegarder. Par conséquent, si P est de l'ordre de milliers ou de millions, chaque noeud devra avoir une capacité de mémoire de positions en milliers ou millions. Parconséquent, ces algorithmes ne sont pas extensibles ou évolutifs. Dans cette thèse, on propose des protocoles de reconfiguration où les noeuds ne sont pas conscients de leurs positions dans le plan et n'enregistrent aucune position de la forme cible. En d'autres termes, les noeuds ne stockent pas au départ les coordonnées qui construisent la forme cible. Par conséquent, l'utilisation de mémoire pour chaque noeud est réduite à une complexité constante. L'objectif desalgorithmes distribués proposés est d'optimiser la topologie logique du réseau des microrobots afin de chercher une meilleure complexité pour l'échange de message et une communication peu coûteuse. Ces solutions sont complètement distribués. On montre pour la reconfiguration d'une chaîne à un carré comment gérer la dynamicité du réseau pour sauvegarder l'énergie, on étudie comment utiliser le parallélisme de mouvements pour optimiser le temps d'exécution et lenombre de mouvements. Ainsi, on propose une autre solution où la topologie physique initiale peut être n'importe quelle configuration initiale. Avec ces solutions, les noeuds peuvent exécuter l'algorithme indépendamment du lieu où ils sont déployés, parce que l'algorithme est indépendant de la carte de la forme cible. En outre, ces solutions cherchent à atteindre la forme de la cible avec une quantité minimale de mouvement. / MEMS microrobots are miniaturized elements that can capture and act on the environment. They have a small size, low memory capacity and limited energy capacity. These inexpensive devices can perform several missions and tasks in a wide range of applications such as locating odor, fighting against fires, medical service, surveillance, search, rescue and safety. To do these tasks and missions, they have to carry out protocols of redeployment to adapt to the working conditions. These algorithms should be efficient, scalable, robust and should only use local information. Redeployment for mobile MEMS microrobots currently requires a positioning system and a map (predefined positions) of the target shape. Traditional positioning solutions such as using GPS consumes a lot of energy and it is no applicable in the micro scale. Also, the use of an algorithmic solution positioning with multilateration techniques causes problems due to errors in the coordinates obtained. In the literature works, if we want a microrobots self-reconfiguring to a target shape consisting of P positions, each microrobot must have a storage capacity of at least P positions to save them. Therefore, if P equals to thousands or millions, every node must have a storage capacity of thousands or millions of positions. However, these algorithms are notscalable. In this thesis, we propose protocols of self-reconfiguration where nodes are not aware of their position in the plane and do not record the positions of the target shape. Therefore, the memory space required for each node is significantly reduced at a constant complexity. The purpose of these distributed algorithms is to optimize the logical topology of the network of mobile MEMS microrobots to seek a better complexity for message exchange and inexpensive communication.In this work, we show for the reconfiguration of a chain into a square, how to handle the dynamicity of the network to save energy, and we study how to use parallelism in motion to optimize the execution time and the number of movements. Furthermore, another solution is proposed where the initial physical topology may be any connected configuration. With thesesolutions the nodes can execute the algorithm regardless of where they are deployed, because the algorithm is independent of the map of the target shape. Furthermore, these solutions seek to achieve the shape of the target with a minimum amount of movement.

La dissémination collaborative d'une information d'un agent à tous les autres agents d'un système distribué est un problème fondamental qui est particulièrement important lorsque l'on veut obtenir des algorithmes distribués qui sont à la fois robustes et fonctionnent dans un cadre anonyme, c'est-à-dire sans supposer que les agents possèdent des identifiants distincts connus. Ce problème, connu sous le nom de problème de propagation de rumeur , est à la base de nombreux algorithmes de communication sur des réseaux de capteurs sans-fil [Dimakis et al. (2010)] ou des réseaux mobiles ad-hoc. Il est aussi une brique de base centrale pour de nombreux algorithmes distribués avancés [Mosk-Aoyama et Shah (2008)].Les méthodes les plus connues pour surmonter les défis de robustesse et d'anonymat sont les algorithmes basés sur les ragots ( gossip-based algorithms ), c'est-à-dire sur la paradigme que les agents contact aléatoirement les autres agents pour envoyer ou récupérer l'information. Nousproposons une méthode générale d'analyse de la performance des algorithmes basés sur les ragots dans les graphes complets. Contrairement aux résultats précédents basés sur la structure précise des processus étudiés, notre analyse est basée sur la probabilité et la covariance des évènements correspondants au fait qu'un agent non-informé s'informe. Cette universalité nous permet de reproduire les résultats basiques concernant les protocoles classiques de push, pull et push-pull ainsi qu'analyser les certaines variantions telles que les échecs de communications ou les communications simultanés multiples réalisées par chaque agent. De plus, nous sommescapables d'analyser les certains modèles dynamiques quand le réseaux forme un graphe aléatoire échantillonné à nouveau à chaque étape [Clementi et al. (ESA 2013)]. Malgré sa généralité, notre méthode est simple et précise. Elle nous permet de déterminer l'espérance du temps de la diffusion à une constante additive près, ce qu'il est plus précis que la plupart des résultatsprécédents. Nous montrons aussi que la déviation du temps de la diffusion par rapport à son espérance est inférieure d'une constante r avec la probabilité au moins 1 − exp(Ω(r)).À la fin, nous discutons d'une hypothèse classique que les agents peuvent répondre à plusieurs appels entrants. Nous observons que la restriction à un seul appel entrant par agent provoque une décélération importante du temps de la diffusion pour un protocole de push-pull. En particulier, une phase finale du processus prend le temps logarithmique au lieu du temps double logarithmique. De plus, cela augmente le nombre de messages passés de Θ(n log log n) (valeur optimale selon [Karp et al. (FOCS 2000)]) au Θ(n log n) . Nous proposons une variation simple du protocole de push-pull qui rétablit une phase double logarithmique à nouveau et donc le nombre de messages passés redescend sur sa valeur optimal. / Epidemic algorithms are distributed algorithms in which the agents in thenetwork involve peers similarly to the spread of epidemics. In this work, we focus on randomized rumor spreading -- a class of epidemic algorithms based on the paradigm that nodes call random neighbors and exchange information with these contacts. Randomized rumor spreading has found numerous applications from the consistency maintenance of replicated databases to newsspreading in social networks. Numerous mathematical analyses of different rumor spreading algorithms can be found in the literature. Some of them provide extremely sharp estimates for the performance of such processes, but most of them are based on the inherent properties of concrete algorithms.We develop new simple and generic method to analyze randomized rumor spreading processes in fully connected networks. In contrast to all previous works, which heavily exploit the precise definition of the process under investigation, we only need to understand the probability and the covariance of the events that uninformed nodes become informed. This universality allows us to easily analyze the classic push, pull, and push-pull protocols both in their pure version and in several variations such as when messages fail with constant probability or when nodes call a random number of others each round. Some dynamic models can be analyzed as well, e.g., when the network is a random graph sampled independently each round [Clementi et al. (ESA 2013)]. Despite this generality, our method determines the expected rumor spreading time precisely apart from additive constants, which is more precise than almost all previous works. We also prove tail bounds showing that a deviation from the expectation by more than an additive number of r rounds occurs with probability at most exp(−Ω(r)).We further use our method to discuss the common assumption that nodes can answer any number of incoming calls. We observe that the restriction that only one call can be answered leads to a significant increase of the runtime of the push-pull protocol. In particular, the double logarithmic end phase of the process now takes logarithmic time. This also increases the message complexity from the asymptotically optimal Θ(n log log n) [Karp, Shenker, Schindelhauer, Vöcking (FOCS 2000)] to Θ(n log n). We propose a simple variation of the push-pull protocol that reverts back to the double logarithmic end phase and thus to the Θ(n log log n) message complexity.

Durant cette thèse, nous avons introduit les problèmes de Bin Covering avec Contrainte de Distance (BCCD) et de Bin Packing avec Contrainte de Distance (BPCD), qui trouvent leur application dans les réseaux de grande échelle, tel Internet. L'étude de ces problèmes que nous effectuons dans des espaces métriques quelconques montre qu'il est impossible de travailler dans un tel cadre sans avoir recours à de l'augmentation de ressources, un procédé qui permet d'élaborer des algorithmes construisant des solutions moins contraintes que la solution optimale à laquelle elles sont comparées. En plus de résultats d'approximation intéressants, nous prouvons la difficulté de ces problèmes si ce procédé n'est pas utilisé. Par ailleurs, de nombreux outils ont pour objectif de plonger les grands réseaux qui nous intéressent dans des espaces métriques bien décrits. Nous avons alors étudié nos problèmes dans les espaces métriques générés par certains de ces outils, comme Vivaldi et Sequoia.

La conception d'algorithmes pour les systèmes concurrents et répartis est subtile et difficile. Ces systèmes sont enclins à des blocages et à des conditions de course et sont par conséquent difficiles à reproduire La vérification formelle est une technique essentielle pour modéliser le système et ses propriétés et s'assurer de sa correction au moyen du model checking. Des langages formels tels TLA+ permettent de décrire des algorithmes compliqués de manière assez concise, mais les concepteurs d'algorithmes trouvent souvent difficile de modéliser un algorithme par un ensemble de formules. Dans ce mémoire nous présentons le langage PlusCal-2 qui vise à allier la simplicité de pseudo-code à la capacité d'être vérifié formellement. PlusCal-2 améliore le langage algorithmique PlusCal conçu par Lamport en levant certaines restrictions de ce langage et en y ajoutant de nouvelles constructions. Notre langage est destiné à la description d'algorithmes à un niveau élevé d'abstraction. Sa syntaxe ressemble à du pseudo-code mais il est tout à fait expressif et doté d'une sémantique formelle. Pour calculer la dépendance conditionnelle pour les algorithmes en PlusCal-2 nous exploitons des informations sur la localité des actions et nous générons des prédicats d'indépendance. Nous proposons également une adaptation d'un algorithme de réduction par ordre partiel dynamique pour une variante du model checker TLC. Enfin, nous proposons une variante d'un algorithme de réduction par ordre partiel statique s'appuyant sur une relation de dépendance constante, et son implantation au sein de TLC. Nous présentons nos résultats expérimentaux et une preuve de correction / Designing sound algorithms for concurrent and distributed systems is subtle and challenging. These systems are prone to deadlocks and race conditions, and are therefore hard to reproduce. Formal verification is a key technique to model the system and its properties and then perform verification by means of model checking. Formal languages like TLA+ have the ability to describe complicated algorithms quite concisely, but algorithm designers often find it difficult to model an algorithm in the form of formulas. In this thesis, we present PlusCal-2 that aims at being similar to pseudo-code while being formally verifiable. PlusCal-2 improves upon Lamport?s PlusCal algorithm language by lifting some of its restrictions and adding new constructs. Our language is intended for describing algorithms at a high level of abstraction. Finite instances of algorithms described in PlusCal-2 can be verified through the TLC model checker. The second contribution presented in this thesis is a study of partial-order reduction methods using conditional and constant dependency relation. To compute conditional dependency for PlusCal-2 algorithms, we exploit their locality information and present them in the form of independence predicates. We also propose an adaptation of a dynamic partial-order reduction algorithm for a variant of the tlc model checker. As an alternative to partial order reduction based on conditional dependency, we also describe a variant of a static partial-order reduction algorithm for the tlc model checker that relies on constant dependency relation. We also present our results for the experiments along with the proof of correctness

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 de nombreux secteurs industriels, la miniaturisation des systèmes est devenue une nécessité afin de réduire l’espace occupé, le poids, les prix et la consommation d’énergie et de matière. Pour ce faire, les industriels utilisent les Micro-Electro-Mechanical Systems (MEMS). En revanche, les MEMS présentent plusieurs problèmes de fiabilité dus à leurs nombreux mécanismes de défaillance qui ont un impact sur la disponibilité des systèmes dans lesquels ils sont utilisés. Il est alors important de surveiller ces microsystèmes, d’anticiper leurs défaillances et de recommander les actions nécessaires afin d’allonger leur durée de vie. Une solution efficace pour ce faire est de développer le Prognostics & Health Management (PHM) pour les MEMS. Dans cet esprit, la thèse porte sur le pronostic et l’étude de l’état de santé de MEMS et la prise de décision post-pronostic dans les systèmes contenant ces microsystèmes. L’objectif est de rendre un système à base de MEMS distribué intelligent en intégrant des modules d’évaluation et de prédiction de l’état de santé du système ainsi que des capacités d’auto-adaptation dépendant des missions que le système doit accomplir. Dans un premier temps, une approche de pronostic hybride pour les MEMS basée sur le filtrage particulaire est proposée. Dans un second temps, et afin de mieux utiliser les résultats de cette approche, une stratégie de décision post-pronostic dans les systèmes distribués à base de MEMS est introduite. Un simulateur distribué a été développé pour simuler la décision post-pronostic. La performance de l’approche de pronostic et de la stratégie de décision post-pronostic est validée sur une application réelle, à savoir un convoyeur modulaire à base de MEMS distribués. Un cycle complet de PHM est ainsi développé : de l’acquisition des données à la prise de décision. / In many industrial sectors, system miniaturization becomes mandatory, allowing reducing occupied space, weight, price, power and material consumption. For this, manufacturers use Micro-Electro- Mechanical Sytems (MEMS). However, MEMS devices have several reliability issues due to their numerous failure mechanisms, which have an impact on the availability of systems where they are utilized. Therefore, it is important to monitor these micro-systems, to anticipate their failures and to perform appropriate actions to maximize their lifespan. One possible solution is to develop the Prognostics & Health Management (PHM) for MEMS. The thesis deals then with the prognostics and the study of MEMS health state and the post-prognostics decision making in systems containing these micro-systems. The aim is to make a MEMS-based system distributed and intelligent by integrating modules of health state assessment and prediction and capacities of self-adaptability dependent of the tasks performed by the system. Firstly, a hybrid prognostics approach for MEMS based on the particle filtering is proposed. Secondly, and to better use the results of this approach, a post-prognostics decision strategy in MEMS-based distributed systems is introduced. This strategy is based on a distributed decision algorithm. The performance of the prognostics approach and the post-prognostics strategy is validated on a real application consisting of a modular conveyor based on distributed MEMS. A complete PHM cycle is thus performed: from data acquisition to decision making.

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.