Le modèle du système réparti s'oppose au modèle classique dit ''client-serveur'' par l'absence de serveur central. Supprimer ce serveur a des conséquences bénéfiques: le réseau entier ne dépend plus de cette unique entité et ainsi un système réparti est plus robuste. Mais cette suppression a aussi un coût: le serveur centralise les données et a une connaissance globale (ou totale) du système. Dans un système réparti au contraire, aucune entité n'a de connaissance globale du système et de son état. Chaque entité échange de l'information avec un sous-ensemble des entités du système. On parle alors de vision locale (ou partielle) du système. Dans cette thèse, nous nous intéressons à la structure induite par ces visions locales et à son impact sur les applications réparties. Notre étude prend pour contexte différents modèles des systèmes répartis: le modèle partiellement synchrone, le modèle pair-à-pair et le modèle des réseaux de capteurs fixes. Notre approche se divise en trois parties: 1) nous montrons l'impact des structures de communication sur les applications réparties, et proposons une manière de capturer cet impact. Ensuite, 2) nous montrons comment l'utilisation d'hypothèses sur ces structures permet de résoudre deux problèmes classiques des systèmes répartis. Enfin 3) nous montrons comment transformer ces structures de communication en des structures logiques et explicites: les systèmes de coordonnées.

Mes travaux de recherche portent sur les modèles de programmation distribuée, principalement par objets et composants. Dans ce domaine, j'ai travaillé à fournir des outils facilitant la programmation d'applications distribuées à large échelle et vérifiant la correction de leur comportement. Pour faciliter la programmation d'applications distribuées je me suis intéressé à la mise au point de langages avec un fort niveau d'abstraction: objets actifs, squelettes algorithmiques, composants. Afin de vérifier la correction du comportement d'une application j'ai collaboré à la mise au point d'outils de spécification et de vérification comportementales d'applications distribuées. Mes travaux ont pour but de fournir un modèle formel des langages de programmations, des bibliothèques, et des environnements d'exécution fournies au programmeur afin de garantir un comportement sûr des applications distribuées. Ma thèse m'a permis de mettre au point le calcul ASP modélisant lecomportement des objets actifs et des futurs. Depuis, nous avons créé une version fonctionnelle de ce calcul que nous avons modélisé en Isabelle/HOL. Aussi j'ai fortement contribué à la définition d'un modèle à composants distribués -- le GCM (Grid Component model)--, à sa formalisation et à son utilisation pour programmer des composants adaptables ou autonomes. Enfin, j'ai contribué à la spécification et la vérification comportementale des programmes utilisant des objets actifs et des composants afin de garantir la sûreté de leur exécution. Actuellement, nous travaillons à la fois à une extension multi-threadée du modèle à objets actifs mieux adaptée aux machines multi-coeurs, et à l'utilisation de méthodes formelles pour mettre au point et prouver la correction d'un algorithme de diffusion pour réseau pair-à-pair de type CAN (Content Adressable Network). Ce manuscrit fournit une vue d'ensemble de tous ces travaux.

Mémoire numérisé par la Direction des bibliothèques de l'Université de Montréal.

Les systèmes distribués sont au cœur de nombreuses applications modernes (réseaux sociaux, services web, etc.). Cependant, les développeurs sont confrontés à de nombreux défis dans l’implémentation des systèmes distribués, notamment les comportements erronés à éviter et qui sont causées par la concurrence entre les entités de ce système. La génération automatique de code à partir des exigences des systèmes distribués reste un vieux rêve. Dans cette thèse, nous considérons la génération automatique d'un squelette de code portant sur les interactions entre les différentes entités d'un système distribué. Cela nous permet d'éviter les comportements erronés causés par la concurrence. Ensuite, ce squelette peut être complété par l'ajout et le débogage du code qui décrit les actions locales qui se passent sur chaque entité indépendamment de ses interactions avec les autres entités. / Distributed systems lie at the heart of many modern applications (social networks, web services, etc.). However, developers face many challenges in implementing distributed systems. The major one we focus on is avoiding the erroneous behaviors, that do not appear in the requirements of the distributed system, and that are caused by the concurrency between the entities of this system. The automatic code generation from requirements of distributed systems remains an old dream. In this thesis, we consider the automatic generation of a skeleton of code covering the interactions between the entities of a distributed system. This allows us to avoid the erroneous behaviors caused by the concurrency. Then, in a later step, this skeleton can be completed by adding and debugging the code that describes the local actions happening on each entity independently from its interactions with the other entities. The automatic generation that we consider is from a scenario-based specification that formally describes the interactions within informal requirements of a distributed system. We choose High-level Message Sequence Charts (HMSCs for short) as a scenario-based specification for the many advantages that they present: namely the clear graphical and textual representations, and the formal semantics. The code generation from HMSCs requires an intermediate step, called “Synthesis” which is their transformation into an abstract machine model that describes the local views of the interactions by each entity (A machine representing an entity defines sequences of messages sending and reception). Then, from the abstract machine model, the skeleton’s code generation becomes an easy task. A very intuitive abstract machine model for the synthesis of HMSCs is the Communicating Finite State Machine (CFSMs). However, the synthesis from HMSCs into CFSMs may produce programs with more behaviors than described in the specifications in general. We thus restrict then our specifications to a sub-class of HMSCs named "local HMSC". We show that for any local HMSC, behaviors can be preserved by addition of communication controllers that intercept messages to add stamping information before resending them. We then propose a new technique that we named "localization" to transform an arbitrary HMSC specification into a local HMSC, hence allowing correct synthesis. We show that this transformation can be automated as a constraint optimization problem. The impact of modifications brought to the original specification can be minimized with respect to a cost function. Finally, we have implemented the synthesis and the localization approaches into an existing tool named SOFAT. We have, in addition, implemented to SOFAT the automatic code generation of a Promela code and a JAVA code for REST based web services from HMSCs.

