Guide est un système d'exploitation expérimental reparti sur un réseau local. Les informations qu'il manipule sont structurées selon un modelé à objets. La description de l'un des composants de la machine virtuelle réalisant la gestion d'objets, a savoir la mémoire d'objets, est proposée. Sont présentés les choix de conception, sa réalisation et une analyse de l'expérience acquise. La mémoire d'objets est repartie et comporte deux niveaux: la mémoire virtuelle d'objets, qui constitue le support d'exécution des objets et la mémoire permanente d'objets, qui se charge de leur conservation

Etude des systèmes d'exploitation de quelques systèmes repartis universitaires ou industriels et comparaison à CHORUS. Exposé des principes généraux d'implantation du système d'exploitation CHORUS, de l'architecture du système d'exploitation et ses relations avec les applications. Présentation d'une implantation réelle écrite en Pascal sur des microprocesseurs Intel 8086; étude des principales difficultés rencontrées d'une part avec le système de développement choisi, d'autre part avec le langage; l'aspect spécifiquement matériel n'est pas abordé. Bilan de cette expérience

Les moyens de traitement de l'information auxquels nous avons accès sont de plus en plus puissants, de plus en plus répartis. Des modèles de programmation, tels que la multiprogrammation légère ou la programmation par objets, leur sont appliqués afin de juguler l'accroissement de la complexité qui en découle. Mais qu'apportent ces modèles ? La mise en oeuvre de ces modèles permet-elle d'employer au "mieux" les ressources disponibles ? Pour répondre à cette question, nous nous plaçons dans une démarche de type "évaluation de performances". La problématique porte sur la reconstruction post-mortem, à partir de mesures, de la dynamique d'une exécution afin de réaliser une analyse qualitative et quantitative des ressources d'exécution consommées. L'hypothèse posée est que l'analyse des interactions entre objets, effectuée à différents niveaux d'abstraction, procure les informations suffisantes à nos études. Pour cela, nous réalisons des observations au niveau applicatif el système et cela sans modification du code exécutable original de l'application ou du noyau du système d'exploitation. Une infrastructure d'observation multi-niveaux a été réalisée dans le cadre d'applications Java réparties. Elle a été appliquée à l'étude d'un serveur multimédia Java. Une analyse de l'algorithmique et des consommations de ressources systèmes a été menée. Pour cela, les observations du niveau applicatif sont effectuées au travers de la JVMPI. Le coût moyen d'observation est de 3µs par point de mesure. Celles du niveau système sont obtenues par insertion à chaud d'un module dans un noyau Linux. De cette façon, les appels systèmes attachés aux écritures et aux lectures dans une "socket" sont déroutés. II nous est ainsi possible de reconstruire les interactions distantes entre objets Java et d'obtenir des indices de consommation des ressources systèmes. Le coût moyen d'observation est ici de 2µs par point de mesure.

L'importante augmentation de la quantité d'informations sur Internet a contribué à une forte demande pour un stockage persistant des données. Les architectures centralisées de stockage de données sont financièrement onéreuses, faiblement évolutives et vulnérables aux attaques car elles constituent un point unique de défaillance du système. Ces dernières années, les architectures pair-à-pair ont mergé comme une alternative pour la mise en place d'une architecture de stockage persistant des données. Les systèmes pair-à-pair sont fondamentalement évolutifs et moins chers que les modèles client-serveur. Cependant, pour construire des systèmes de stockage persistant en utilisant le modèle pair-à-pair, deux défis fondamentaux doivent être abordés. i) Faire face à la dynamique des pairs, en raison de leur connectivité transitoire. ii) Réduire l'impact du comportement malicieux des pairs. La réplication est une technique régulièrement utilisée pour faire face à la connectivité transitoire des systèmes de stockage pair-à-pair. Toutefois, selon le ratio d'arrivées et de départs des pairs dans le système, cette technique présente un impact négatif en termes de stockage et de bande passante. Les réseaux pair-à-pair qui offrent la tolérance aux fautes byzantins, font généralement l'hypothèse que seulement une fraction limitée des pairs dans le système sont des pairs de comportements malveillants. Toutefois, l'estimation de la proportion de pairs malveillants dans un système pair-à-pair est une opération peu fiable. Ainsi, créer une architecture qui fournit le stockage persistant de données fiables et qui permet de faire face à tous ces problèmes est une contribution souhaitable. Dans cette thèse, nous proposons Datacube. Datacube est une architecture pair-à-pair de stockage de données scalable et efficace qui fournit un stockage persistant en utilisant un schéma de redondance hybride sur un réseau overlay structuré basée sur des clusters. Le schéma de redondance hybride proposé par Datacube assure la persistance et l'intégrité des données garantissant une forte résilience aux arrivées et départs de pairs même en présence de pairs malveillants. Datacube repose sur les propriétés des codes fontaines pour mettre en place son schéma de redondance hybride. Les valuations analytiques ont montré que Datacube est notamment performant en termes de disponibilité, de surcharge de stockage et de bande passante. Nous avons aussi effectué des évaluations pratiques concernant les performances de deux types de codes fontaines dans le contexte de systèmes de stockage pair-à-pair. Ces évaluations ont aidé à comprendre l'impact des paramètres de codage sur les performances de Datacube. À notre connaissance, ceci est la première étude complète qui permet aux développeurs d'applications de trouver les valeurs des paramètres de codage adaptés au contexte des réseaux pair-à-pair.

