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 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.

La conception des systèmes distribués est une tâche onéreuse : les objectifs de performance, d’exactitude et de fiabilité sont étroitement liés et ont donné naissance à des compromis complexes décrits par de nombreux résultats théoriques. Ces compromis sont devenus de plus en plus importants à mesure que le calcul et le stockage se sont déplacés vers des architectures distribuées. De plus, l’absence d’approches systématiques de ces problèmes dans les outils de programmation modernes les a aggravés — d’autant que de nos jours la plupart des programmeurs doivent relever les défis liés aux applications distribués. En conséquence, il existe un écart évident entre les abstractions de programmation, les exigences d’application et la sémantique de stockage, ce qui entrave le travail des concepteurs et des développeurs. Cette thèse présente un ensemble de contributions tourné vers la conception de systèmes de stockage distribués fiables, en examinant ces questions à travers le prisme de la cohérence. Nous commençons par fournir un cadre uniforme et déclarative pour définir formellement les modèles de cohérence. Nous utilisons ce cadre pour décrire et comparer plus de cinquante modèles de cohérence non transactionnelles proposés dans la littérature. La nature déclarative et composite de ce cadre nous permet de construire un classement partiel des modèles de cohérence en fonction de leur force sémantique. Nous montrons les avantages pratiques de la composabilité en concevant et en implémentant Hybris, un système de stockage qui utilise différents modèles pour améliorer la cohérence faible généralement offerte par les services de stockage dans les nuages. Nous démontrons l’efficacité d’Hybris et montrons qu’il peut tolérer les erreurs arbitraires des services du nuage au prix des pannes. Enfin, nous proposons une nouvelle technique pour vérifier les garanties de cohérence offertes par les systèmes de stockage du monde réel. Cette technique s’appuie sur notre approche déclarative de la cohérence : nous considérons les modèles de cohérence comme invariants sur les représentations graphiques des exécutions des systèmes de stockage. Une mise en œuvre préliminaire prouve cette approche pratique et utile pour améliorer l’état de l’art sur la vérification de la cohérence. / Engineering distributed systems is an onerous task: the design goals of performance, correctness and reliability are intertwined in complex tradeoffs, which have been outlined by multiple theoretical results. These tradeoffs have become increasingly important as computing and storage have shifted towards distributed architectures. Additionally, the general lack of systematic approaches to tackle distribution in modern programming tools, has worsened these issues — especially as nowadays most programmers have to take on the challenges of distribution. As a result, there exists an evident divide between programming abstractions, application requirements and storage semantics, which hinders the work of designers and developers.This thesis presents a set of contributions towards the overarching goal of designing reliable distributed storage systems, by examining these issues through the prism of consistency. We begin by providing a uniform, declarative framework to formally define consistency semantics. We use this framework to describe and compare over fifty non-transactional consistency semantics proposed in previous literature. The declarative and composable nature of this framework allows us to build a partial order of consistency models according to their semantic strength. We show the practical benefits of composability by designing and implementing Hybris, a storage system that leverages different models and semantics to improve over the weak consistency generally offered by public cloud storage platforms. We demonstrate Hybris’ efficiency and show that it can tolerate arbitrary faults of cloud stores at the cost of tolerating outages. Finally, we propose a novel technique to verify the consistency guarantees offered by real-world storage systems. This technique leverages our declarative approach to consistency: we consider consistency semantics as invariants over graph representations of storage systems executions. A preliminary implementation proves this approach practical and useful in improving over the state-of-the-art on consistency verification.

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