Les systèmes distribués ont réussi à étendre la technologie de l’information à un public plus large, en termes d’emplacement et de nombre. Cependant, ces systèmes géo-répliqués doivent être évolutifs afin de répondre aux demandes toujours croissantes. De plus, le système doit pouvoir traiter les messages dans un ordre équivalent à celui de leur création afin d’éviter des effets indésirables. L’exécution suivant des ordres partiels fournit un ordonnancement d’événements que tous les nœuds suivront, ce qui permet donc le traitement des messages dans un ordre adéquat. Un système qui applique un ordre partiel simplifie le développement des applications distribuées et s’assure que l’utilisateur final n’observera pas des comportements défiant la causalité. Dans cette thèse, nous présentons des modèles statistiques pour différentes contraintes d’ordre partiel, en utilisant différentes distributions de modèles de latence. Étant donné un modèle de latence, qui donne le temps qu’il faut pour qu’un message passe d’un nœud à un autre, notre modèle s’appuie sur lui pour donner le temps supplémentaire qu’il faut pour appliquer un ordre partiel spécifique. Nous avons proposé les modèles suivants. Tout d’abord, dans une communication entre un et plusieurs nœuds, la probabilité que le message soit délivré dans tous les nœuds avant un temps donné. Deuxièmement, après la réception d’un message, la probabilité que tous les autres nœuds aient exécuté ce message avant temps donné. Troisièmement, dans une communication de un à plusieurs nœuds, la probabilité que le message soit arrivé à au moins un sous-ensemble d’entre eux avant un temps donné. Quatrièmement, l’ordre FIFO ou causal qui détermine si un message est prêt à être livré, dans un nœud ou plusieurs. Tout cela favorise la compréhension du comportement des systèmes distribués en présence d’ordres partiels. En outre, en utilisant cette connaissance, nous avons construit un algorithme qui utilise ces modèles de comportement du réseau pour établir un système de livraison causal fiable. Afin de valider nos modèles, nous avons développé un outil de simulation qui permet d’exécuter des scénarios adaptés à nos besoins. Nous pouvons définir les différents paramètres du modèle de latence, le nombre de clients et les charges de travail des clients. Cette simulation nous permet de comparer les valeurs générées de façon aléatoire pour chaque configuration spécifique avec les résultats prévus de notre modèle. Une des applications qui peuvent tirer profit de notre modèle, est un algorithme de livraison causale fiable. Il utilise l’information causale pour détecter les éléments manquants et réduit le besoin d’acquittement de message en contactant d’autres répliques seulement lorsque le message est supposé manquant. Cette information est fournie par notre modèle, qui définit les temporisateurs d’attente en fonction des statistiques du réseau et de la consommation des ressources. Enfin, cette application a été testée dans le même simulateur que les modèles, avec des résultats prometteurs, puis évaluée dans une expérience réelle utilisant Amazon EC2 comme plate-forme / Distributed systems have managed to extend technology to a broader audience, in both terms of location and numbers. However these geo-replicated systems need to be scalable in order to meet the ever growing demands. Moreover, the system has to be able to process messages in an equivalent order that they were created to avoid unwanted side effects. Partial order enforcement provides an ordering of events that all nodes will follow therefore processing the messages in an adequate order. A system that enforces a partial order simplifies the challenge of developing distributed applications, and ensures that the end-user will not observe causality defying behaviors. In this thesis we present models for different partial order enforcements, using different latency model distributions. While a latency model, which yields the time it takes for a message to go from one node to another, our model builds on it to give the additional time that it takes to enforce a given partial order. We have proposed the following models. First, in a one to many nodes communication, the probability for the message to be delivered in all the nodes before a given time. Second, in a one to many nodes communication from the receivers, the probability that all the other nodes have delivered the message after a given time of him receiving it. Third, in a one to many nodes communication, the probability that the message has arrived to at least a subset of them before a given time. Fourth, applying either FIFO or Causal ordering determining if a message is ready for being delivered, in one node or many. All of this furthers the understanding of how distributed systems with partial orders behave. Furthermore using this knowledge we have built an algorithm that uses the insight of network behavior to provide a reliable causal delivery system. In order to validate our models, we developed a simulation tool that allows to run scenarios tailored to our needs. We can define the different parameters of the latency model, the number of clients, and the clients workloads. This simulation allows us to compare the randomly generated values for each specific configuration with the predicted outcome from our model. One of the applications that can take advantage of our model, is a reliable causal delivery algorithm. It uses causal information to detect missing elements and removes the need of message acknowledgment by contacting other replicas only when the message is assumed missing. This information is provided by our model, that defines waiting timers according to the network statistics and resource consumption. Finally this application has been both tested in the same simulator as the models, with promising results, and then evaluated in a real-life experiment using Amazon EC2 for the platform

