L'équation de Schrödinger est une équation fondamentale de la physique, qui fait intervenir une fonction appelée potentiel, linéaire ou non linéaire, pouvant prendre différentes expressions selon le contexte physique. Pour résoudre numériquement cette équation, il faut se restreindre à un domaine borné en espace, en précisant sur la frontière de ce domaine de calcul des conditions aux limites artificielles (CLA) appropriées. En dimension un et pour un potentiel nul, la condition aux limites exacte est connue. L'objectif de cette thèse est de généraliser ces résultats en construisant des CLA approchées dans le cas d'un potentiel, linéaire ou non linéaire. A cette fin, nous proposons une recherche détaillée de méthodes permettant de tenir compte du potentiel, sans distinction selon ses propriétés mathématiques. Cette construction repose sur l'analyse microlocale et les règles du calcul symbolique associé aux opérateurs pseudodifférentiels. Les CLA obtenues se prêtent alors à une discrétisation et une implémentation numérique effective à l'aide d'un schéma de Crank-Nicolson suivi d'une méthode éléments finis linéaires. Dans ce travail, nous avons élaboré des familles de CLA pour l'équation en dimension un ou deux d'espace avec un potentiel linéaire ou non linéaire, ainsi que pour le problème stationnaire en dimension un. Dans chaque cas, de nombreuses simulations numériques ont été effectuées afin de comparer l'efficacité des conditions aux limites proposées par rapport aux autres méthodes existantes, ainsi que pour comparer entre elles les différentes familles de conditions aux limites construites suivant différentes stratégies / The Schrödinger equation is a fundamental equation involved in many physical domains. It deals with a linear or nonlinear function called potential, which can appear under various different expressions depending on the physical context. In order to solve the equation numerically, one has to restrict to a bounded spatial domain, and to add appropriate artificial boundary conditions (ABC) on the boundary of the computational domain. For the free-potential equation in one dimension, the exact boundary condition is known. The aim of this thesis is to generalize these results thanks to the construction of approximate ABC in the case of a linear or nonlinear potential. To this end, we propose a detailed research of methods taking the potential into account in the artifical boundary condition, without considering the mathematical properties of the considered potential. The construction of these CLA relies on microlocal analysis and the rules of symbolic calculus associated to pseudodifferential operators. These approximate boundary conditions can then be discretized and numerically computed, using a Crank-Nicolson scheme and a linear finite element method. In this work, we have derived families of ABCs for the Schrödinger equation in dimension one and two, with a linear or nonlinear potential, and for the stationary one-dimensional problem. In each case, many numerical simulations have been implemented in order to compare the efficiency of the new boundary conditions with respect to existing methods, and also in order to compare with one another the different families of boundary conditions developed following different strategies

Ce travail de thèse propose une méthodologie de dimensionnement s'adaptant à un grand nombre de structures de convertisseurs statiques. Elle intègre différents outils préexistants, et s'appuie sur la formulation automatique, avec des techniques de calcul symbolique, d'un modèle de dimensionnement. Celui-ci prend en charge, à un même niveau, l'aspect physique du fonctionnement et l'aspect conception qui s'exprime en termes de respect d'un cahier des charges. La connaissance fondamentale pour mettre en œuvre cette démarche se veut minimale, et comprend les équations des nœuds du circuit et les spécifications du cahier des charges. L'intervention de l'utilisateur dans la méthodologie est réduite au maximum et simplifiée. Sur ces principes, cette approche de CAO cherche à fournir au concepteur, via l'ordinateur, en plus de logiciels d'analyse, un véritable outil d'aide au dimensionnement intégrable dans une méthodologie globale de conception des convertisseurs statiques.

