Cette thèse se situe dans la problématique de la conduite en convoi de véhicules autonomes : des ensembles de véhicules qui se déplacent en conservant une configuration spatiale, sans aucune accroche matérielle. Ses objectifs sont d'abord, la définition d'une approche de prise de décision pour les systèmes de convois de véhicules, puis, la définition d'une approche de vérification, adaptée à la preuve de propriétés relatives aux convois de véhicules, avec une attention particulière envers les propriétés de sûreté.L'approche pour la prise de décision est décentralisée et auto organisée : chaque véhicule détermine son comportement de façon locale, à partir de ses propres capacités de perception, sans avoir recours à une communication explicite, de telle sorte que l'organisation du convoi, son maintien et son évolution soient le résultat émergeant du comportement de chaque véhicule. L'approche proposée s'applique a des convois suivant plusieurs types de configuration, et permet des changements dynamiques de configuration.L'approche proposée pour la vérification de propriétés de sûreté des convois de véhicules, adopte le model-checking comme technique de preuve. Pour contourner le problème de l'explosion combinatoire, rencontré dans la vérification des systèmes complexes, nous avons proposé une méthode compositionnelle de vérification, qui consiste a décomposer le système en sous systèmes et à associer une propriété auxiliaire à chacun des sous systèmes. La propriété globale sera ensuite déduite de l'ensemble des propriétés auxiliaires, par l'application d'une règle de déduction compositionnelle. La complexité calculatoire est mieux maîtrisée car le model-checking s'applique aux sous-systèmes. Nous proposons une règle de déduction adaptée aux systèmes de conduite en convoi, en particulier ceux qui sont basés sur des approches décentralisées. La règle considère chaque véhicule comme un composant. Elle est consistante sous la condition que l'ajout d'un nouveau composant au système n'a pas d'influence sur le comportement du reste du système. L'approche décentralisée proposée pour la conduite en convoi satisfait cette condition. Deux propriétés de sûreté ont été vérifiées : absence de collision et évolution confortable pour les passagers

Ce travail s'inscrit dans le cadre du développement de nouveaux procédés de désacidification de gaz naturel à travers l'étude thermodynamique des équilibres entre les gaz acides (CO2 et H2S) et un solvant mixte. Ce solvant résulte de la combinaison d'un solvant chimique (solution aqueuse de diéthanolamine) et d'un solvant physique (méthanol). Couplant équilibres chimique et physique, la modélisation de ces systèmes nécessite l'élaboration de modèles complexes et une large gamme de données d'équilibre liquide-vapeur. La première partie de ce travail est consacrée à l'acquisition de données expérimentales de solubilité des gaz acides dans le solvant mixte. En étendant le champ d'application d'un appareillage fonctionnant en méthode synthétique, nous avons acquis des données originales de solubilité des mélanges CO2 + H2S dans des solvants eau-diéthanolamine-méthanol. Dans la seconde partie, la modélisation simultanée des équilibres chimiques et physiques est réalisée. L'approche hétérogène développée combine le modèle NRTL-Electrolyte pour représenter la phase liquide avec l'équation d'état de Peng-Robinson pour décrire le comportement de la phase vapeur. La procédure d'ajustement des paramètres est graduelle si bien que le système complet eau-diéthanolamine-méthanol-CO2-H2S est décrit de manière prédictive, les paramètres du modèle NRTL-Electrolyte ayant été déterminés sur des systèmes inférieurs. L'effet de solvatation du méthanol est aussi mis en valeur. Nous nous sommes également intéressés au calcul des chaleurs d'absorption et à l'extension de notre modèle à d'autres alcanolamines / This work is related to the development of new processes about gas sweetening with hybrid solvents coupling a chemical one (aqueous solution of diethanolamine) with a physical one (methanol). In the liquid phase, CO2 and H2S react with diethanolamine so that the VLE description of these systems is quite complex and requires experimental data. The first part of this work is dedicated to the experimental determination of acid gases + hybrid solvent solubility data. The experimental apparatus was improved to study H2S solubility and CO2 + H2S mixtures solubility in water-diethanolamine-methanol solvents. In the second part, the simultaneous representation of chemical and phase equilibria was realised. The heterogeneous approach developed here combines the Peng-Robinson equation of state for the vapour phase with the Electrolyte-NRTL model for the liquid phase. Parameters are fitted gradually so that the entire system water-diethanolamine-methanol-CO2-H2S system is extrapolated using Electrolyte-NRTL parameters determined by fitting experimental acid gas partial pressures of lower systems. Methanol effect is also described. An original calculation of heat of absorption was also developed. We extended the use of our approach to study others alkanolamines