La problématique de recherche développée concerne la modélisation de milieux complexes sous différentes approches. Initialement centrée sur la simulation d'écoulements fluides implémentée sur des systèmes informatiques parallèles, la thématique a évoluée vers des conceptions et des domaines d'applications plus vastes et notamment la modélisation des écosystèmes aquatiques dans leur complexité naturelle. On développe des aspects méthodologiques permettant la représentation d'organisations dynamiques détectées par des techniques de clustering puis représentées globalement dans des simulations multi-échelles. Les aspects liés à l'implémentation sont développés dans le cadre de systèmes informatiques distribués dynamiques et abordent quelques problèmes liés à la migration dynamique de codes. Le travail présenté ici traduit un instantané d'une recherche qui s'inscrit dans une dynamique qui a conduit à l'émergence d'une activité de recherche significative dans le cadre de la montée en puissance d'un laboratoire, le LIH (Laboratoire d'Informatique du Havre), et d'une formation doctorale, le DEA ITA (Informatique Théorique et Applications).

Au cours de ces dernières décennies, les systèmes technologiques ont beaucoup évolué. Dans le même temps, leurs installations sont de plus en plus distribuées sur plusieurs sites. Ceci conduit à la résolution de problèmes logistiques lors des prises de décision en vue d'actions de maintenance qui exigent par ailleurs des approches coopératives dans un contexte de gestion à distance. Dans ce travail, nous étudions des méthodes d'aides à la décision temps-réel pour la maintenance des systèmes multi-sites distribués dans un environnement à ressources partagées, avec des contraintes logistiques non négligeables entre les différents sites. Les exigences sont de planifier et d'ordonnancer les tâches de maintenance, de les affecter en temps-réel aux ressources de maintenance disponibles, tout en minimisant les coûts inhérents au fonctionnement et en maîtrisant les délais d'intervention des ressources. Les coûts sont relatifs notamment au fonctionnement en état dégradé (état critique), aux fréquences trop élevées ou au déficit de maintenance. Ils dépendent aussi de combinaisons linéaires ou convexes d'ensemble de paramètres tels que les temps de réponse (temps de séjour), les retards et avances ainsi que des facteurs de pondération des tâches de maintenance. Les coûts sont également fonction de la disponibilité, cette dernière étant révélatrice des dégradations des entités constituant le système. Pour satisfaire ces exigences, différents problèmes doivent être résolus dans le but de maintenir la disponibilité du système au dessus d'une limite minimale, de minimiser le coût des opérations de maintenance et d'affecter en temps-réel les tâches aux ressources de maintenance, le tout dans un processus optimal de décision. Ce processus doit tenir compte de différentes contraintes : dates d'arrivée inégales des tâches, temps logistiques non négligeables entre les sites, séquences optimales des tâches d'une intervention, précédences entre les tâches d'une même entité et critères de priorité et d'urgence de chaque tâche. Dans cette démarche, les caractéristiques et lois de comportement en fiabilité et en maintenabilité, et les sollicitations d'intervention sur les entités sont connues. Pour résoudre ces problèmes, nous proposons une approche mettant en oeuvre des méthodes d'ordonnancement d'activités (tâches ou actions) de maintenance basées sur des règles de priorité dont nous montrons l'optimalité locale (par rapport au temps) dans ce document. Partant d'une ressource de maintenance, ces règles de décision s'inspirent des principes d'ordonnancement sur une seule machine. Elles sont utilisées dans des algorithmes d'aide à la décision en temps-réel pour la planification dynamique des tâches de maintenance des systèmes distribués. Aux solutions fournies par la plupart de ces règles nous avons déterminé des bornes inférieures. Nous avons structuré ce document en six chapitres dont le premier introduit de façon générale la maintenance et ses différentes pratiques dans les entreprises. Le chapitre 2 propose une analyse de l'état de l'art des travaux de recherche scientifique dans le domaine de la gestion des activités de maintenance. Ensuite, dans le chapitre 3, des approches de résolution des problèmes relatifs aux coûts des états critiques du système sont proposées. Le chapitre 4 traite alors les différents problèmes relatifs aux contraintes de délais sur les opérations de maintenance induisant notamment des coûts combinés liés aux états critiques et aux retards d'intervention d'une part, et des coûts dus aux avances ou retards des tâches d'autre part. Il apparut alors nécessaire d'étudier la robustesse des performances des approches proposées dans les chapitres 3 et 4 en environnements incertains. Cette étude fût donc réalisée dans le chapitre 5 par des simulations Monte Carlo de la maintenance à partir des données d'un système réel soumis à des aléas de défaillance appelant des actions correctives. Enfin, de l'ensemble des investigations menées dans ce travail furent tirées les principales conclusions et les perspectives proposées dans le chapitre 6.

