Cette thèse se situe dans le cadre du projet INCOME (INfrastructure de gestion de COntexte Multi-Échelle pour l'Internet des Objets) financé par l'ANR (Appel INFRA 2011). L'objectif de ce projet est de fournir un cadriciel pour le développement et le déploiement d'un gestionnaire de contexte. Les entités logicielles d'acquisition, de traitement, de dissémination et de présentation d'informations de contexte, qui constituent un gestionnaire de contexte, doivent être construites et déployées au-dessus d'infrastructures technologiques hétérogènes et interconnectées. Ainsi, les cibles incluent les réseaux de capteurs, les systèmes ambiants, les dispositifs mobiles ou encore les serveurs du cloud, et de façon plus globale l'Internet des Objets (IoT). Les travaux menés dans cette thèse concernent plus particulièrement la gestion " de bout en bout " de la Qualité de Contexte (QoC) au sein de cette nouvelle génération de gestionnaires de contexte à déployer sur l'IoT à grande et multiples échelles. La qualité de l'information de contexte relevant de critères tels que la précision, la fraîcheur, la complétude, la granularité... Par gestion de la QoC, nous faisons référence à l'ensemble des opérations qui, tout le long du cycle de vie d'une information de contexte, permettent de gérer sa qualification, mais également d'influer, en fonction de cette qualité, sur sa dissémination et sa livraison aux applications sensibles au contexte. Actuellement des solutions de gestion de la QoC existent mais restent ad hoc à des environnements ambiants particuliers ou des applications spécifiques. Elles s'avèrent inadéquates en termes d'ouverture, de généricité et de calculabilité pour des environnements fortement hétérogènes et dynamiques tels que l'IoT où il n'y a plus de couplages forts et figés entre producteurs ou consommateurs d'informations de contexte. QoCIM (QoC Information Model) constitue le cœur de notre contribution. Il s'agit d'un méta-modèle dédié qui permet, de façon unifiée et ouverte, de définir des critères de QoC simples et composites. Basées sur QoCIM, des opérations de gestion de la QoC ont été identifiées et spécifiées. Elles permettent d'associer des critères de QoC, sous forme de métadonnées, à l'information de contexte, de caractériser les métriques et les unités pour leur valuation, d'inférer des critères de QoC de plus haut niveau d'abstraction, ou encore d'exprimer des conditions de filtrage portant sur de tels critères et/ou leurs valeurs. Un outillage logiciel d'édition de modèles QoCIM et une API en Java sont proposés aux développeurs pour facilement intégrer la gestion de tout critère de QoC lors du développement d'entités d'acquisition, de traitement, de livraison et de propagation d'informations de contexte et des applications sensibles au contexte. L'utilisation de ce cadriciel a été expérimentée, à la fois en phases de conception et d'exécution, sur un scénario de pollution urbaine. Des évaluations de performances ont été également menées et ont montré que le surcoût apporté par la prise en considération des niveaux de QoC pour le routage des informations de contexte était acceptable. Enfin, une solution d'auto-(re)configuration des opérations de gestion de la QoC a été également conçue et prototypée. / The objective of the ANR INCOME project is to provide a framework for the development and the deployment of a context manager. A context manager is composed of software entities, which acquire, process, disseminate or deliver context data. These software entities have to be built and deployed over interconnected heterogeneous ICT infrastructures, which include sensor networks, ambient systems, mobile devices, cloud servers and, more generally, the Internet of Things (IoT). Related to this project, the research work presented in this thesis concerns more specifically the end-to-end management of Quality of Context (QoC) within the new generation of context managers that have to be deployed at large and multiple scales over the IoT. Quality of context data refers to criteria like accuracy, freshness, completeness or granularity. As for QoC management, it deals with all the operations that allow, throughout the life cycle of context data, to manage their qualification, but also to impact, according to this quality, on its dissemination and delivery to context-aware applications. Current QoC management solutions are dedicated to particular ambient environments or to specific applications. They are limited in terms of openness, genericity and computationability, properties required by greatly heterogeneous and dynamic IoT-based environments, in which producers and consumers of context data are no more static and highly coupled. Our contribution relies on QoCIM (QoC Information Model), a meta-model dedicated to define, in a uniform and open way, any atomic or composite QoC criterion. Based on QoCIM, some QoC management operations have been identified and specified. These operations allow to associate criteria of QoC, in the form of metadata, with the information of context; to characterize the metrics and units for their valuation; to infer QoC criteria of a higher level of abstraction; or even to express filtering conditions for such criteria or their values. A software tool for editing QoCIM models and a Java API are provided to developers to easily implement the management of any QoC criterion for their software entities that acquire, process, deliver or propagate context data, or their context-sensititive application. The use of this framework was experimented, both at design time and at run time, on a scenario related to urban pollution. Benchmarking was also led and showed that the additional cost brought when considering QoC in context information routing was acceptable. Finally, a solution for self-(re)configuring QoC management operations was also designed and prototyped.

Depuis plusieurs années, de nombreuses recherches ont été menées autour du diagnostic. Cependant, il est impératif de se préoccuper dès la phase de conception d’un système des objectifs de diagnostic à atteindre. Aussi, de nombreux travaux se sont intéressés à analyser et à caractériser les propriétés de la diagnosticabilité d’un système. La diagnosticabilité est la propriété d’un système garantissant qu’il génère des observations permettant de détecter et discriminer les fautes en temps fini après leur occurrence.Le sujet de cette thèse porte sur les méthodes permettant d’établir les propriétés de la diagnosticabilité des systèmes à événements discrets dans le cadre distribué, sans construction du modèle global du système. Ce cadre est de première importance pour les applications réelles : systèmes naturellement distribués, systèmes trop complexes pour traiter leur modèle global, confidentialité des modèles locaux les uns par rapport aux autres. L’analyse de la diagnosticabilité de tels systèmes distribués se fonde sur des opérations de synchronisation des modèles locaux, par les observations et les communications. D’abord, nous étudions comment optimiser cette analyse de la diagnosticabilité en faisant abstraction de l’information nécessaire et suffisante à partir des objets locaux pour décider la diagnosticabilité globale. L'efficacité de l’algorithme peut être grandement améliorée par la synchronisation des objets locaux et abstraits en comparaison avec celle des objets locaux et non abstraits.Ensuite, nous proposons, dans le cadre distribué, l'algorithme de la diagnosticabilité de motifs d'événements particuliers a priori inobservables dans les systèmes. Ces motifs peuvent être simplement l’occurrence, brutale ou graduelle, d’une faute permanente ou transitoire, plusieurs occurrences d’une faute, plusieurs fautes en cascade, etc. Dans le cadre distribué, la reconnaissance du motif d’événements s’effectue d’abord progressivement dans un sous-système et ensuite la diagnosticabilité de ce motif peut être déterminée par la méthode abstraite et distribuée. Nous prouvons la correction et l'efficacité de notre algorithme à la fois en théorie et en pratique par la mise en œuvre de l’implémentation sur des exemples.Finalement, nous étudions le problème de la diagnosticabilité dans les systèmes distribués avec composants autonomes, où l’information observable est distribuée au lieu d’être centralisée comme jusqu’alors. En d'autres termes, chaque composant ne peut appréhender que ses propres événements observables. Nous donnons la définition de la diagnosticabilité conjointe. Et puis nous discutons de l'indécidabilité de diagnosticabilité conjointe dans le cas général, c'est à dire, les événements de communication ne sont pas observables, avant de proposer un algorithme pour tester sa condition suffisante. De plus, nous obtenons également un résultat de décidabilité et de l'algorithme lorsque les communications sont observables. / Over the latest decades, much research work has been done on automatic fault diagnosis. However, it is imperative to analyze at system design stage how correctness and efficiency and diagnosis algorithm can achieve. Thus many studies were interested in analyzing and characterizing the properties of diagnosability of a system. Diagnosability is the property of a system ensuring that it generates observations for detecting and discriminating faults in finite time after their occurrence.In this thesis, we investigate how to optimize distributed diagnosability analysis by abstracting necessary and sufficient information from local objects to decide global diagnosability decision. The algorithm efficiency can be greatly improved by synchronization of abstracted local objects compared to that of non abstracted local ones.Then we extend the distributed diagnosability algorithm from fault event first to simple pattern and then to general pattern, where pattern can describe more general objects in the diagnosis problem, e.g., multiple faults, multiple occurrences of the same fault, ordered occurrences of significant events, etc. In the distributed framework, the pattern recognition is first incrementally performed normally in a subsystem and then pattern diagnosability can be determined by adjusting abstracted method used in fault event case. We prove the correctness and efficiency of our proposed algorithm both in theory through proof and in practice through implementation.Finally we study joint diagnosability problem in systems with autonomous components, i.e., observable information is distributed instead of centralized. In other words, each component can only observe its own observable events. We give joint diagnosability definition. And then we discuss the undecidability of joint diagnosability in the general case, i.e., communication events are not observable, before proposing an algorithm to test its sufficient condition. In addition, we also get a decidability result and algorithm when communications are observable.

Les systèmes actuels deviennent chaque jour de plus en plus complexe; à la distribution s’ajoutent les contraintes temps réel. Les méthodes classiques en charge de garantir la sûreté de fonctionnement, comme le test, l’injection de fautes ou les méthodes formelles ne sont plus suffisantes à elles seules. Afin de pouvoir traiter les éventuelles erreurs lors de leur apparition dans un système distribué donné, nous désirons mettre en place un programme, surveillant ce système, capable de lancer une alerte lorsque ce dernier s’éloigne de ses spécifications ; un tel programme est appelé superviseur (ou moniteur). Le fonctionnement d’un superviseur consiste simplement à interpréter un ensemble d’informations provenant du système sous forme de message, que l’on qualifiera d’évènement, et d’en déduire un diagnostic. L’objectif de cette thèse est de mettre un place un superviseur distribué permettant de vérifier en temps réel des propriétés temporelles. En particulier nous souhaitons que notre moniteur soit capable de vérifier un maximum de propriétés avec un minimum d’information. Ainsi notre outil est spécialement conçu pour fonctionner parfaitement même si l’observation est imparfaite, c’est-à-dire, même si certains évènements arrivent en retard ou s’ils ne sont jamais reçus. Nous avons de plus cherché à atteindre cet objectif de manière distribuée pour des raisons évidentes de performance et de tolérance aux fautes. Nous avons ainsi proposé un protocole distribuable fondé sur l’exécution répartie d’un réseau de Petri temporisé. Pour vérifier la faisabilité et l’efficacité de notre approche, nous avons mis en place une implémentation appelée Minotor qui s’est révélée avoir de très bonnes performances. Enfin, pour montrer l’expressivité du formalisme utilisé pour exprimer les spécifications que l’on désire vérifier, nous avons détaillé un ensemble de propriétés sous forme de réseaux de Petri à double sémantique introduite dans cette thèse (l’ensemble des transitions étant partitionné en deux catégories de transitions, chacune de ces parties ayant sa propre sémantique). / Current systems are becoming every day more and more complex, being both distributed and real-timed. Conventional methods responsible for guaranteeing dependability, such as testing, fault injection or formal methods are no longer sufficient. In order to process any errors when they appear in a given distributed system, we want to implement a software monitoring it and capable of launching an alert when the system does not respect anymore its specification. Such a program is called monitor. A monitor interpret information received from the system as messages (these messages are called events) and propose a diagnosis. The objective of this thesis is to set in place a monitor for a distributed real-time verification of temporal properties. In particular we want our monitor to be able to check up a maximum of properties with a minimum of information. Thus, our tools are designed to work perfectly even if the observation is imperfect, that is to say, even if some events are late or never received. We have also managed to achieve this goal through a highly distributed protocol. To verify the feasibility and effectiveness of our approach, we have established an implementation called Minotor who was found to have very good performance. Finally, we detailed a set of properties, expressed in our formalism, to show it’s expressiveness.

Les mécanismes de réputation sont des outils très utiles pour inciter des utilisateurs ne se connaissant pas à se faire confiance, en récompensant les bons comportements et, inversement, en pénalisant les mauvais. Cependant, pour que la réputation des fournisseurs de service soit précise et robuste aux attaques, les mécanismes de réputation existants requièrent de nombreuses informations qui menacent la vie privée des utilisateurs; par exemple, il est parfois possible de traquer les interactions effectuées par les clients. Des mécanismes de réputation préservant aussi bien la vie privée des clients que celle des fournisseurs sont donc apparus pour empêcher de telles attaques. Néanmoins, pour garantir des propriétés fortes de vie privée, ces mécanismes ont dû proposer des scores de réputation imprécis, notamment en ne permettant pas aux clients de témoigner de leurs interactions négatives.Dans cette thèse, nous proposons un nouveau mécanisme de réputation distribué préservant la vie privée, tout en permettant aux clients d'émettre des témoignages négatifs. Une telle construction est possible grâce à des outils issus des systèmes distribués -- des tierces parties distribuées qui permettent de distribuer la confiance et de tolérer des comportements malveillants -- et de la cryptographie -- par exemple des preuves de connaissance à divulgation nulle de connaissance ou des signatures proxy anonymes. Nous prouvons de plus que ce mécanisme garantit les propriétés de vie privée et de sécurité nécessaires, et montrons par des analyses théoriques et pratiques que ce mécanisme est utilisable. / Reputation mechanisms are very powerful mechanisms to foster trust between unknown users, by rewarding good behaviors and punishing bad ones. Reputation mechanisms must guarantee that the computed reputation scores are precise and robust against attacks; to guarantee such properties, existing mechanisms require information that jeopardize users' privacy: for instance, clients' interactions might be tracked. Privacy-preserving reputation mechanisms have thus been proposed, protecting both clients' privacy and the providers' one. However, to guarantee strong privacy properties, these mechanisms provide imprecise reputation scores, particularly by preventing clients to testify about their negative interactions. In this thesis, we propose a new distributed privacy-preserving reputation mechanism allowing clients to issue positive as well as negative feedback. Such a construction is made possible thanks to tools from the distributed systems community -- distributed third parties that allow for a distribution of trust and that tolerate malicious behaviors -- as well as from the cryptographic one -- for instance zero-knowledge proofs of knowledge or anonymous proxy signatures. Furthermore, we prove that our mechanism guarantees the required privacy and security properties, and we show with theoretical and practical analysis that this mechanism is usable.

Dans cette thèse, nous proposons une approche rigoureuse pour la conception et le développement de systèmes à base de composants hiérarchiques distribués. L’idée de base du travail présenté est de combiner les techniques de conception de logiciels dirigées par les modèles, bien connues des programmeurs, avec des méthodes de vérification formelles puissantes, capables d’assurer les propriétés fonctionnelles d’un système distribué et de détecter les erreurs dès le stade de la conception. Tout d’abord, nous introduisons un formalisme graphique basé sur UML pour l’architecture et le comportement des composants hiérarchiques de modélisation. Deuxièmement, nous spécifions formellement un ensemble de contraintes qui assurent la correction de la composition des composants, en mettant l’accent sur la séparation entre les aspects fonctionnels et non-fonctionnels. Troisièmement, nous expliquons comment nos modèles graphiques peuvent être traduits automatiquement dans le formalisme d’entrée d’un model-checker. Nous nous concentrons ensuite sur le codage des fonctionnalités avancées de composants distribués, comme communications de 1 vers N, la reconfiguration et les communications asynchrones basées sur les appels de procédures distants. Enfin, nous mettons en oeuvre cette approche dans une plateforme intégrée orienté modèle qui comprend un ensemble d’éditeurs graphiques, un module de validation de la décision correcte de l’architecture statique, un module traduisant le modèle conceptuel dans une entrée pour la plateforme de vérification CADP, et enfin un générateur de code exécutable / In this thesis we introduce an approach for rigorous design and development of distributed hierarchical component-based systems. The core idea of the presented work is to combine the well-known among the programmers techniques for modeldriven software design and the powerful formal verification methods able to ensure the functional properties of a distributed system and to detect errors at the early design stage. First, we introduce a UML-based graphical formalism for modelling architecture and behaviour of hierarchical components. Second, we formally specify a set of constraints that ensure the correct components composition with a focus on separation between the functional and non-functional aspects. Third, we explain how the graphical models can be automatically translated into an input for a model-checker. For this aim, we rely on a formally specified intermediate structure encoding the semantics of components behaviour as a network of synchronised parametrised label transition systems. We focus here on encoding the advanced features of distributed components such as one-to-many communications, reconfiguration, and asynchronous communications based on request-reply. Finally, we implement the approach in an integrated model-driven environment which comprises a set of graphical editors, an architecture static correctness validation plug-in, a plug-in translating the conceptual model into an input for a verification toolsuite CADP, and a generator of the implementation code

Dans cette thèse, nous abordons deux problèmes soulevés par les systèmes distribués décentralisés - le placement de réseaux logiques de façon compatible avec le réseau physique sous-jacent et la construction de cohortes d'éditeurs pour dans les systèmes d'édition collaborative. Bien que les réseaux logiques (overlay networks) été largement étudiés, la plupart des systèmes existant ne prennent pas ou prennent mal en compte la topologie du réseau physique sous-jacent, alors que la performance de ces systèmes dépend dans une grande mesure de la manière dont leur topologie logique exploite la localité présente dans le réseau physique sur lequel ils s'exécutent. Pour résoudre ce problème, nous proposons dans cette thèse Fluidify, un mécanisme décentralisé pour le déploiement d'un réseau logique sur une infrastructure physique qui cherche à maximiser la localité du déploiement. Fluidify utilise une stratégie double qui exploite à la fois les liaisons logiques d'un réseau applicatif et la topologie physique de son réseau sous-jacent pour aligner progressivement l'une avec l'autre. Le protocole résultant est générique, efficace, évolutif et peut améliorer considérablement les performances de l'ensemble. La deuxième question que nous abordons traite des plates-formes d'édition collaborative. Ces plates-formes permettent à plusieurs utilisateurs distants de contribuer simultanément au même document. Seuls un nombre limité d'utilisateurs simultanés peuvent être pris en charge par les éditeurs actuellement déployés. Un certain nombre de solutions pair-à-pair ont donc été proposées pour supprimer cette limitation et permettre à un grand nombre d'utilisateurs de collaborer sur un même document sans aucune coordination centrale. Ces plates-formes supposent cependant que tous les utilisateurs d'un système éditent le même jeu de document, ce qui est peu vraisemblable. Pour ouvrir la voie à des systèmes plus flexibles, nous présentons, Filament, un protocole décentralisé de construction de cohorte adapté aux besoins des grands éditeurs collaboratifs. Filament élimine la nécessité de toute table de hachage distribuée (DHT) intermédiaire et permet aux utilisateurs travaillant sur le même document de se retrouver d'une manière rapide, efficace et robuste en générant un champ de routage adaptatif autour d'eux-mêmes. L'architecture de Filament repose sur un ensemble de réseaux logiques auto-organisées qui exploitent les similarités entre jeux de documents édités par les utilisateurs. Le protocole résultant est efficace, évolutif et fournit des propriétés bénéfiques d'équilibrage de charge sur les pairs impliqués. / In this thesis, we address two issues in the area of decentralized distributed systems: network-aware overlays and collaborative editing. Even though network overlays have been extensively studied, most solutions either ignores the underlying physical network topology, or uses mechanisms that are specific to a given platform or applications. This is problematic, as the performance of an overlay network strongly depends on the way its logical topology exploits the underlying physical network. To address this problem, we propose Fluidify, a decentralized mechanism for deploying an overlay network on top of a physical infrastructure while maximizing network locality. Fluidify uses a dual strategy that exploits both the logical links of an overlay and the physical topology of its underlying network to progressively align one with the other. The resulting protocol is generic, efficient, scalable and can substantially improve network overheads and latency in overlay based systems. The second issue that we address focuses on collaborative editing platforms. Distributed collaborative editors allow several remote users to contribute concurrently to the same document. Only a limited number of concurrent users can be supported by the currently deployed editors. A number of peer-to-peer solutions have therefore been proposed to remove this limitation and allow a large number of users to work collaboratively. These decentralized solution assume however that all users are editing the same set of documents, which is unlikely to be the case. To open the path towards more flexible decentralized collaborative editors, we present Filament, a decentralized cohort-construction protocol adapted to the needs of large-scale collaborative editors. Filament eliminates the need for any intermediate DHT, and allows nodes editing the same document to find each other in a rapid, efficient and robust manner by generating an adaptive routing field around themselves. Filament's architecture hinges around a set of collaborating self-organizing overlays that utilizes the semantic relations between peers. The resulting protocol is efficient, scalable and provides beneficial load-balancing properties over the involved peers.

Les automates distribués sont des machines à états finis qui opèrent sur des graphes orientés finis. Fonctionnant comme des algorithmes distribués synchrones, ils utilisent leur graphe d'entrée comme un réseau dans lequel des processeurs identiques communiquent entre eux pendant un certain nombre (éventuellement infini) de rondes synchrones. Pour la variante locale de ces automates, où le nombre de rondes est borné par une constante, Hella et al. (2012, 2015) ont établi une caractérisation logique par des formules de la logique modale de base. Dans le cadre de cette thèse, nous présentons des caractérisations logiques similaires pour deux classes d'automates distribués plus expressives.La première classe étend les automates locaux avec une condition d'acceptation globale et la capacité d'alterner entre des modes de calcul non-déterministes et parallèles. Nous montrons qu'elle est équivalente à la logique monadique du second ordre sur les graphes.En nous restreignant à des transitions non-déterministes ou déterministes, nous obtenons également deux variantes d'automates strictement plus faibles pour lesquelles le problème du vide est décidable.Notre seconde classe adapte la notion standard d'algorithme asynchrone au cadre des automates distribués non-locaux. Les machines résultantes sont prouvées équivalentes à un petit fragment de la logique de point fixe, et plus précisément, à une variante restreinte du μ-calcul modal qui autorise les plus petits points fixes mais interdit les plus grands points fixes. Profitant du lien avec la logique, nous montrons aussi que la puissance expressive de ces automates asynchrones est indépendante du fait que des messages puissent être perdus ou non.Nous étudions ensuite la décidabilité du problème du vide pour plusieurs classes d'automates non-locaux. Nous montrons que le problème est indécidable en général, en simulant une machine de Turing par un automate distribué qui échange les rôles de l'espace et du temps. En revanche, le problème s'avère décidable en LOGSPACE pour une classe d'automates oublieux, où les nœuds voient les messages reçus de leurs voisins, mais ne se souviennent pas de leur propre état. Finalement, à titre de contribution mineure, nous donnons également de nouvelles preuves de séparation pour plusieurs hiérarchies d'alternance de quantificateurs basées sur la logique modale. / Distributed automata are finite-state machines that operate on finitedirected graphs. Acting as synchronous distributed algorithms, they use their input graph as a network in which identical processors communicate for a possibly infinite number of synchronous rounds. For the local variant of those automata, where the number of rounds is bounded by a constant, Hella et al. (2012, 2015) have established a logical characterization in terms of basic modal logic. In this thesis, we provide similar logical characterizations for two more expressive classes of distributed automata.The first class extends local automata with a global acceptance condition and the ability to alternate between non deterministic and parallel computations. We show that it is equivalent to monadic second-order logic on graphs. By restricting transitions to be non deterministic or deterministic, we also obtain two strictly weaker variants for which the emptiness problem is decidable.Our second class transfers the standard notion of asynchronous algorithm to the setting of non local distributed automata. There sulting machines are shown to be equivalent to a small fragment of least fixpoint logic, and more specifically, to a restricted variantof the modal μ -calculus that allows least fixpoints but forbids greatest fixpoints. Exploiting the connection with logic, we additionally prove that the expressive power of those asynchronous automata is independent of whether or not messages can be lost.We then investigate the decidability of the emptiness problem forseveral classes of nonlocal automata. We show that the problem isundecidable in general, by simulating a Turing machine with adistributed automaton that exchanges the roles of space and time. Onthe other hand, the problem is found to be decidable in logspace for a class of forgetful automata, where the nodes see the messages received from their neighbors but cannot remember their own state. As a minor contribution, we also give new proofs of the strictness of several set quantifier alternation hierarchies that are based on modallogic.

Les applications de transmission de messages distribués font partie du courant dominant des technologies de l'information car elles exploitent la puissance des systèmes informatiques parallèles pour produire des performances plus élevées. La conception de programmes distribués reste difficile car les développeurs doivent raisonner sur la concurrence, le non-déterminisme, la distribution de données… qui sont les principales caractéristiques des programmes distribués. En outre, il est pratiquement impossible de garantir l'exactitude de tels programmes via des approches de test classiques, car il est possible que l'on n'atteigne jamais avec succès l'exécution qui conduit à des comportements indésirables dans les programmes. Il existe donc un besoin de techniques de vérification plus puissantes. La vérification des modèles est l'une des méthodes formelles qui permet de vérifier automatiquement et efficacement certaines propriétés des modèles de systèmes informatiques en explorant tous les comportements possibles (états et transitions) du modèle de système. Cependant, les espaces d'état augmentent de façon exponentielle avec le nombre de processus simultanés, conduisant à une «explosion de l'espace d'état» .La réduction dynamique de l'ordre partiel basée sur le dépliage (UDPOR) est une technique récente mélangeant la réduction dynamique de l'ordre partiel (DPOR) avec des concepts de théorie de la concurrence tels que dépliages pour atténuer efficacement l'explosion de l'espace d'états lors de la vérification des modèles de programmes simultanés. Il est optimal dans le sens où chaque trace de Mazurkiewicz, c'est-à-dire une classe d'entrelacements équivalents en commutant des actions indépendantes adjacentes, est explorée exactement une fois. Et elle s'applique aux programmes en cours d'exécution, pas seulement aux modèles de programmes.La thèse vise à adapter UDPOR pour vérifier les programmes distribués asynchrones (par exemple les programmes MPI) dans le cadre du simulateur SIMGRID d'applications distribuées. Pour ce faire, un modèle de programmation abstrait de programmes distribués asynchrones est défini et formalisé en langage TLA +, permettant de définir avec précision une relation d'indépendance, ingrédient principal de la sémantique concurrentielle. Ensuite, l'adaptation de l'UDPOR, impliquant la construction d'un dépliage, est rendue efficace par une analyse précise des dépendances dans le modèle de programmation, permettant des calculs efficaces d'opérations habituellement coûteuses. Un prototype d'implémentation d'UDPOR adapté aux programmes asynchrones distribués a été développé, donnant des résultats expérimentaux prometteurs sur un ensemble significatif de références. / Distributed message passing applications are in the mainstream of information technology since they exploit the power of parallel computer systems to produce higher performance. Designing distributed programs remains challenging because developers have to reason about concurrency, non-determinism, data distribution… that are main characteristics of distributed programs. Besides, it is virtually impossible to ensure the correctness of such programs via classical testing approaches since one may never successfully reach the execution that leads to unwanted behaviors in the programs. There is thus a need for more powerful verification techniques. Model-checking is one of the formal methods that allows to verify automatically and effectively some properties on models of computer systems by exploring all possible behaviors (states and transitions) of the system model. However, state spaces increase exponentially with the number of concurrent processes, leading to “state space explosion”.Unfolding-based Dynamic Partial Order Reduction (UDPOR) is a recent technique mixing Dynamic Partial Order Reduction (DPOR) with concepts of concurrency theory such as unfoldings to efficiently mitigate state space explosion in model-checking of concurrent programs. It is optimal in the sense that each Mazurkiewicz trace, i.e. a class of interleavings equivalent by commuting adjacent independent actions, is explored exactly once. And it is applicable to running programs, not only models of programs.The thesis aims at adapting UDPOR to verify asynchronous distributed programs (e.g. MPI programs) in the setting of the SIMGRID simulator of distributed applications. To do so, an abstract programming model of asynchronous distributed programs is defined and formalized in the TLA+ language, allowing to precisely define an independence relation, a main ingredient of the concurrency semantics. Then, the adaptation of UDPOR, involving the construction of an unfolding, is made efficient by a precise analysis of dependencies in the programming model, allowing efficient computations of usually costly operation. A prototype implementation of UDPOR adapted to distributed asynchronous programs has been developed, giving promising experimental results on a significant set of benchmarks.

Le Cloud, avec son modèle économique, offre la possibilité d’un gestion élastique des ressources; les utilisateurs peuvent louer des ressources selon leurs besoins. Cette élasticité permet de réduire les coûts énergétiques et financiers, et aide les applications à s’adapter aux charges de travail variables.Les applications manipulant de grandes quantités de données exécutées dans le Cloud ou sur des supercalculateurs sont souvent colocalisées avec un système de stockage distribué pour garantir un accès rapide aux données. Bien que de nombreux travaux aient été proposés pour redimensionner dynamiquement les capacités de calcul pour s’ajuster à la charge de travail, le stockage n’est pas considéré comme malléable (capable d’être redimensionné dynamiquement) puisque les transferts de grandes quantités de données nécessaires sont considérés trop lents. Cependant, le matériel et les techniques de stockage ont évolué et cette hypothèse doit être réévaluée.Dans cette thèse, nous présentons une étude sous différents angles des opérations de redimensionnement des systèmes de stockage distribués.Nous commençons par modéliser la durée minimale de ces opérations pour évaluer leur vitesse potentielle. Puis, nous développons un benchmark conçu pour mesurer la viabilité de la malléabilité d’un système de stockage sur une plateforme donnée. Finalement, nous implémentons un gestionnaire d’opérations de redimensionnement pour systèmes de stockage distribués qui décide et organise les transferts de données requis par ces opérations. / The Cloud, with its pay-as-you-go model, gives the possibility of elastic resource management; users can claim and release resources as needed. This elasticity leads to financial and energetical cost reductions, and helps applications to cope with varying workloads.Distributed cloud and HPC applications processing large amounts of data are often co-located with a distributed storage system in order to ensure fast data accesses. Although many works have been proposed to dynamically rescale the processing part of such systems to match their workload, the storage is never considered as malleable (able to be dynamically rescaled) since moving massive amounts of data around is assumed to be too slow in practice. However, in recent years hardware and storage techniques have evolved and this assumption needs to be revisited.In this thesis, we present a study of the rescaling operations in distributed storage systems approached from different angles. We start by modeling the minimal duration of rescaling operations to estimate their potential speed. Then, we develop a benchmark to measure the viability of distributed storage system malleability on a given platform. Last, we implement a rescaling manager for distributed storage systems that decides and organizes the data transfers required during a rescaling operation.

La réalité mixe, les jeux en ligne massivement multijoueur (MMOGs), les mondes virtuels et le cyberespace sont des concepts extrêmement attractifs. Mais leur déploiement à large échelle reste difficile et il est en conséquence souvent évité.La contribution principale de la thèse réside dans le système distribué Kiwano, qui permet à un nombre illimité d'avatars de peupler et d'interagir simultanément dans un même monde contigu. Dans Kiwano nous utilisons la triangulation de Delaunay pour fournir à chaque avatar un nombre constant de voisins en moyenne, indépendamment de leur densité ou distribution géographique. Le nombre d'interactions entre les avatars et les calculs inhérents sont bornés, ce qui permet le passage à l'échelle du système.La charge est repartie sur plusieurs machines qui regroupent sur un même nœud les avatars voisins de façon contiguë dans le graphe de Delaunay. L'équilibrage de la charge se fait de manière contiguë et dynamique, en suivant la philosophie des réseaux pair-à-pair (peer-to-peer overlays). Cependant ce principe est adapté au contexte de l'informatique dématérialisée (cloud computing).Le nombre optimal d'avatars par CPU et les performances de notre système ont été évalués en simulant des dizaines de milliers d'avatars connectés à la même instance de Kiwano tournant à travers plusieurs centres de traitement de données.Nous proposons également trois applications concrètes qui utilisent Kiwano : Manycraft est une architecture distribuée capable de supporter un nombre arbitrairement grand d'utilisateurs cohabitant dans le même espace Minecraft, OneSim, qui permet à un nombre illimité d'usagers d'être ensemble dans la même région de Second Life et HybridEarth, un monde en réalité mixte où avatars et personnes physiques sont présents et interagissent dans un même espace: la Terre. / Virtual worlds attract millions of users and these popular applications --supported by gigantic data centers with myriads of processors-- are routinely accessed. However, surprisingly, virtual worlds are still unable to host simultaneously more than a few hundred users in the same contiguous space.The main contribution of the thesis is Kiwano, a distributed system enabling an unlimited number of avatars to simultaneously evolve and interact in a contiguous virtual space. In Kiwano we employ the Delaunay triangulation to provide each avatar with a constant number of neighbors independently of their density or distribution. The avatar-to-avatar interactions and related computations are then bounded, allowing the system to scale. The load is constantly balanced among Kiwano's nodes which adapt and take in charge sets of avatars according to their geographic proximity. The optimal number of avatars per CPU and the performances of our system have been evaluated simulating tens of thousands of avatars connecting to a Kiwano instance running across several data centers, with results well beyond the current state-of-the-art.We also propose Kwery, a distributed spatial index capable to scale dynamic objects of virtual worlds. Kwery performs efficient reverse geolocation queries on large numbers of moving objects updating their position at arbitrary high frequencies. We use a distributed spatial index on top of a self-adaptive tree structure. Each node of the system hosts and answers queries on a group of objects in a zone, which is the minimal axis-aligned rectangle. They are chosen based on their proximity and the load of the node. Spatial queries are then answered only by the nodes with meaningful zones, that is, where the node's zone intersects the query zone.Kiwano has been successfully implemented for HybridEarth, a mixed reality world, Manycraft, our scalable multiplayer Minecraft map, and discussed for OneSim, a distributed Second Life architecture. By handling avatars separately, we show interoperability between these virtual worlds.With Kiwano and Kwery we provide the first massively distributed and self-adaptive solutions for virtual worlds suitable to run in the cloud. The results, in terms of number of avatars per CPU, exceed by orders of magnitude the performances of current state-of-the-art implementations. This indicates Kiwano to be a cost effective solution for the industry. The open API for our first implementation is available at \url{http://kiwano.li}.