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.

Cette thèse s’intéresse à la gestion décentralisée à l’aide des systèmes multi-agents de l’énergie, notamment de sources renouvelables, dans le contexte des réseaux électriques intelligents (smart grids). Nos travaux de recherche visent à minimiser la facture énergétique des consommateurs en se focalisant sur deux verrous essentiels que nous nous proposons de lever : (1) résoudre le problème de l’intermittence des énergies renouvelables; (2) minimiser les pertes d’énergie. Pour pallier le problème d’intermittence des énergies renouvelables et dans le but de maintenir un coût énergétique peu onéreux même lors des pics d’utilisation, nous avons intégré un système de stockage intelligent. Nous avons, en effet, proposé des algorithmes permettant d’utiliser les systèmes de stockage intelligents et la négociation multi-agents pour réduire la facture énergétique tout en conservant un taux de décharge minimal de la batterie et une perte énergétique minimale. La validation par simulation de nos contributions a montré que celles-ci répondent aux enjeux identifiés, notamment en réduisant le coût de l’énergie pour les consommateurs en comparaison aux travaux de l’état de l’art. / This thesis focuses on the decentralized management using multi-agent systems of energy, including renewable energy sources, in the smart grid context. Our research aims to minimize consumers’ energy bills by answering two key challenges: (1) handle the problem of intermittency of renewable energy sources; (2) reduce energy losses. To overcome the problem of renewable resources intermittency and in order to minimize energy costs even during peak hours, we integrated an intelligent storage system. To this end, we propose many algorithms in order to use intelligent storage systems and multi-agent negotiation algorithm to reduce energy cost while maintaining a minimal discharge rate of the battery and minimal energy loss. The validation of our contributions has shown that our proposals respond to the identified challenges, including reducing the cost of energy for consumers, in comparison to the state of the art.

Cette étude développe une plate-forme mathématique allant de la création d’une base de connaissances à la mise en place d’un modèle adaptatif. Une nouvelle approche en ce qui concerne la modélisation du four rotatif du clinker a été nécessaire pour mener à bien notre étude. Ainsi, un modèle d’état du système aux paramètres repartis, à la base des phénomènes physico-chimiques, a été conçu à l’aide d’équations aux dérivées partielles. La structure du modèle est basée sur trois variables d’état qui peuvent décrire correctement les principaux phénomènes (diffusions, déplacements, transferts et échanges thermiques, etc.) qui se déroulent dans le four rotatif de clinker. En outre, ces variables d’état sont accessibles à travers des paramètres mesurables tels que les températures de la surface extérieure du four et de l’air ambiant. Les paramètres du modèle proposé sont des fonctions de trois variables d’état, qui tout en remplaçant les paramètres mal connus et inaccessibles, décrivent les phénomènes physicochimiques qui caractérisent la complexité du système et sont définis comme des fonctions opératoires. Cette approche permet non seulement de minimiser les erreurs (hypothèse de simplification) mais aussi permet un accès facile et aisé des paramètres. Nous avons élaboré une procédure d’identification basée sur des analyses phénoménologique et dimensionnelle. Ainsi, à partir de données issues d’un complément d’instrumentation associé à la base de connaissances, l’identification des fonctions opératoires (paramètres) a été effectuée à partir d’un état stationnaire du système qui représente notre condition initiale. Cette opération est importante dans la mesure où elle donne aux paramètres du modèle les propriétés de la dynamique du système. Ces résultats sont corroborés par les estimations des variables d’état dont les valeurs et évolutions sont acceptables. Après l’évaluation de l’influence des fonctions opératoires sur les variables d’état, une modélisation des paramètres (fonctions opératoires) du modèle a été proposée à la base d’une décomposition physique à la lumière des connaissances fournies dans la littérature. Une procédure d’ajustement a été également développée afin de pouvoir fournir des variables d’état optimales. Ainsi, l’erreur peut être compensée par ajustement des fonctions opératoires. Par conséquent, à travers la rapidité de la procédure d’ajustement et l’adaptation des paramètres du modèle dans un horizon de temps bien déterminé, le modèle renferme les caractéristiques d’un modèle adaptatif qui pourra être un support essentiel dans la commande automatique du système. / This study develops a mathematical platform going from the establishment of a knowledge database to the setting up of an adaptive model. This has required a new approach of modeling of the clinker rotary kiln (CRK). Thus, a state model of distributed parameter systems, based on physico-chemical phenomena, was designed using partial differential equations. The model structure is based on three state variables which are: the gas, clinker temperatures and the clinker mass distributions, and are elaborated with the help of heat, pressure and mass balance equations. The model parameters are defined by the functions of three state variables. Moreover, the resulting state model, decomposed into five phenomenological zones of CRK, is used as a first step to define a set of Operating Functions (OFs). These OFs has also been decomposed into longitudinal distribution of CRK to replace the constant, unknown or unmeasured parameters. We develop an identification procedure based on phenomenological and dimensional analysis where the identification of operational functions (model parameters) was performed from a stationary state of the CRK. Once the restores state variables have been evaluated, the desired input (which is treated as the control of the CRK) can be more easily found by the proposed model than by simple trial and error. Moreover, the fact that the computation time, to estimate-calibrate the OFs above-mentioned, is very short, then this dynamic computation works faster than real-time. In summary, the cooperation and coordination in real-time between industrial computers and the CRK allows for an adaptable model, where each specific set of the OFs must be analyzed by its accuracy.