Les systèmes informatiques ont connu récemment de grandes avancées dans leur conception. D'une part, la démocratisation des réseaux via la croissance exponentielle de l'Internet a permis d'envisager des systèmes à l'échelle mondiale, visant de mettre en commun une multitude de ressources à travers la planète entière. D'autre part, la réduction continue de la taille des équipements informatiques a permis l'apparition de matériels miniatures. Le jumelage de ces deux évolutions est à l'origine de l'apparition des réseaux de capteurs sans fil. Le spectre des applications potentielles de ces réseaux est extrêmement large, que cela soit dans le contexte d'une infrastructure fixe autant que dans l'informatique embarquée. Cette thèse propose un ensemble de contributions pour la gestion de l'information à la fois dans le contexte mobile et statique. Édifiées autour des mêmes propriétés de collaboration et d'auto-organisation, ces propositions sont conçues selon une méthodologie de la théorie vers la pratique. Cette thèse vise ainsi, en premier lieu, une analyse théorique a priori d'une application classique des réseaux de capteurs statiques, à savoir le suivi de trajectoires d'objets mobiles non identifiés. Par la suite, nous étendons le spectre des applications visées en proposant une structure générique à toute mise en oeuvre réelle de réseaux de capteurs statiques. En second lieu, nous considérons une modélisation de la mobilité permettant d'analyser fondamentalement les impacts de celle-ci sur la convergence des protocoles dits de population. Enfin, nous établissons un parallèle entre les travaux menés théoriquement sur les réseaux de capteurs mobiles avec ceux plus pratiques et empiriques proposés dans le cadre des protocoles épidémiques sur réseaux filaires. En démontrant que ces deux domaines portent en réalité sur la même classe de protocoles -- et donc de problèmes -- nous ouvrons ainsi une voie captivante pour de futures recherches dans chacun de ces deux domaines, par l'utilisation de l'un dans l'autre.

L'ouverture de ces systèmes est assurée au moyen d'un service de communication externe. Ce service permet aux applications s'exécutant dans le système distribue local de communiquer à plusieurs niveaux de protocoles avec d'autres applications s'exécutant sur des systèmes distants distribues ou centralises. On étudie l'architecture et le fonctionnement de tels systèmes

Cette thèse se place dans le cadre de la vérification automatique des systèmes distribués. Elle aborde le problème de la spécification pour de tels systèmes, qui consiste à définir un formalisme logique pour décrire des propriétés des comportements de systèmes. On en attend qu'il soit facile d'exprimer les propriétés courantes (accessibilité, sûreté, exclusion mutuelle, vivacité, etc.). On souhaite par ailleurs que la vérification de ces propriétés soient aisée. Il s'agit donc de trouver un compromis entre pouvoir d'expression et simplicité d'utilisation.<br /><br />On s'intéresse ensuite à la modélisation des systèmes concurrents, en recherchant à nouveau un compromis entre réalisme des modèles et facilité de vérification. Les modèles étudiés dans ce travail sont les automates asynchrones, qui modélisent des processus concurrents communiquant par mémoire partagée.<br /><br />La thèse s'intéresse enfin au problème de la synthèse de contrôleur. Étant donné un système spécifié de façon incomplète, donc non-déterministe, en interaction avec un environnement, il s'agit de calculer de manière automatique comment restreindre son comportement afin qu'il vérifie une spécification donnée (quelles que soient les actions de l'environnement). Ce problème se formule en<br />termes de jeux. Dans le cas distribué, les jeux ont naturellement plusieurs joueurs. Dans ce cadre, la plupart des résultats sont négatifs : il est indécidable de savoir si on peut ou non contrôler un tel système. Cette thèse prouve que certaines propriétés de l'architecture de communication garantissent décidabilité pour toute spécification régulière.