Cette thèse se positionne dans le domaine de la vérification déductive de programmes, qui consiste à transformer une propriété à vérifier sur un programme en un énoncé logique, pour ensuite démontrer cet énoncé. La vérification effective d'un programme peut poser de nombreuses difficultés pratiques. En fait, les concepts mis en jeu derrière le programme peuvent suffire à faire obstacle à la vérification. En effet, certains programmes peuvent être assez courts et n'utiliser que des constructions simples, et pourtant s'avérer très difficiles à vérifier. Cela nous amène à la question suivante: dans le contexte d'un environnement de vérification déductive de programmes basé sur les démonstrateurs automatiques, quelles méthodes appliquer pour réduire l'effort nécessaire à la fois pour spécifier des comportements attendus complexes, ainsi que pour démontrer qu'un programme respecte ces comportements attendus? Pour mener notre étude, nous nous sommes placés dans le cadre de l'environnement de vérification déductive de programmes Why3. La vérification de programmes en Why3 est basée sur la génération de conditions de vérification, et l'usage de démonstrateurs externes pour les prouver, que ces démonstrateurs soient automatiques ou interactifs. Nous avons développé plusieurs méthodes, certaines générales et d'autres spécifiques à des classes de programmes, pour réduire l'effort manuel. Nos contributions sont les suivantes. Tout d'abord, nous ajoutons des fonctionnalités à Why3 pour assister le processus de vérification, notamment un mécanisme léger de preuve déclarative basé sur la notion d'indicateurs de coupures. Ensuite, nous présentons une méthode de vérification d'absence de débordement arithmétique pour une classe d'utilisation des entiers difficile à traiter par les méthodes standards. Enfin, nous nous intéressons au développement d'une bibliothèque générique pour la spécification et la preuve de programmes générateurs de code. / This thesis is set in the domain of deductive verification of programs, which consists of transforming a property to be verified about a program into a logical statement, and then proving this statement. Effective verification of a program can pose many practical difficulties. In fact, the concepts behind the program may be sufficient to impede verification. Indeed, some programs can be quite short and use only simple constructions, and yet prove very difficult to verify. This leads us to the following question: in the context of a deductive program verification environment based on automatic provers, what methods can be applied to reduce the effort required both to specify complex behaviors, as well as to prove that a program respects these expected behaviors? To carry out our study, we placed ourselves in the context of the deductive verification environment of programs Why3. The verification of programs in Why3 is based on the generation of verification conditions, and the use of external provers to prove them, whether these provers are automatic or interactive. We have developed several methods, some general and others specific to some program classes, to reduce manual effort. Our contributions are as follows. First, we add features to Why3 to assist the verification process, including a lightweight declarative proof mechanism based on the notion of cut indicators. Then we present a method for checking the absence of arithmetic overflow, for use cases which are difficult to process by standard methods. Finally, we are interested in the development of a generic library for the specification and proof of code generating programs.

L'objectif de ce travail de thèse est de définir et de présenter une nouvelle approche de la conception sous contraintes de machines électriques. Celle-ci permet aux électrotechniciens d'utiliser l'ordinateur non pas seulement comme un outil d'analyse mais aussi comme un outil ayant de réelles facultés de dimensionnement automatique. Cette approche offre de grands avantages comme: -la gestion des contraintes d'un cahier des charges, -la gestion de l'interdépendance des phénomènes physiques intervenant dans une machine, -ou encore l'optimisation des solutions trouvées. Cependant sa grande originalité est qu'elle assure automatiquement la génération du logiciel de conception. Pour cela elle utilise comme connaissance de base, un modèle analytique de la machine à laquelle on s'intéresse, et comme moyen, des techniques de calcul symbolique et de programmation automatique. Afin de guider le processus de conception, elle emploie des algorithmes génériques d'optimisation numérique sous contraintes. Cette approche est notamment appliquée, dans ce mémoire, au dimensionnement de machines asynchrones.