Dans les systèmes répartis asynchrones, l'horloge logique et le vecteur d'horloges sont deux outils fondamentaux pour gérer la communication et le partage de données entre les entités constitutives de ces systèmes. L'objectif de cette thèse est d'exploiter ces outils avec une perspective d'implantation. Dans une première partie, nous nous concentrons sur la communication de données et contribuons au domaine de la diffusion uniforme à ordre total. Nous proposons le protocole des trains : des jetons (appelés trains) circulent en parallèle entre les processus participants répartis sur un anneau virtuel. Chaque train est équipé d'une horloge logique utilisée pour retrouver les train(s) perdu(s) en cas de défaillance de processus. Nous prouvons que le protocole des trains est un protocole de diffusion uniforme à ordre total. Puis, nous créons une nouvelle métrique : le rendement en termes de débit. Cette métrique nous permet de montrer que le protocole des trains a un rendement supérieur au meilleur, en termes de débit, des protocoles présentés dans la littérature. Par ailleurs, cette métrique fournit une limite théorique du débit maximum atteignable en implantant un protocole de diffusion donné. Il est ainsi possible d'évaluer la qualité d'une implantation de protocole. Les performances en termes de débit du protocole des trains, notamment pour les messages de petites tailles, en font un candidat remarquable pour le partage de données entre coeurs d'un même processeur. De plus, sa sobriété en termes de surcoût réseau en font un candidat privilégié pour la réplication de données entre serveurs dans le cloud. Une partie de ces travaux a été implantée dans un système de contrôle-commande et de supervision déployé sur plusieurs dizaines de sites industriels. Dans une seconde partie, nous nous concentrons sur le partage de données et contribuons au domaine de la RFID. Nous proposons une mémoire répartie partagée basée sur des étiquettes RFID. Cette mémoire permet de s'affranchir d'un réseau informatique global. Pour ce faire, elle s'appuie sur des vecteurs d'horloges et exploite le réseau formé par les utilisateurs mobiles de l'application répartie. Ainsi, ces derniers peuvent lire le contenu d'étiquettes RFID distantes. Notre mémoire répartie partagée à base de RFID apporte une alternative aux trois architectures à base de RFID disponibles dans la littérature. Notre mémoire répartie partagée a été implantée dans un jeu pervasif qui a été expérimenté par un millier de personnes.

Avec l'émergence de plates-formes distribuées très hétérogènes, dynamiques et à large échelle, la nécessité d'un moyen de les programmer efficacement et de les gérer est apparu. Le concept de l'informatique autonomique propose de créer des systèmes auto-gérés c'est-à-dire des systèmes qui sont conscients de leurs composants et de leur environnement, et peuvent se configurer, s'optimiser, se réparer et se protéger. Dans le cadre de la réalisation de tels systèmes, la programmation déclarative, dont l'objectif est de faciliter la tâche du programmeur en séparant le contrôle de la logique du calcul, a retrouvé beaucoup d'intérêt ces derniers temps. En particulier, la programmation à base de des règles est considérée comme un modèle prometteur dans cette quête d'abstractions de programmation adéquates pour ces plates-formes. Cependant, bien que ces modèles gagnent beaucoup d'attention, ils créent une demande pour des outils génériques capables de les exécuter à large échelle. Le modèle de programmation chimique, qui a été conçu suivant la métaphore chimique, est un modèle de programmation à bas de règles et d'ordre supérieur, avec une exécution non-déterministe, où les règles sont appliquées de façon concurrente sur un multi ensemble de données. Dans cette thèse, nous proposons la conception, le développement et l'expérimentation d'un intergiciel distribué pour l'exécution de programmes chimique sur des plates-formes à large échelle et génériques. L'architecture proposée combine une couche de communication pair-à-pair avec un protocole de capture atomique d'objets sur lesquels les règles doivent être appliquées, et un système efficace de détection de terminaison. Nous décrivons le prototype d'intergiciel mettant en oeuvre cette architecture. En s'appuyant sur son déploiement sur une plate-forme expérimentale à large échelle, nous présentons les résultats de performance, qui confirment les complexités analytiques obtenues et montrons expérimentalement la viabilité d'un tel modèle de programmation.

