Un nouveau concept de stockage inter-saisonnier par absorption de l'énergie solaire pour l'habitat est développé dans cette thèse. Le processus est présenté et décrit. L'étude de la capacité de stockage, du rendement, de la pression de fonctionnement, du besoin de température pour l'énergie solaire, de la température possible pour le chauffage du bâtiment, des critères de sécurité et du coût des matériaux de sept couples d'absorption: CaCl2/H2O, Glycérine/H2O, KOH/H2O, LiBr/H2O, LiCl/H2O, NaOH/H2O et H2O/NH3 est effectuée à l'aide d'une simulation statique. Un prototype de démonstration de la faisabilité de ce concept innovant avec le couple CaCl2/H2O a été conçu, dimensionné et construit. Il est issu d'une optimisation minimisant le nombre de composants du système. Des expérimentations ont été effectuées à différentes conditions de fonctionnement. Les performances thermodynamiques et les différents problèmes du prototype sont analysés. Comme les résultats expérimentaux sont influencés par plusieurs facteurs tels que la présence d'air dans le système (en particulier pour la phase d'absorption), la précision des capteurs et des facteurs humains lors de l'opération, pour une meilleure compréhension du processus, une simulation dynamique est développée. Le fonctionnement optimal du prototype est alors étudié. Une simulation globale annuelle est effectuée afin d'étudier le fonctionnement annuel du système de stockage inter-saisonnier en lien avec un système solaire et un bâtiment. Les modèles du système de stockage, d'un capteur solaire, d'un bâtiment et des conditions météorologiques sont couplés. Les caractéristiques : pressions, températures, masses, fractions massiques, puissances échangées, rendements, capacités de stockage, etc. du système de stockage sont présentés et analysés.

Thèse diffusée initialement dans le cadre d'un projet pilote des Presses de l'Université de Montréal/Centre d'édition numérique UdeM (1997-2008) avec l'autorisation de l'auteur.

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

Thèse numérisée par la Direction des bibliothèques de l'Université de Montréal.

Pour répondre au besoin de miniaturisation des spectromètres de terrain travaillant dans l’infrarouge, l’ONERA a développé un nouveau concept baptisé MICROSPOC. Ce dispositif est un détecteur infrarouge auquel a été intégré un interféromètre à deux ondes, constituant un spectromètre statique par transformée de Fourier. Ce plan focal infrarouge modifié, qui fusionne la fonction interférométrique et la fonction de détection, associé à une optique de tête simplifiée, permet d’envisager la réalisation d’instruments très compacts. L’objectif de cette thèse est de concevoir un spectromètre infrarouge miniature basé sur le dispositif MICROSPOC. Dans un premier temps, un travail théorique a été mené, dans l’objectif de dimensionner un système optique très compact. Notre choix s’étant orienté vers un système optique de collection (le détecteur voit une source étendue à distance finie), l’étude de l’acceptance angulaire de MICROSPOC dans ces conditions d’éclairement est indispensable afin de prévoir le contraste et la forme des franges d’interférence. Les résultats montreront la grande acceptance angulaire de MICROSPOC.Dans un second temps, un démonstrateur basé sur un composant MICROSPOC et sur le système optique simplifié a été réalisé. Ce démonstrateur a été caractérisé en laboratoire puis utilisé sur le terrain lors d’une campagne de mesures. Ces différentes exploitations ont montré la robustesse de l’instrument malgré l’obtention d’interférogrammes présentant divers défauts.Dans un troisième temps, une chaîne de traitement a été développée afin d’estimer un spectre à partir d’un interférogramme obtenu à l’aide du démonstrateur. Du fait des caractéristiques intrinsèques de MICROSPOC, la transformée de Fourier n’est pas la meilleure solution pour estimer un spectre. Nous l’avons montré en nous intéressant aux effets des disparités de longueur d’onde de coupure du détecteur sur l’estimation d’un spectre. Nous nous sommes alors tournés vers une approche consistant à utiliser la caractérisation spectrale de l’instrument pour inverser la mesure. Cette approche donne des résultats satisfaisants.Enfin, le but principal de cette thèse a été élargi par la conception et la réalisation de différents démonstrateurs combinant une fonction d’imagerie à une fonction de spectrométrie. Les premières pistes pour la conception d’un spectromètre qui tient dans la main ont été données. / In order to satisfy the need for handheld infrared spectrometers, the ONERA developed a new concept called MICROSPOC. This device is an infrared focal plane array with a built-in two-wave wedge-like interferometer and forms a static Fourier-transform spectrometer. This modified focal plane array, which merges the detection function and the interferometric function, in association with a simplified optical system, allows to consider the realisation of a much compact instrument. The goal of this thesis is to design and to realize a miniaturized infrared spectrometer based on the MICROSPOC concept.Firstly, a theoritical work has been led in order to design a compact optical system. Since we have chosen a collection optical system (the focal plane array sees an extended source placed at a finite distance), the study of MICROSPOC angular acceptance in these lightening conditions is needed in order to predict the contrast and the shape of interference fringes. The huge angular acceptance of MICROSPOC will be established with the results of this study.Secondly, a demonstrator based on MICROSPOC device and on the simplified optical system has been realized. This demonstrator has been caracterized in the laboratory and used in real conditions of a measurement campaign. These different exploitations have shown the robustness of the instrument despite some defaults on acquired interferograms.Then, a processing chain has been developed in order to estimate a spectrum from an interferogram acquired with our demonstrator. Considering the MICROSPOC’s own characteristics, the Fourier-transform is not the best way to estimate a spectrum. We have come to this conclusion by studying the effects of cut-off wavelenghts disparities of the detector on the spectrum estimation. At this point we have considered an approach that consists of using the spectral characterization of the instrument in order to inverse the measure. This approach gives satisfying results.Finaly, the main goal has been widened with the design and the realisation of other instruments that combine a spectrometric function and a imaging function. The first elements for the design of a handheld spectrometer have been given.