Cette thèse développe des modèles d'évaluation de performance d'une ligne de production composée de machines non fiables sujettes à plusieurs modes de défaillances, ou pouvant opérer en fonctionnement dégradé. Ces machines sont dites multi-états et sont séparées par de stocks intermédiaires de capacités finies. On considère que le fonctionnement dégradé affecte uniquement le taux de production nominal des machines de la ligne et non la qualité des pièces produites. Un modèle continu est utilisé pour décrire le débit d'une machine et le niveau d'un stock. Chaque mode de défaillance est caractérisé par ses propres temps de bon fonctionnement et de réparation. Ces temps sont considérés comme des variables aléatoires exponentiellement distribuées. Les modèles proposés permettent l'évaluation de performances de longues lignes de production en procédant par agrégation de machines. Cette technique consiste à évaluer les paramètres d'une machine équivalente pouvant se substituer à un ensemble constitué d'un stock et des deux machines qui l'encadrent. Ainsi, une machine équivalente à la ligne complète est évaluée de proche en proche. Afin de valider les modèles proposés, les résultats analytiques obtenus sont comparés avec des résultats de simulation. Pour cela, nous avons développé un outil de simulation appelé « ProdLineSim ». Dans le cas de machines sujettes à plusieurs modes de défaillances, les résultats de simulation ont montré qu'en tenant compte de manière explicite des différents modes de défaillances de chaque machine, la méthode proposée permet une évaluation de performance plus précise qu'en ne considérant, pour chaque machine, qu'un seul mode de défaillance. Dans le cas de machines pouvant opérer en fonctionnement dégradé, les résultats de simulation ont aussi montré qu'en tenant compte de manière explicite de ce fonctionnement dégradé, la méthode proposée permet une évaluation de performance plus précise.

Ce travail se situe dans le cadre de la commande des systèmes à paramètres répartis régis par des équations aux dérivées partielles non linéaires. On cherche ici à élargir l'utilisation de la stratégie de commande prédictive du cadre classique de systèmes décrits par des équations différentielles ordinaires à celui où les systèmes sont décrits par une classe d'équations non linéaires aux dérivées partielles (EDP). L'intérêt de l'utilisation de la stratégie de commande prédictive est de pouvoir résoudre divers problèmes de conduite tout en tenant compte explicitement de diverses contraintes de fonctionnement. Nous avons choisi une démarche qui a consisté à considérer directement des cas réels issus du Génie des Procédés, où de nombreux modèles de connaissance sont décrits par des EDP fortement non linéaires : un procédé de séchage de peinture par infrarouge (donnant lieu à une application réelle), un procédé de fabrication de matériau composite et un procédé de destruction de gaz polluants par catalyse. La particularité de ce travail concerne le fait de proposer une structure adaptée de commande prédictive par modèle interne, celui-ci étant déterminé autour d'une trajectoire soit prédéfinie, soit générée en tenant compte de diverses contraintes de fonctionnement. Dans le contexte de résolution du problème d'optimisation posé par l'approche prédictive, nous proposons un algorithme hors-ligne (génération de trajectoire) et un autre en ligne.

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