L'élasticité est une propriété qui permet aux systèmes Cloud de s'auto-adapter à leur charge de travail en provisionnant et en libérant des ressources informatiques, de manière autonomique, lorsque la demande augmente et diminue. En raison de la nature imprévisible de la charge de travail et des nombreux facteurs déterminant l'élasticité, fournir des plans d'action précis pour gérer l'élasticité d'un système cloud, tout en respectant des politiques de haut niveau (performances, cout, etc.) est une tâche particulièrement difficile.Les travaux de cette thèse visent à proposer, en utilisant le formalisme des bigraphes comme modèle formel, une spécification et une implémentation des systèmes Cloud Computing élastiques sur deux aspects : structurel et comportemental.Du point de vue structurel, le but est de définir et de modéliser une structure correcte des systèmes Cloud du côté " backend ". Cette partie est supportée par les capacités de spécification fournies par le formalisme des Bigraphes, à savoir : le principe de "sorting" et de règles de construction permettant de définir les desiderata du concepteur. Concernant l'aspect comportemental, il s'agit de modéliser, valider et implémenter des stratégies génériques de mise à l'échelle automatique en vue de décrire les différents mécanismes d'auto-adaptation élastiques des systèmes cloud (mise à l'échelle horizontale, verticale, migration, etc.), en multi-couches (i.e., aux niveaux service et infrastructure). Ces tâches sont prises en charge par les aspects dynamiques propres aux Systèmes Réactifs Bigraphiques (BRS) notamment par le biais des règles de réaction.Les stratégies d'élasticité introduites visent à guider le déclenchement conditionnel des différentes règles de réaction définies, afin de décrire les comportements d'auto-adaptation des systèmes Cloud au niveau service et infrastructure. L'encodage de ces spécifications et leurs implémentations sont définis en logique de réécriture via le langage Maude. Leur bon fonctionnement est vérifié formellement à travers une technique de model-checking supportée par la logique temporelle linéaire LTL.Afin de valider ces contributions d'un point de vue quantitatif, nous proposons une approche à base de file d'attente pour analyser, évaluer et discuter les stratégies d'élasticité d'un système Cloud à travers différents scénarios simulés. Dans nos travaux, nous explorons la définition d'une "bonne" stratégie en prenant en compte une étude de cas qui repose sur la nature changeante de la charge de travail. Nous proposons une manière originale de composer plusieurs stratégies d'élasticité à plusieurs niveaux afin de garantir différentes politiques de haut-niveau. / Elasticity property allows Cloud systems to adapt to their incoming workload by provisioning and de-provisioning computing resources in an autonomic manner, as the demand rises and drops. Due to the unpredictable nature of the workload and the numerous factors that impact elasticity, providing accurate action plans to insure a Cloud system's elasticity while preserving high level policies (performance, costs, etc.) is a particularly challenging task. This thesis aims at providing a thorough specification and implementation of Cloud systems, by relying on bigraphs as a formal model, over two aspects: structural and behavioral.Structurally, the goal is to define a correct modeling of Cloud systems' "back-end" structure. This part is supported by the specification capabilities of Bigraph formalism. Specifically, via "sorting" mechanisms and construction rules that allow defining the designer's desiderata. As for the behavioral part, it consists of model, implement and validate generic elasticity strategies in order to describe Cloud systems' auto-adaptive behaviors (i.e., horizontal and vertical scaling, migration, etc.) in a cross-layer manner (i.e., at service and infrastructure levels). These tasks are supported by the dynamic aspects of Bigraphical Reactive Systems (BRS) formalism (through reaction rules).The introduced elasticity strategies aim at guiding the conditional triggering of the defined reaction rules, to describe Cloud systems' auto-scaling behaviors in a cross-layered manner. The encoding of these specifications and their implementation are defined in Rewrite Logic via Maude language. Their correctness is formally verified through a model-checking technique supported by the linear temporal logic LTL.In order to quantitatively validate these contributions, we propose a queuing-based approach in order to evaluate, analyze and discuss elasticity strategies in Cloud systems through different simulated execution scenarios. In this work, we explore the definition of a “good” strategy through a case study which considers the changing nature of the input workload. We propose an original way de compose different cross-layer elasticity strategies to guarantee different high-level policies.