Il existe de nombreuses approches développées par la communauté Implicit Computational Complexity (ICC) permettant d'analyser les ressources nécessaires à la bonne exécution des algorithmes. Dans cette thèse, nous nous intéressons plus particulièrement au contrôle des ressources à l'aide d'interprétations sémantiques. Après avoir rappelé brièvement la notion de quasi-interprétation ainsi que les différentes propriétés et caractérisations qui en découlent, nous présentons les différentes avancées obtenues dans l'étude de cet outil : nous étudions le problème de la synthèse qui consiste à trouver une quasi-interprétation pour un programme donné, puis, nous abordons la question de la modularité des quasi-interprétations. La modularité permet de diminuer la complexité de la procédure de synthèse et de capturer un plus grand nombre d'algorithmes. Après avoir mentionné différentes extensions des quasi-interprétations à des langages de programmation réactifs, bytecode ou d'ordre supérieur, nous introduisons la sup-interprétation. Cette notion généralise la quasi-interprétation et est utilisée dans des critères de contrôle des ressources afin d'étudier la complexité d'un plus grand nombre d'algorithmes dont des algorithmes sur des données infinies ou des algorithmes de type diviser pour régner. Nous combinons cette notion à différents critères de terminaison comme les ordres RPO, les paires de dépendance ou le size-change principle et nous la comparons à la notion de quasi-interprétation. En outre, après avoir caractérisé des petites classes de complexité parallèles, nous donnons quelques heuristiques permettant de synthétiser des sup-interprétations sans la propriété sous-terme, c'est à dire des sup-interprétations qui ne sont pas des quasi-interprétations. Enfin, dans un dernier chapitre, nous adaptons les sup-interprétations à des langages orientés-objet, obtenant ainsi différents critères pour contrôler les ressources d'un programme objet et de ses méthodes / There are several approaches developed by the Implicit Computational Complexity (ICC) community which try to analyze and control program resources. In this document, we focus our study on the resource control with the help of semantics interpretations. After introducing the notion of quasi-interpretation together with its distinct properties and characterizations, we show the results obtained in the study of such a tool: We study the synthesis problem which consists in finding a quasi-interpretation for a given program and we tackle the issue of quasi-interpretation modularity. Modularity allows to decrease the complexity of the synthesis procedure and to capture more algorithms. We present several extensions of quasi-interpretations to reactive programming, bytecode verification or higher-order programming. Afterwards, we introduce the notion of sup-interpretation. This notion strictly generalizes the one of quasi-interpretation and is used in distinct criteria in order to control the resources of more algorithms, including algorithms over infinite data and algorithms using a divide and conquer strategy. We combine sup-interpretations with distinct termination criteria, such as RPO orderings, dependency pairs or size-change principle, and we compare them to the notion of quasi-interpretation. Using the notion of sup-interpretation, we characterize small parallel complexity classes. We provide some heuristics for the sup-interpretation synthesis: we manage to synthesize sup-interpretations without the subterm property, that is, sup-interpretations which are not quasi-interpretations. Finally, we extend sup-interpretations to object-oriented programs, thus obtaining distinct criteria for resource control of object-oriented programs and their methods

