A ce jour, les méthodes formelles ont montré qu'elles étaient applicables avec succès au développement de logiciels industriels. Pour maîtriser la complexité croissante de ces applications, la mise en oeuvre des paradigmes d'abstraction et de composition est incontournable. La méthode B permet d'assister le processus de développement des spécifications au code et offre une notion de modularité qui permet de composer à la fois les spécifications et les développements. La compositionnalité des preuves est assurée par des restrictions imposées par le langage, qui limitent les formes d'architectures autorisées. A la suite de nos précédents travaux, le manuscrit présenté ici explicite les principes de composition des spécifications et des développements, énonce les théorèmes sous-jacents à la composition des preuves et complète et valide les restrictions imposées par la méthode B. Bien que dédiés à la méthode B, les résultats présentés sont plus généraux : ils peuvent s'appliquer à d'autres approches formelles basées sur la notion d'état, comme les approches objet

La thèse concerne trois problématiques indépendantes : le transport dissipatif dans des milieux hétérogènes; échange de masse entre un réservoir de gaz et aquifère ; ségrégation compositionnelle. Le point commun entre les problèmes traités sont les processus irréversibles de redistribution de la composition chimique. Le premier chapitre est consacré à la déduction, en accord avec les principes de la thermodynamique, d’un modèle généralisé de transport simultané de matière et de chaleur. Le chapitre 2 est consacré à l’étude de diffusion multi-compositionnelle dans un milieu hétérogène. Cette étude vise une application aux phénomènes de transport dans les réservoirs des hydrocarbures qui, d’une part, sont le siège de divers des processus de transport (plusieurs composants + chaleur) en interaction (processus croisés au sens d’Onsager) et, d’autre part, sont anisotropes pour les processus de transport étudiés. Le chapitre 3 est consacré à l’étude du processus de balayage d’un réservoir par une nappe aquifère. Le chapitre 4 est consacré au développement d’un code « éléments finis » conçu pour résoudre le même problème que dans le chapitre 3, mais dans une approche moins idéalisée. Le chapitre 5 est consacré à l’étude de la convection forcée dans un réservoir avec des champs de gravité et de température non colinéaires. Cette convection est une des composantes du processus de séparation thermo-gravitationnelle des espèces chimiques qui peut avoir lieu dans les réservoirs souterrains / The thesis concerns three independent subject areas: the dissipative transport in heterogeneous geological media; a transport problem in an underground gas reservoir; compositional segregation in reservoirs. The common point of all examined problems is the irreversible redistribution of chemical composition of a fluid in the reservoirs. The first chapter is devoted to development of a microscopic model of simultaneous mass and heat transfer in agreement with thermodynamic principles. The second chapter is dedicated to study of multi-component diffusion in a heterogeneous medium. This study aims an application to transport phenomena in hydrocarbon reservoirs characterized firstly by diversity of transported substances (several components + heat) and their interaction (in Onsager’s meaning) and secondly by anisotropy of medium where they take place. The third chapter is dedicated to analytical study of underground gas storage sweeping due to gas dissolution in aquifer. In the fourth chapter the same problem (gas sweeping) was studied numerically in a less idealized approach using finite element method. The fifth chapter is dedicated to study of forced convection taking place in the reservoirs where the temperature gradient and gravity force are not collinear. This convection represents an element of the thermo-gravitational component segregation employed in industry (thermo-gravitational columns) and can take place in underground reservoirs

Le présent manuscrit constitue la partie écrite du travail de thèse réalisé par Bruno Mery sous la direction de Christian Bassac et Christian Retoré entre 2006 et 2011, portant sur le sujet "Modélisation de la sémantique lexicale dans la théorie des types". Il s'agit d'une thèse d'informatique s'inscrivant dans le domaine du traitement automatique des langues, et visant à apporter un cadre formel pour la prise en compte, lors de l'analyse sémantique de la phrase, d'informations apportées par chacun des mots.Après avoir situé le sujet, cette thèse examine les nombreux travaux l'ayant précédée et s'inscrit dans la tradition du lexique génératif. Elle présente des exemples de phénomènes à traiter, et donne une proposition de système de calcul fondée sur la logique du second ordre. Elle examine ensuite la validité de cette proposition par rapport aux exemples et aux autres approches déjà formalisées, et relate une implémentation de ce système. Enfin, elle propose une brève discussion des sujets restant en suspens. / This paper is part of the thesis by Bruno Mery advised by Christian Bassac and Christian Retore in the years 2006-2011, on the topic "Modelling lexical semantics in a type-theoretic framework''. It is a doctoral thesis in computer science, in the area of natural language processing, aiming to bring forth a formal framework that takes into account, in the parsing of the semantics of a sentence, of lexical data.After a discussion of the topic, this thesis reviews the many works perceding it and adopts the tradition of the generative lexicon. It presents samples of data to account for, and gives a proposal for a calculus system based upon a second-order logic. It afterwards reviews the validity of this proposal, coming back to the data samples and the other formal approaches, and gives an implementation of that system. At last, it engages in a short discussion of the remaining questions.