La présente étude porte sur la capacité d'améliorer la détection des Activités de la Vie Quotidienne, AVQ (ou ADL :"Activity of Daily Life") par l'utilisation de capteur [i.e. capteurs] de mouvements portés par l'occupant d'un habitat intelligent. Les données provenant de ces capteurs devraient fusionner avec les informations issues de l'appartement pour donner une information plus pertinente par le principe de synergie [21]. La solution choisie pour le dispositif porté par la personne est l'innovation principale du projet : un réseau de capteurs disposés à plusieurs endroits sur le corps, communicant sans fil entre eux et avec le contrôle de l'appartement. Les données extraites sont le mouvement relatif du corps, et plus spécifiquement des mains et du tronc, par rapport à la verticale. De par les propriétés de ces éléments - nécessairement petits, discrets - des MEMS seront utilisés pour satisfaire ces critères. Le projet repose sur la conception des dispositifs embarqués sur l'occupant dans l'optique d'en étendre les fonctionnalités à d'autres analyses tels [i.e. telles] que le son, la position dans l'environnement, le statut médical, etc. Pour prouver la faisabilité, des capteurs externes seront ajoutés pour compléter les informations de base et donc étendre la qualité des inférences sur les activités en cours. Le mouvement est une donnée facilement détectable de par sa relative simplicité de mise en oeuvre et il fournit une bonne base de travail pour étudier de façon systématique les différents points clés de l'étude : la communication, la synergie des informations, l'analyse des activités, etc.

Les automates d'ordres, plus connus sous le nom de Message sequence Charts (MSC), ont connu une énorme popularité depuis les années 1990. Ce succès est à la fois académique et industriel. Les raisons de ce succès sont multiples : le modèle est simple et s'apprend très vite. De plus il possède une puissance d'expression supérieure à celle des automates finis, et pose des problèmes difficiles. L'apparente simplicité des MSCs est en fait trompeuse, et de nombreuses manipulations algorithmiques se révèlent rapidement être des problèmes indécidables. Dans ce document, nous revenons sur 10 années de recherches sur les Message Sequence Charts, et plus généralement sur les langages de scénarios, et tirons quelques conclusions à partir des travaux effectués. Nous revenons sur les propriétés formelles des Message Sequence charts, leur décidabilité, et les sous-classes du langage permettant la décision de tel ou tel problème. L'approche classique pour traiter un problème sur les MSCs est de trouver la plus grande classe possible sur laquelle ce problème est décidable. Un autre challenge est d'augmenter la puissance d'expression des MSCs sans perdre en décidabilité. Nous proposons plusieurs extensions de ce type, permettant la crétion dynamique de processus, ou la définition de protocoles de type "fenêtre glissante". Comme tout modèle formel, les MSCs peuvent difficilement dépasser une taille critique au delà de laquelle un utilisateur ne peut plus vraiment comprendre le diagramme qu'il a sous les yeux. Pour pallier à cette limite, une solution est de travailler sur de plus petits modules comportementaux, puis de les assembler pour obtenir des ensembles de comportements plus grands. Nous étudions plusieurs mécanismes permettant de composer des MSCs, et sur la robustesses des sous-classes de scénarios connues à la composition. La conclusion ce cette partie est assez négative: les scénarios se composent difficilement, et lorsqu'une composition est faisable, peu de propriétés des modèles composés sont préservées. Nous apportons ensuite une contributions à la synthèse automatique de programmes distribués à partir de spécification données sous forme d'automates d'ordres. Cette question répond à un besoin pratique, et permet de situer un role possible des scénarios dans des processus de conception de logiciels distribués. Nous montrons que la synthèse automatique est possible sur un sous ensemble raisonnable des automates d'ordres. Dans une seconde partie de ce document, nous étudions des applications possibles pour les MSCs. Nous regardons entre autres des algorithmes de model-checking, permettant de découvrir des erreurs au moment de la spécification d'un système distribué par des MSCs. La seconde application considérée est le diagnostic, qui permet d'expliciter à l'aide d'un modèle les comportement d'un système réel instrumenté. Enfin, nous regardons l'utilisation des MSCs pour la recherche de failles de sécurité dans un système. Ces deux applications montrent des domaines réalistes d'utilisation des scénarios. Pour finir, nous tirons quelques conclusions sur les scénarios au regard du contenu du document et du travail de ces 10 dernières années. Nous proposons ensuite quelques perspectives de recherche.