L'analyse statique est utilisée pour vérifier de manière formelle qu'un programme ne fait pas d'erreurs, mais un analyseur statique est lui même un programme complexe sujet aux erreurs. Une analyse statique formalisée comme un interpreteur abstrait peut être prouvée correcte, cependant un telle preuve ne porte pas directement sur l'implementation de l'analyseur. Pour résoudre cette difficultée, nous proposons de générer des conditions de vérification (VCs, des formules logiques valides seulement si le résultat de l'analyseur est correct), et de les décharger à l'aide d'un prouveur de théorèmes automatique (ATP). Les VCs générées appartiennent à la logic du premier ordre multi-sortée (MSFOL), une logique utilisée avec succés en vérification déductive, suffisament expressive pour encoder les résultats d'analyses complexes et pour formaliser la sémantique operationnelle d'un langage objet, ce qui nous permet de prouver la correction des VCs générées à l'aide d'outils de vérification deductive. Pour assurer que les VCs puissent être déchargée automatiquement pour des analyses du tas, nous introduisons un calcul de VCs appartenant à un fragment décidable de MSFOL, et afin de pouvoir utiliser le même calcul pour différentes analyses, nous décrivons une famille d'analyses à l'aide d'une fonction de concretisation et d'un instrumentation de la sémantique paramétrées. Pour améliorer la fiabilité des ATPs, nous étudions aussi la certification de résultat des proveurs de satisfiabilité modulo théories, une famille d'ATPs dédiée à MSFOL. Nous proposons un système de preuve et un vérifieur modulaires, qui s'appuient sur des vérifieur dédiés aux théories sous-jacentes. / Static program analysis is a core technology for both verifying and finding errors in programs but most static analyzers are complex pieces of software that are not without error. A Static analysis formalised as an abstract interpreter can be proved sound, however such proofs are significantly harder to do on the actual implementation of an analyser. To alleviate this problem we propose to generate Verification Conditions (VCs, formulae valid only if the results of the analyser are correct) and to discharge them using an Automated Theorem Prover (ATP). We generate formulae in Many-Sorted First-Order Logic (MSFOL), a logic that has been successfully used in deductive program verification. MSFOL is expressive enough to describe the results of complex analyses and to formalise the operational semantics of object-oriented languages. Using the same logic for both tasks allows us to prove the soundness of the VC generator using deductive verification tools. To ensure that VCs can be automatically discharged for complex analyses of the heap, we introduce a VC calculus that produces formulae belonging to a decidable fragment of MSFOL. Furthermore, to be able to certify different analyses with the same calculus, we describe a family of analyses with a parametric concretisation function and instrumentation of the semantics. To improve the reliability of ATPs, we also studied the result certification of Satisfiability Modulo Theory solvers, a family of ATPs dedicated to MSFOL. We propose a modular proof-system and a modular proof-verifier programmed and proved correct in Coq, that rely on exchangeable verifiers for each of the underlying theories.

Depuis plusieurs décennies, la modélisation moyenne de convertisseurs statiques a fait l'objet de nombreuses études. En effet, nous avons intérêt à transformer le système original en un système continu qui représente macroscopiquement au mieux les comportements dynamiques et statiques du circuit, notamment en vue d'une étude système. Le modèle dit « moyen » trouve un vaste champ d'applications que ce soit en commande, en simulation (rapide et système) ou encore en analyse des modes... Cependant, la modélisation moyenne peut s'avérer laborieuse dés que le nombre de semi-conducteurs du convertisseur devient important. Dans cette optique, plusieurs auteurs ont essayé d'apporter une aide automatique dans le processus de calcul de ces modèles afin d'épargner l'utilisateur de cette fastidieuse tâche de calcul faite à la main. Néanmoins, actuellement, la démarche de modélisation n'a jamais été entièrement automatisée. Dans cette perspective, les objectifs de cette thèse visent à fournir un outil d'aide à la génération automatique de modèles exacts et moyens dans le cas de la conduction continue et/ou discontinue et en partant d'un a priori sur le fonctionnement du convertisseur à étudier : la description du circuit, le mode de fonctionnement et la commande du convertisseur statique. La conception d'un tel outil repose sur trois étapes principales et qui sont l'analyse topologique du circuit, le calcul des matrices d'état pour chaque configuration du convertisseur statique et enfin une mise en équations des modèles. Les modèles générés sont sous forme symbolique ce qui permet de les réutiliser dans plusieurs logiciels.

Analyse limite : formulations analytique et numérique avec application aux structures en géotechnique, pour les milieux isotropes et orthotropes de révolution.

Une base de données est au service de plusieurs catégories d'utilisateurs ayant chacune sa vision personnelle et évolutive des différentes sortes d'objets d'un univers. L'application systématique du concept d'abstraction a permis de dégager la notion d'objet pouvant être vu selon différentes facettes, appartenir à plusieurs ensembles et/ou relations, tout en demeurant unique. Ces objets sont spécifiés à l'aide de p-types, concept défini dans le cadre des types abstraits algébriques. La définition d'un p-type est modulaire et évolutive; une vue du p-type est caractérisée par des fonctions attributs et des contraintes d'intégrité. Les contraintes étudiées sont les dépendances entre valeurs d'attributs d'une occurrence d'un p-type (DIA) et les dépendances inter-objets (DIO). L'analyse statique de ces contraintes permet de garantir leur cohérence et de minimiser les vérifications dynamiques