Le travail présenté dans ce mémoire s’inscrit dans le cadre du suivi d'objets dans des vidéos, et plus particulièrement, sur l'utilisation de représentations par modèle d'apparence pour le suivi. La notion de modèle d'apparence est précisée sur la base de l'extraction de descripteurs visuels comparés à l'aide de similarités à une référence. De nouvelles techniques pour évaluer les performances vis à vis du suivi sont présentées. Les approches classiques d’évaluation considèrent uniquement la qualité des trajectoires finales estimées. Les métriques proposées dans ce mémoire s’en distinguent par le fait qu’elles quantifient la performance intrinsèque des modèles d’apparence utilisés au sein du système. Deux axes sont ainsi développés : d’une part, un ensemble de mesures de la précision spatiale d’un modèle couplées à la mesure de la robustesse vis-à-vis d’une initialisation spatiale approximative, et d’autre part, la proposition d’une méthodologie permettant de mesurer la stabilité d’un modèle du point de vue temporel sur des données vidéos naturelles. Ces techniques seront utilisées dans la suite du mémoire pour évaluer les méthodes existantes ainsi que celles présentées. Deux nouveaux modèles d'apparence sont ensuite introduits. Le premier modèle dénommé l’histogramme multi-échelles permet de limiter les ambigüités liées à la représentation par histogramme de couleurs. Le deuxième modèle, fondé sur une extension de la métrique de Matusita pour la comparaison de distributions de couleurs, prend en compte les variations possibles des couleurs des objets liées aux conditions de changement d’illumination. Enfin, le lien entre modèle d'apparence et technique de recherche de la position optimale est abordé dans le contexte du suivi multi-noyaux à travers la proposition d'un nouvel algorithme de suivi basé sur une approche compositionnelle inverse. Celui-ci offre un temps de calcul fortement réduit pour une qualité de suivi similaire aux algorithmes existants. / Abstract

L'évolution thermique des huiles dans les réservoirs est contrôlée par la cinétique du craquage. Cette étude traite de la stabilité thermique des composés aromatiques légers (C6-C14) des huiles brutes dans les conditions géologiques. L'objectif est de prédire cette stabilité par un modèle dérivé des expériences au laboratoire. La coupe légère de l'huile brute Safaniya <250 °C, correspondant aux composés en C15- , est séparée par distillation fractionnée. Une fraction aromatique pure est ensuite isolée par chromatographie liquide. La caractérisation moléculaire complète de cette fraction est réalisée par HPLC, GC et GC/MS. Les composés aromatiques ainsi identifiés et quantifiés sont regroupés selon leurs structures et leurs stabilités thermiques estimées dans six classes moléculaires: les BTXN, les méthylaromatiques, les alkylaromatiques, les naphténoaromatiques, les indènes et les composés aromatiques soufrés. Les pyrolyses sont effectuées en milieu fermé dans des tubes en or sous une pression de 100 bars et pour différentes conditions (température/temps) couvrant une très large gamme de conversion (1 à 93 %). Les effluents de pyrolyse sont fractionnés, analysés et regroupés en classes. L'évolution de l'ensemble des classes a été interprétée par l'élaboration d'un schéma cinétique semi-empirique composé de 13 réactions stoechiométriques qui rendent compte du craquage de la charge et du craquage secondaire des produits instables. Les paramètres cinétiques estimés de ce schéma ont été ensuite calibrés par optimisation numérique sous la contrainte des bilans de masse et de la conservation d'hydrogène. Afin d'évaluer l'effet de la pression sur le craquage thermique, nous avons réalisé une série de pyrolyses à 375 °C sous de hautes pressions de 400, 800 et 1200 bars. La comparaison des résultats de ces expériences à ceux obtenus à 100 bars a montré que l'augmentation de la pression retarde le craquage. Nous avons également mis en évidence une certaine sélectivité dans l'action de la pression sur les différentes classes que contient la charge et sur la distribution des produits de pyrolyse. L'extrapolation du modèle construit dans cette étude aux conditions du Bassin d'Elgin (Mer du Nord) a montré que l'augmentation de la pression aurait augmenté la stabilité thermique de la fraction aromatique légère en décalant son craquage de 8 °C.