L'étude de certaines variables aléatoires, comme les paramètres additifs sur les arbres hyperquaternaires de points, ou encore le nombre de maxima au sein d'un ensemble de n points indépendants, et uniformément distribués dans [0,1]^d font apparaître des suites particulières, les sommes harmoniques multiples (SHM), extensions des nombres harmoniques classiques à des multi-indices.<br /><br />Nos travaux visant à appliquer des méthodes symboliques pour l'étude de ces variables aléatoires, nous remplaçons l'utilisation de multi-indices par des codages sur des alphabets distincts, et nous appuyons alors sur des résultats importants en combinatoire des mots pour les appliquer à nos suites de SHM, et aux fonctions polylogarithmes, qui sont des variantes des génératrices ordinaires des SHM. Dans les cas convergents, les deux objets convergent (respectivement lorsque z tend vers 1 et lorsque N tend vers l'infini) vers la même limite, appelée polyzêta. Pour les cas divergents, l'utilisation de séries génératrices non commutatives nous permet d'établir un théorème ``à l'Abel'', faisant apparaître une limite commune. Ce théorème permet de donner une forme explicite aux constantes d'Euler généralisées associées à des SHM divergentes et ainsi d'obtenir un algorithme très efficace pour calculer leur développement asymptotique.<br /><br />Finalement, nous proposons des applications des sommes harmoniques dans le domaine des structures de données multidimensionnelles, pour lesquelles notre approche donne naissance à des calculs exacts, qui peuvent par la suite être aisément évalués asymptotiquement.

La résolution numérique de l'équation de Schrödinger en domaine extérieur nécessite l'utilisation de conditions aux limites appropriées sur la frontière du domaine de calcul. Les conditions aux limites à utiliser sont directement reliées à la fonction de potentiel intervenant dans l'équation. Pour l'équation à potentiel nul, la condition aux limites exacte est connue, ainsi que des méthodes efficaces de discrétisation et d'implémentation numérique. L'objectif de cette thèse est d'étendre les méthodes mises en jeu à potentiel nul dans le cas d'un potentiel aussi général que possible, à l'image des situations physiques variées faisant intervenir un potentiel, linéaire ou non linéaire. Nous prenons le parti de renoncer à établir des conditions aux limites exactes, au profit d'une plus grande généralité de la méthode et d'une bonne adaptation à une implémentation numérique. En se basant sur le calcul pseudodifférentiel, on propose alors une recherche détaillée de méthodes permettant de prendre en compte le potentiel dans une condition aux limites artificielle (CLA). Cette thèse traite le cas de l'équation en dimension un ou deux avec potentiel linéaire ou non linéaire, ainsi que de l'équation stationnaire en dimension un. La construction de ces CLA repose sur l'analyse microlocale et le calcul symbolique associé aux opérateurs pseudodifférentiels fractionnaires. La discrétisation en temps est effectuée à l'aide de convolutions discrètes ou d'approximants de Padé, et la discrétisation en espace repose sur des éléments finis linéaires. On utilise la méthode de relaxation de Besse pour résoudre l'équation non linéaire. L'analyse mathématique des conditions construites dans cette thèse permet de démontrer dans certains cas des estimations a priori, sur le plan continu et sur le plan semi-discret. De nombreuses simulations numériques permettent de tester l'efficacité des conditions aux limites proposées et de les comparer entre elles.

Au cours de ce travail, une implantation de la méthode d'analyse de sensibilité d'ordre élevé a été réalisée au sein de la méthode des éléments finis (MEF). Tout d'abord nous avons posé ta base théorique des développements: la MEF classique et surtout la méthode de dérivées d'ordre élevé qui engendre les résultats sous la forme de développements de Taylor par rapport aux paramètres de conception. En s'appuyant sur la structure typique d'un code de calculs EF, nous avons développé ensuite les modules d'un calcul "paramétré": la paramétrisation géométrique, la dérivation du maillage et la résolution paramétrée. L'originalité de cette implantation consiste dans une nouvelle organisation des calculs de dérivées qui sont basés notamment sur les opérations symboliques. Pour valider des étapes de calculs, plusieurs exemples ont été présentés. Enfin, les applications possibles des résultats paramétrés sont évoquées, entre autres, une procédure pour définir le modèle analytique équivalent de dispositifs électromagnétiques a été proposée. Notons que plusieurs problèmes de réalisation informatique ont été mise en évidence et résolus, ce qui représente un gros investissement en programmation. Des nombreuses perspectives sont ouvertes par cette approche, le travail mériterait donc d'être poursuivi.

Ce travail s'intéresse à la conception sous contraintes de dispositifs électromagnétiques à l'aide de modèles analytiques. Après avoir présenté le contexte de conception en génie électrique, et les problèmes inhérents au dimensionnement sous contraintes, notamment celui des systèmes d'équations implicites, l'étude présente une nouvelle architecture orientée objet pour le dimensionnement à l'aide de modèles analytiques. L'objectif est de créer un environnement souple et modulaire pour manipuler les équations analytiques de façon à utiliser toute l'information qu'elles contiennent. On veut par exemple ré-orienter le modèle étudié ou calculer les dérivées partielles symboliques des paramètres de sortie, ceci afin d'effectuer de la propagation de contraintes, du solver ou de l'optimisation sous contraintes. Un prototype informatique implantè est présenté.

Du fait de son impact énergétique, la gestion énergétique dans le bâtiment est devenu un enjeu majeur ses dernières années, qu'il s'agisse d'encourager la sobriété énergétique ou de s'adapter aux besoins des réseaux énergétiques. Différents travaux de recherche ont conduit à des gestionnaires énergétiques souvent dotés de capacités d'anticipation. Les premiers résultats, bien qu'encourageants, n'envisagent pas la complexité tant du fait nombre d'éléments que de la diversité des applications de gestion énergétique.Cette thèse propose d'apporter des éléments de solution à la problématique de complexité. Les travaux ont démarré par l'analyse du gestionnaire énergétique GHomeTech et son adaptation au prototype de bâtiment complexe CANOPEA. Les problématiques de composition sont explorées. Une solution favorisant la réutilisabilité d'éléments de modèles, l'agrégation et la transformation vers des modèles d'optimisation de type programmation linéaire en nombres entiers (PLNE), est proposée. L'outil résultant a été validé sur le projet CANOPEA.La gestion énergétique ne se limite pas à l'optimisation PLNE. Différentes natures d'applications permettent d'offrir d'autres services : l'estimation paramétrique de modèles pour simplifier la configuration des gestionnaires énergétiques, la simulation pour la validation et la prédiction fonction de scénarios définis par exemple. Cette autre dimension de la complexité est abordée dans un second volet du manuscrit. Des solutions de réécriture automatique de modèles sont proposées grâce à des manipulations symboliques permettant différents types de transformation. Plusieurs exemples de génération automatique de modèles applicatifs sont présentés. / Energy management for building has become a major issue this last decade because of its energy impact. Building energy management reduces energy wastes and enable a better matching between energy needs and grid capabilities. Different types of energy management systems are proposed in scientific literature, most of them with anticipation capacities.The first results do not really consider the complexity issue coming from the number of modeling elements and also coming from the diversity of energy management applications.This thesis proposes elements of solution to the complexity problem. The work started by analyzing the energy management system 'GHomeTech' and its adaptation to the complex building prototype CANOPEA. The issue of composition from elementary models is explored. A solution is proposed; it enables the reusability of elementary models. Aggregation and transformation into mixed integer linear programming optimization models is presented. The resulting tool has been validated on the CANOPEA project.Energy management is not limited to MILP optimization. Different types of applications are also used to provide other services: parametric estimation models to simplify the configuration of energy management systems, simulation for validation and prediction depending on pre-defined scenarios for example. This other dimension of complexity is discussed in a second part of the manuscript. Solutions for automatic rewriting of models are detailed. It relies on symbolic manipulations in different types of processing. Several examples of applications illustrating the automatic generation of models are presented.

.