La vérification de propriétés de sûreté des logiciels distribués basés sur des canaux fifo non bornés et fiables mène directement au model checking de systèmes infinis. Nous introduisons la famille des (q)ueueing (c)oncurrent (p)rocesses (QCP) composant des systèmes de transitions locaux, par exemple des automates finis/à pile, qui communiquent entre eux par des files fifo. Le problème d'atteignabilité des états de contrôle est indécidable pour des automates communicants et des automates à plusieurs piles, et par conséquent pour QCP.Nous présentons deux solutions pour contourner ce résultat négatif :Primo, une sur-approximation basée sur l'approche abstraire-tester-raffiner qui s'appuie sur notre nouveau concept de raffinement par chemin. Cette approche mène à permettre d'écrire un semi-algorithme du type CEGAR qui est implémenté avec des QDD et réalisé dans le framework McScM dont le banc d'essai conclut notre présentation.Secundo, nous proposons des restrictions pour les QCP à des piles locales pour démêler l'interaction causale entre les données locales (la pile), et la synchronisation globale. Nous montrons qu'en supposant qu'il existe une borne existentielle sur les exécutions et qu'en ajoutant une condition sur l'architecture, qui entrave la synchronisation de deux piles, on arrive à une réponse positive pour le problème de décidabilité de l'atteignabilité qui est EXPTime-complet (et qui généralise des résultats déjà connus). La construction de base repose sur une simulation du système par un automate à une pile équivalent du point de vue de l'atteignabilité --- sous-jacente, nos deux restrictions restreignent les exécutions à une forme hors-contexte. Nous montrons aussi que ces contraintes apparaissent souvent dans des situations ``concrètes''et qu'elles sont moins restrictives que celles actuellement connues. Une autre possibilité pour arriver à une solution pratiquement utilisable consiste à supposer une borne du problème de décidabilité : nous montrons que l'atteignabilité par un nombre borné de phases est décidable par un algorithme constructif qui est 2EXPTime-complet.Finalement, nous montrons qu'élargir les résultats positifs ci-dessus à la vérification de la logique linéaire temporelle demande soit de sacrifier l'expressivité de la logique soit d'ajouter des restrictions assez fortes aux QCP --- deux restrictions qui rendent cette approche inutilisable en pratique. En réutilisant notre argument de type ``hors-contexte'', nous représentons l'ordre partiel sous-jacent aux exécutions par des grammaires hypergraphes. Cela nous permet de bénéficier de résultats connus concertant le model checking des formules de la logique MSO sur les graphes (avec largeur arborescente bornée), et d'arriver aux premiers résultats concernant la vérification des propriétés sur l'ordre partiel des automates (à pile) communicants. / The safety verification of distributed programs, that are based on reliable, unbounded fifo communication, leads in a straight line to model checking of infinite state systems. We introduce the family of (q)ueueing (c)oncurrent (p)rocesses (QCP): local transition systems, e.g., (pushdown-)automata, that are globally communicating over fifo channels. QCP inherits thus the known negative answers to the control-state reachability question from its members, above all from communicating automata and multi-stack pushdown systems. A feasible resolution of this question is, however, the corner stone for safety verification.We present two solutions to this intricacy: first, an over-approximation in the form of an abstract-check-refine algorithm on top of our novel notion of path invariant based refinement. This leads to a \cegar semi-algorithm that is implemented with the help of QDD and realized in a small software framework (McScM); the latter is benchmarked on a series ofsmall example protocols. Second, we propose restrictions for QCP with local pushdowns that untangle the causal interaction of local data, i.e., thestack, and global synchronization. We prove that an existential boundedness condition on runs together with an architectural restriction, that impedes the synchronization of two pushdowns, is sufficient and leads to an EXPTime-complete decision procedure (thus subsuming and generalizing known results). The underlying construction relies on a control-state reachability equivalent simulation on a single pushdown automaton, i.e., the context-freeness of the runs under the previous restrictions. We can demonstrate that our constraints arise ``naturally'' in certain classes of practical situations and are less restrictive than currently known ones. Another possibility to gain a practicable solution to safety verification involves limiting the decision question itself: we show that bounded phase reachability is decidable by a constructive algorithms in 2ExpTime, which is complete.Finally, trying to directly extend the previous positive results to model checking of linear temporal logic is not possible withouteither sacrificing expressivity or adding strong restrictions (i.e., that are not usable in practice). However, we can lift our context-freeness argument via hyperedge replacement grammars to graph-like representation of the partial order underlying each run of a QCP. Thus, we can directly apply the well-known results on MSO model checking on graphs (of bounded treewidth) to our setting and derive first results on verifying partial order properties on communicating (pushdown-) automata.