L'objectif de la thèse est de développer des méthodologies et des outils pour la vérification compositionnelle et incrémentale des systèmes à base de composants. Nous proposons une méthode compositionnelle pour vérifier des propriétés de sûreté. La méthode est basée sur l'utilisation des deux types d'invariants: invariants de composant qui expriment des aspects locaux des systèmes et invariants d'interaction qui caractérisent les contraintes globales induites par les synchronisations fortes entre les composants. Nous offrons des techniques efficaces pour calculer ces invariants. Nous proposons également une nouvelle méthode de vérification incrémentale qui prend la conception incrémentale du système en compte. L'intégration de la vérification dans le processus de conception permet de déceler une erreur dès qu'elle apparaît. En outre, cette méthode permet d'éviter de refaire tous les processus de vérification par la réutilisation de résultats intermédiaires. Elle prend des avantages des structures de systèmes pour faire face à la complexité de la vérification globale et, par conséquent, réduit significativement le coût de la vérification en temps et en mémoire utilisée. Les méthodes compositionnelles et incrémentales ont été mises en oeuvre dans la chaîne d'outil D-Finder. Les résultats expérimentaux obtenus sur plusieurs études de cas non triviales montrent l'efficacité de nos méthodes ainsi que les capacités de D-Finder.

Le présent manuscrit constitue la partie écrite du travail de thèse réalisé par Bruno Mery sous la direction de Christian Bassac et Christian Retoré entre 2006 et 2011, portant sur le sujet "Modélisation de la sémantique lexicale dans la théorie des types". Il s'agit d'une thèse d'informatique s'inscrivant dans le domaine du traitement automatique des langues, et visant à apporter un cadre formel pour la prise en compte, lors de l'analyse sémantique de la phrase, d'informations apportées par chacun des mots. Après avoir situé le sujet, cette thèse examine les nombreux travaux l'ayant précédée et s'inscrit dans la tradition du lexique génératif. Elle présente des exemples de phénomènes à traiter, et donne une proposition de système de calcul fondée sur la logique du second ordre. Elle examine ensuite la validité de cette proposition par rapport aux exemples et aux autres approches déjà formalisées, et relate une implémentation de ce système. Enfin, elle propose une brève discussion des sujets restant en suspens.

La pyrolyse rapide est une des voies de conversion thermochimique qui permet la transformation de biomasse lignocellulosique en bio-huiles. Ces bio-huiles, différentes des coupes lourdes du pétrole ne peuvent pas être directement mélangés dans les procédés de valorisation. En effet, en raison de leur forte teneur en oxygène, les bio-huiles nécessitent une étape de pré-raffinage, telle que l’hydrotraitement, pour éliminer ces composants.L’objectif de ce travail est de comprendre la structure, la composition et la réactivité de la bio-huile grâce à la modélisation de données expérimentales. Pour comprendre leur structure et leur composition, des techniques de reconstruction moléculaire basées sur des données analytiques, ont été appliquées, générant un mélange synthétique, dont les propriétés correspondent à celles du mélange. Pour comprendre leur réactivité, l'hydrotraitement de molécules modèles a été étudié: gaïacol et furfural. Pour cela, un modèle déterministe et stochastique a été créé pour chacun d’eux. L’approche déterministe visait à récupérer une gamme de paramètres cinétiques, qui ont ensuite été affinés par l’approche stochastique créant un nouveau modèle. Cette approche a permis de générer un réseau de réactions en définissant et en utilisant un nombre limité de familles et règles des réactions. Finalement, le mélange synthétique a été utilisé dans la simulation stochastique de l’hydrotraitement de la bio-huile, étayée par la cinétique des molécules modèles.En conclusion, ce travail a permis de recréer la fraction légère de la bio-huile et de simuler leur l'hydrotraitement, via les paramètres cinétiques des composés modèles, qui prédisent de manière raisonnable les effluents de l'hydrotraitement de celles-ci, mais sont inadéquat pour le bio-huile / Fast pyrolysis is one of the thermochemical conversion routes that enable the transformation of solid lignocellulosic biomass into liquid bio-oils. These complex mixtures are different from oil fractions and cannot be directly integrated into existing petroleum upgrading facilities. Indeed, because of their high levels of oxygen compounds, bio-oils require a dedicated pre-refining step, such as hydrotreating, to remove these components.The aim of the present work is to understand the structure, composition and reactivity of bio-oil compounds through modeling of experimental data. To understand the structure and composition, molecular reconstruction techniques, based on analytical data, were applied generating a synthetic mixture, whose properties are consistent with the mixture properties. To understand the reactivity, the hydrotreating of two model molecules was studied: Guaiacol and Furfural. A deterministic and stochastic model were created for each compounds. The deterministic approach intended to retrieve a range of kinetic parameters, later on refined by the stochastic simulation approach into a new model. This approach generates an reaction network by defining and using a limited number of reaction classes and reaction rules. To consolidate the work, the synthetic mixture was used in the stochastic simulation of the hydrotreating of bio-oils, supported by the kinetics of the model compounds.In sum, the present work was able to recreate the light fraction of bio-oil and simulate the hydrotreating of bio-oils, via the kinetic parameters of model compounds, which can reasonably predict the effluents of the hydrotreating of these, but are unsuitable for bio-oil.Fast pyrolysis is one of the thermochemical conversion routes that enable the transformation of solid lignocellulosic biomass into liquid bio-oils. These complex mixtures are different from oil fractions and cannot be directly integrated into existing petroleum upgrading facilities. Indeed, because of their high levels of oxygen compounds, bio-oils require a dedicated pre-refining step, such as hydrotreating, to remove these components.The aim of the present work is to understand the structure, composition and reactivity of bio-oil compounds through modeling of experimental data. To understand the structure and composition, molecular reconstruction techniques, based on analytical data, were applied generating a synthetic mixture, whose properties are consistent with the mixture properties. To understand the reactivity, the hydrotreating of two model molecules was studied: Guaiacol and Furfural. A deterministic and stochastic model were created for each compounds. The deterministic approach intended to retrieve a range of kinetic parameters, later on refined by the stochastic simulation approach into a new model. This approach generates an reaction network by defining and using a limited number of reaction classes and reaction rules. To consolidate the work, the synthetic mixture was used in the stochastic simulation of the hydrotreating of bio-oils, supported by the kinetics of the model compounds.In sum, the present work was able to recreate the light fraction of bio-oil and simulate the hydrotreating of bio-oils, via the kinetic parameters of model compounds, which can reasonably predict the effluents of the hydrotreating of these, but are unsuitable for bio-oil

