Cette thèse porte sur deux aspects de la théorie de Morse: théorie de Morse discrète de Forman (cas de la dimension finie) et homologie de Heegaard-Floer (cas de la dimension infinie).<br />Dans une première partie, on s'intéresse au problème de relèvement de signe pour l'homologie de Heegaard-Floer combinatoire. On montre que la construction originale faite par Manolescu, Ozsváth, Szabó et D. Thurston peut être refaite de manière plus conceptuelle. On donne ensuite le lien entre ces deux constructions puis finalement on décrit un algorithme qui permet de calculer les signes.<br />La seconde partie porte sur la théorie de Morse discrète définie par Forman. Après avoir fait le lien entre l'algèbre sur les complexes de chaînes et la théorie de Morse discrète, on montre que le complexe de Thom-Smale donné par une fonction de Morse lisse sur variété lisse close peut être réalisé par une triangulation et une fonction de Morse discrète sur celle-ci. On utilise cela pour obtenir une représentation particulière sous forme de couplage complet de toute structure d'Euler sur une variété de dimension 3 close orientée.

Dans cette thèse, une approche pratique pour la génération de maillages triangulaires isotropes est proposée. En 2D comme en 3D, l'ob jectif consiste à mailler un domaine donné, pouvant avoir une géométrie complexe. L'approche présentée consiste à entrelacer des étapes de raffinement de Delaunay et des étapes d'optimisation de maillages dans le but de générer des maillages gradés de qualité. L'utilisateur peut contrôler les caractéristiques du maillage en définissant des critères de taille et de forme des simplexes, ainsi que de topologie et d'approximation. Les méthodes par éléments finis, largement utilisées en simulation, nécessitent des maillages gradés, composés de simplexes bien formés. Des alternatives aux méthodes de raffinement de Delaunay usuelles sont développées. Les méthodes d'optimisation de maillages proposées permettent d'optimiser la position des sommets intérieurs et de ceux du bord. Les caractéristiques du bord du domaine à mailler, et en particulier des arêtes vives, sont préservées par ces méthodes. En 2D, l'optimisation est basée sur l'algorithme de Lloyd et les diagrammes de Voronoi centrés (CVT). En 3D, une extension naturelle des triangulations de Delaunay optimales (ODT) de Chen, capable d'optimiser la position des sommets du bord du maillage, est introduite. Notre algorithme de maillage tétraédrique est enrichi par une étape de post-traitement permettant d'améliorer de façon significative la qualité des angles dièdres du maillage. Nous montrons que l'entrelacement d'étapes de raffinement et d'optimisation permet d'obtenir des maillages de meilleure qualité que ceux générés par les méthodes connues en termes d'angles dans les simplexes et de complexité.

Dans les domaines critiques d'application de l'informatique, il peut être vital de disposer d'un génie logiciel qui soit capable de garantir le bon fonctionnement des systèmes produits. Dans ce contexte, la méthode B évènementielle promeut le développement de modèles abstraits du système à concevoir et l'utilisation de démonstrations formelles ainsi que de la relation de raffinement entre les modèles. Notre but est de pouvoir travailler sur des systèmes ayant des aspects temporels quantitatifs (propriétés et contraintes de temps) en restant au sein du cadre défini par la méthode B qui a déjà montré son efficacité par ailleurs, mais qui ne dispose pas de concepts spécifiques pour le temps. C'est ainsi que nous proposons l'introduction des contraintes de temps par le raffinement, ceci permet de respecter la philosophie de la méthode B et de systématiser cette approche par la formalisation de patrons de raffinement. Nos différentes modélisations du temps sont proposées sous la forme de patron à réappliquer sur le système à étudier. Nous pouvons donc étudier progressivement le système à partir d'une abstraction non-temporelle afin de le valider progressivement et de distribuer la difficulté de la preuve en plusieurs étapes. L'introduction des aspects temporels ne se fait que lorsque cela est nécessaire lors du processus de développement prouvé. Nous avons validé cette approche sur des études de cas réalistes en utilisant les outils logiciels de démonstration formelle de la méthode B.

Cette thèse se situe au croisement de deux domaines : la sûreté de fonctionnement des systèmes critiques et les méthodes formelles. Nous cherchons à établir la cohérence des analyses de sûreté de fonctionnement réalisées à l'aide de modèles représentant un même système à des niveaux de détail différents. Pour cela, nous proposons une notion de raffinement dans le cadre de la conception de modèles AltaRica : un modèle détaillé raffine un modèle abstrait si le modèle abstrait simule le modèle détaillé. La vérification du raffinement de modèles AltaRica est supportée par l'outil de model-checking MecV. Ceci permet de réaliser des analyses multi-systèmes à l'aide de modèles à des niveaux de détail hétérogènes : le système au centre de l'étude est détaillé tandis que les systèmes en interface sont abstraits. Cette approche a été appliquée à l'étude d'un système de contrôle de gouverne de direction d'un avion connecté à un système de génération et distribution électrique.

L'augmentation en taille et en complexité des systèmes réactifs font que leur vérification est de plus en plus difficile à comprendre et à appréhender. Dans cette thèse, une approche est proposée pour spécifier et vérifier compositionnellement certains de ces systèmes.<br /><br />Cette approche est basée sur un principe de décomposition supportant un raffinement compositionnel au niveau des composants et au niveau de leur produit synchronisé~: une méthode est présentée pour vérifier le raffinement d'un système à composants à partir du raffinement de ses composants.<br /><br />Les propriétés LTL sont préservées par le raffinement compositionnel présenté ici. De plus, certaines propriétés -- comme les invariants et les propriétés LTL de sûreté -- peuvent être vérifiées compositionnellement durant la phase de vérification du raffinement.<br /><br />Un outil, nommé SynCo, implante cette approche de vérification compositionnelle. Les différents aspects de ce travail sont illustrés par plusieurs exemples~: un robot industriel, un système d'essuyage et un porte-monnaie électronique.