Cette thèse porte sur l'étude des techniques de fusion de données réparties et incertaines au sein d'un réseau de véhicules pour gérer la confiance dans les autres véhicules ou dans les données reçues. L'algorithme de fusion distribuée proposé est basé sur les fonctions de croyance et est appliqué par chaque nœud à la réception des messages. In se base sur la gestion d'une connaissance directe, locale à chaque nœud et d'une connaissance distribuée diffusée dans le réseau. Cette dernière résulte de la fusion des messages par un opérateur adapté prenant en compte les cycles éventuels et limitant l'effet de "data incest". Chaque nœud peut être autonome pour estimer la confiance mais la coopération entre les véhicules permet d'améliorer et de rendre plus robuste cette estimation. L'algorithme peut être adapté au cas d'étude en considérant un ou plusieurs éléments d'observation et en prenant en compte l'obsolescence des données. Lorsqu'il y a plusieurs éléments d'observation, se pose le problème de l'association de données nécessaire avant l'étape de combinaison. Un nouvel algorithme d'association a été formalisé dans le cadre des fonctions de croyance. Il a été démontré que ce problème est équivalent à un problème d'affectation linéaire, qui peut être résolu en temps polynomial. Cette solution est à la fois optimale et beaucoup plus efficace que d'autres approches développées dans ce formalisme. La gestion de la confiance dans les nœuds et dans les données échangées ont été illustrées par la mise en œuvre de deux applications : la détection de faux nœuds dans une attaque Sybil et la gestion de la confiance dans les cartes dynamiques pour la perception augmentée.