Cette thèse fournit de nouvelles stratégies de contrôle pouvant s'attaquer aux phénomènes hétérogènes et non-linéaires qui décrivent la régulation de la température dans les bâtiments afin d'obtenir un compromis entre le confort et l'efficacité énergétique. Nous nous intéressons donc au contrôle robuste de systèmes coopératifs avec perturbations bornées. Nous résolvons d'abord ce problème grâce à la notion d'intervalle invariant contrôlé robuste, décrivant un ensemble dans lequel l'état peut être maintenu quelle que soit la valeur des perturbations. Une seconde approche décrit des méthodes symboliques pour la synthèse d'un contrôleur discret sur une abstraction finie du système, réalisant une spécification de sûreté associée à l'optimisation des performances. Nous présentons d'abord une méthode symbolique centralisée utilisant les dynamiques du système correspondant au modèle physique. Pour résoudre ses limitations en termes de passage à l'échelle, nous considérons une approche compositionnelle où les méthodes symboliques d'abstraction et de synthèse sont appliquées à des descriptions partielles du système, sous des obligations de type assume-guarantee supposant que la sûreté est satisfaite pour tous les états non-contrôlés. Dans la dernière partie, les contrôleurs présentés sont combinés et évalués dans le cadre d'une régulation de température pour un bâtiment expérimental équipé de la solution UnderFloor Air Distribution. / This thesis provides new control strategies that deal with the heterogeneous and nonlinear dynamics describing the temperature regulation in buildings to obtain a tradeoff between comfort and energy efficiency. We thus focus on the robust control of cooperative systems with bounded disturbances. We first solve this problem with the notion of robust controlled invariant interval, which describes a set where the state can be maintained for any value of the disturbances. A second approach provides dedicated symbolic methods to synthesize a discrete controller on a finite abstraction of the system, realizing safety specifications combined with a performance optimization. We first present a centralized symbolic method using the system dynamics provided by the physical model. To address its limitation in terms of scalability, a compositional approach is considered, where the symbolic abstraction and synthesis methods are applied to partial descriptions of the system under the assume-guarantee obligation that the safety specification is realized for all uncontrolled states. In the final part, the proposed controllers are combined and evaluated on the temperature regulation for an experimental building equipped with UnderFloor Air Distribution.

Dans le présent travail de thèse, nous souhaitons approfondir l’étude des systèmes à commutation pour des problèmes aux dérivées partielles en explorant de nouvelles pistes d’investigation, incluant notamment la question de la synthèse de contrôle garanti par décomposition de l’espace des états, la synthèse de contrôle nécessitant la réduction de modèle, le contrôle des différentes sources d’erreur sur des quantités d’intérêt, et la mesure des incertitudes sur les états et les paramètres du modèle. Nous envisageons l’utilisation de méthodes de calcul ensemblistes associées à des méthodes de réduction de modèle, ainsi que l’utilisation d’observateurs d’état pour l’estimation en ligne du système. / In this thesis, we focus on switched control systems described by partial differential equations, and investigate the issues of guaranteed control of such systems using state-space decomposition methods. The use of state-space decomposition methods requires model order reduction, control of the different sources of error for quantities of interest, and measure of uncertainties on the states and parameters of the system. We are considering using set-based computation methods, in association with model order reduction techniques, along with the use of state-observers for on-line estimation of the system.