Notre thèse se situe dans le domaine des méthodes formelles appliquées aux systèmes réactifs. Nous modélisons et traitons ces systèmes, en continuelle interaction avec leur environnement, grâce au langage<br />synchrone Lustre.<br /><br />D'abord, sur la base d'un travail précurseur, nous établissons pour Lustre une méthode de preuve inductive des propriétés de sûreté. Cette méthode est optimisée, afin de prendre en compte au mieux la dynamique des systèmes. Elle est implémentée dans un outil de preuve, Gloups.<br /><br />Ensuite, suivant le modèle de la méthode B, nous définissons un calcul de raffinement pour Lustre. Ce calcul est à la fois adapté à Lustre et exprimé en ce langage. Les obligations de preuve qui assurent la<br />correction du raffinement peuvent être traitées par Gloups. Pour faciliter le développement, un autre outil, Flush, génère automatiquement les obligations pour Gloups.<br /><br />Ainsi, nous utilisons Lustre à la fois comme langage de programmation et comme cadre formel d'un développement maîtrisé. L'intérêt de ce<br />procédé réside dans la simplicité du langage et dans son adaptation aux systèmes réactifs : en ce domaine, notre méthode de raffinement est suffisamment expressive, sans être inutilement compliquée. Des exemples viennent démontrer l'intérêt de la méthode.

Améliorer la connaissance des circulations dans les océans est d'une importance majeure pour la prévision à court et moyen terme de l'évolution du système climatique, ainsi que pour le développement de l'océanographie cotière et de l'océanographie opérationnelle. Les sources d'information disponibles pour accéder à cette connaissance sont, comme en météorologie, les modèles physiques et numériques et les observations. Dans ce contexte, ce mémoire résume l'essentiel de mes travaux de recherche de ces dernieres années, consacrés à la modélisation numérique et l'assimilation de données pour l'océanographie. J'y présente tout d'abord quelques aspects concernant les schémas utilisés dans les modèles numériques. On s'intéresse ensuite au raffinement, éventuellement adaptatif de maillage dans ces modèles, et à son extension naturelle vers le couplage de modèles. Enfin, la dernière partie est consacrée aux méthodes d'assimilation de données, qui visent à fournir un compromis optimal entre observations et prévisions du modèle, et plus particulièrement au développement de méthodes de rang réduit.

L'importance des systèmes temps-réels embarqués dans les sociétés industrialisées modernes en font un terrain d'application privilégié pour les méthodes formelles. La prépondérance des contraintes temporelles dans les spécifications de ces systèmes motive la mise au point de solutions spécifiques. Cette thèse s'intéresse à une classe de systèmes temps-réels incluant ceux développés avec la chaîne d'outils OASIS, développée au CEA LIST. Nos travaux portent sur la notion de délai de bout-en-bout, que nous proposons de modéliser comme une contrainte temporelle concernant l'influence du flot d'informations des entrées sur celui des sorties. Afin de répondre à la complexité croissante des systèmes temps-réels, nous étudions l'applicabilité de cette notion nouvelle au développement incrémental par raffinement et par composition. Le raffinement est abordé sous l'angle de la conservation de propriétés garantes de la correction du système au cours du processus de développement. Nous délimitons les conditions nécessaires et suffisantes à la conservation du délai de bout-en-bout lors d'un tel processus. De même, nous donnons des conditions suffisantes pour permettre le calcul du délai de bout-en-bout de manière compositionnelle. Combinés, ces résultats permettent d'établir un formalisme permettant la preuve du délai de bout-en-bout lors d'une démarche de développement incrémentale.

Le sujet de cette thèse est l'étude de la vérification et de la correction de spécifications B dans le contexte d'une approche CBSE ("Component-Based Software Engineering"). La méthode B est reconnue comme une méthode formelle bien outillée pour développer formellement des logiciels, elle dispose du raffinement et de prouveurs permettant un développement rigoureux. L'approche CBSE consiste à développer des logiciels par assemblage de composants, elle trouve son intérêt pour des systèmes de grandes tailles. Cette thèse comprend trois contributions principales. La première est la mise en évidence de schémas de constructions B basés sur le raffinement et l'inclusion de machines B ainsi que l'étude de ces schémas pour modéliser des relations entre des Systèmes de Transitions Etiquetés (STEs). La deuxième contribution consiste en l'utilisation de deux formalismes : (i) le formalisme UML pour spécifier l'assemblage de deux interfaces (fournie et requise) et de plusieurs composants ainsi que les communications entre composants, (ii) le formalisme B pour vérifier les assemblages. La troisième contribution étudie l'aide à la correction des spécifications B à partir de l'échec de la preuve en B. Cette étude est d'abord générale et indépendante du contexte, puis elle tient compte du contexte CBSE et s'intérresse à la détection et la correction des incompatibilités : pour l'assemblage de deux interfaces, on corrige les adaptateurs en considérant les trois niveaux syntaxique, sémantique et protocole, pour l'assemblage et la coordination de plusieurs composants, on corrige les médiateurs en considérant les niveaux syntaxique et protocole.

Ce travail s'intéresse à la résolution du système de Maxwell dans le domaine temporel sur des maillages héxaédriques orthogonaux localement raffinés de manière conforme ou non-conforme. Une méthode de Galerkin discontinu, reposant sur une approximation centrée pour le calcul des intégrales de surface et un schéma saute-mouton d'ordre 2 pour l'intégration temporelle est présentée. On définit ainsi une classe de schémas non-diffusifs : un équivalent discret de l'énergie électromagnétique est conservée.