Les systèmes informatiques sont construits par composition de plusieurs sous-systèmes répartis. La manière dont communiquent ces entités, ou pairs, joue un rôle clé dans la bonne marche du système composé. L'étude détaillée de ces interactions est donc essentielle dans le cadre de la vérification et du développement formel de tels systèmes. Ces interactions se décomposent en deux catégories: la communication synchrone et la communication asynchrone. La communication synchrone admet une transmission instantanée de l'information, le message, entre deux entités. La communication asynchrone, en revanche, prend en compte le découplage de la transmission du message en une opération d'envoi puis de réception avec la possibilité que des événements s'intercalent entre les deux donnant ainsi lieu à des variations de comportement, désirables ou non, des systèmes. Souvent considérée comme une entité monolithique duale du monde synchrone, le monde asynchrone se décline en réalité en de multiples modèles qui peuvent induire sur la communication une grande variété de propriétés qu'il convient de caractériser et comparer. Cette thèse se focalise sur les modèles de communication qui orchestrent l'ordre de délivrance des messages : par exemple les modèles dits FIFO qui assurent que certains messages sont reçus dans l'ordre dans lequel ils ont été émis. Nous considérons des modèles de communication classiques de la littérature ainsi que des variations de ces modèles dont nous explicitons les différences parfois négligées. Dans un premier temps nous proposons une formalisation logique abstraite et homogène des modèles de communication considérés et nous les hiérarchisons en étendant des résultats existants. Nous proposons dans un second temps une approche opérationnelle sous forme d'un outil de vérification de compositions de pairs que nous mécanisons à l'aide du langage de spécification TLA+ et du vérificateur de modèles TLC. Cet outil permet de spécifier des pairs communicants et des propriétés temporelles à vérifier pour les différents modèles de communication de façon modulaire. Pour cela, nous apportons un ensemble de spécifications uniformes et opérationnelles des modèles de communication basé sur la notion d'histoires de messages. Nous identifions et prouvons les conditions de leur conformité aux définitions logiques et validons ainsi la pertinence de notre outil. Dans un troisième temps nous considérons des spécifications concrètes de nos modèles de communication, semblables à nombre de celles présentes dans la littérature. Nous disposons donc d'une hiérarchisation des modèles selon les propriétés d'ordre qu'ils garantissent mais également d'une autre hiérarchisation pour un modèle donné entre sa définition logique abstraite et ses implantations concrètes. Ces deux dimensions correspondent à deux dimensions du raffinement. Nous introduisons graduellement par raffinement la notion de communication asynchrone point à point et prouvons, grâce à la méthode Event-B, tous les liens de raffinement entre les différents modèles de communication et leurs déclinaisons. Nous offrons ainsi une cartographie détaillée des modèles pouvant être utilisée pour en développer de nouveaux ou identifier les modèles les plus adaptés à des besoins donnés. Enfin, nous proposons des pistes d'extension de nos travaux à la communication par diffusion où un message peut être envoyé simultanément à plusieurs destinataires. En particulier, nous montrons les différences induites dans la hiérarchie des modèles et les adaptations à effectuer sur notre outil de vérification pour prendre en compte ce mode de communication / Large computing systems are generally built by connecting several distributed subsystems. The way these entities communicate is crucial to the proper functioning of the overall composed system. An in-depth study of these interactions makes sense in the context of the formal development and verification of such systems. The interactions fall in two categories: synchronous and asynchronous communication. In synchronous communication, the transmission of a piece of information - the message - is instantaneous. Asynchronous communication, on the other hand, splits the transmission in a send operation and a receive operation. This make the interleaving of other events possible and lead to new behaviours that may or may not be desirable. The asynchronous world is often viewed as a monolithic counterpart of the synchronous world. It actually comes in multiple models that provide a wide range of properties that can be studied and compared. This thesis focuses on communication models that order the delivery of messages: for instance, the "FIFO" models ensure that some messages are received in the order of their emission. We consider classic communication models from the literature as well as a few variations. We highlight the differences that are sometimes overlooked. First, we propose an abstract, logical, and homogeneous formalisation of the communication models and we establish a hierarchy that extends existing results. Second, we provide an operational approach with a tool that verifies the compatibility of compositions of peers. We mechanise this tool with the TLA+ specification language and its model checker TLC. The tool is designed in a modular fashion: the commmunicating peers, the temporal compatibility properties, and the communication models are specified independently. We rely on a set of uniform operational specifications of the communication models that are based on the concept of message history. We identify and prove the conditions under which they conform to the logical definitions and thus show the tool is trustworthy. Third, we consider concrete specifications of the communication models that are often found in the literature. Thus, the models are classified in terms of ordering properties and according to the level of abstraction of the different specifications. The concept of refinement covers these two aspects. Thus, we model asynchronous point-to-point communication along several levels of refinement and then, with the Event-B method, we establish and prove all the refinements between the communication models and the alternative specifications of each given model. This work results in a detailed map one can use to develop a new model or find the one that best fits given needs. Eventually we explore ways to extend our work to multicast communication that consists in sending messages to several recipients at once. In particular, we highlight the differences in the hierarchy of the models and how we modify our verification tool to handle this communication paradigm.

L'objectif de cette thèse est d'offrir une solution de bout en bout permettant de décrire et de déployer de façon fiable une application distribuée dans un environnement virtualisé. Ceci passe par la définition d'un formalisme permettant de décrirer une application ainsi que son environnement d'exécution, puis de fournir les outils capable d'interpéter ce formalisme pour déployer (installer, instancier et configurer) l'application sur une plate-forme de type cloud computing. / Cloud computing aims to cut down on the outlay and operational expenses involved in setting up and running applications. To do this, an application is split into a set of virtualized hardware and software resources. This virtualized application can be autonomously managed, making it responsive to the dynamic changes affecting its running environment. This is referred to as Application Life-cycle Management (ALM). In cloud computing, ALM is a growing but immature market, with many offers claiming to significantly improve productivity. However, all these solutions are faced with a major restriction: the duality between the level of autonomy they offer and the type of applications they can handle. To address this, this thesis focuses on managing the initial deployment of an application to demonstrate that the duality is artificial. The main contributions of this work are presented in a platform named VAMP (Virtual Applications Management Platform). VAMP can deploy any legacy application distributed in the cloud, in an autonomous, generic and reliable way. It consists of: • a component-based model to describe the elements making up an application and their projection on the running infrastructure, as well as the dependencies binding them in the applicative architecture; • an asynchronous, distributed and reliable protocol for self-configuration and self-activation of the application; • mechanisms ensuring the reliability of the VAMP system itself. Beyond implementing the solution, the most critical aspects of running VAMP have been formally verified using model checking tools. A validation step was also used to demonstrate the genericity of the proposal through various real-life implementations.

Réseaux locaux, quelques structures. Principes du mecanisme de communication. Implémentation du mecanisme de communication. Réalisation du coupleur