Cette thèse s'inscrit dans le cadre de la mise en œuvre de l'ingénierie dirigée par les modèles (IDM) pour le développement des systèmes embarquées. Ces systèmes ayant généralement des ressources limitées (mémoire et/ou calculs), exigent que le code généré soit le plus optimisé possible. L'objectif de cette thèse est de produire à partir d'un modèle spécifié dans le langage UML, un code assembleur plus compact que le code assembleur produit par les compilateurs de code. Malgré l'évolution croissante des compilateurs optimisés, les compilateurs les plus répandus comme le GCC (Gnu Compiler Collection) sont incapables d'effectuer certains types d'optimisations qu'il est possible d'effectuer à un plus haut niveau d'abstraction dans une phase de pré-génération de code. En effet, certaines informations (liées à la sémantique d'exécution du langage UML) sont perdues lors de la génération de code. Ces informations, utiles pour les optimisations de haut niveau, sont invisibles par le compilateur de code vue qu'il prend toutes les informations liées au système modélisé à partir du code généré. Nous proposons ainsi une nouvelle approche dirigée par les modèles pour le développement des systèmes à ressources limitées, qui élimine l'étape de la génération de code en remplaçant cette étape par une compilation directe des modèles. Nous avons développé le premier compilateur de modèles UML (GUML : le front-end UML pour le compilateur GCC) qui génère directement de l'assembleur (sans passer par un langage de programmation) à partir des modèles UML. GUML permet de compiler les classes, les activités et les machines à états UML. Il permet de générer, en compilant certaines machines à états, un code assembleur plus compact que le code assembleur produit par GCC. Deux optimisations de GCC sont améliorées : l'élimination de code mort et l'élimination des expressions redondantes.

Aujourd'hui, les réseaux de communications sont largement utilisés pour relier les points de ressources, qui permettent la transmission de données à distance, de réduire la complexité dans le cadre de câblage et les coûts de support et de fournir l'aise dans la maintenance. En raison de ces avantages, les réseaux ont été introduits dans les systèmes automatiques au cours de ces dernières décennies et de nouveaux protocoles de réseau industriel ont été également développés pour assurer le contrôle à distance. Les systèmes contrôlés en réseau SCR (Networked Control System NCS) sont des systèmes automatiques traditionnels où les actionneurs, les capteurs, les contrôleurs et des autres composants sont distribués autour d'un réseau de communication, qui peut être partagé ou non avec d'autres applications. Les données de commande et de diagnostic sont échangées entre les composants du système (capteur, contrôleur, actionneur) via ce réseau partagé. Cette nouvelle architecture de système de contrôle introduit des problèmes originaux, en termes de retard variable affectant la transmission, des pertes de paquets, etc. Dans l'objectif de maintenir de bonnes performances du module de diagnostic face à des éventuelles variations introduites par le réseau, il est intéressant d'introduire des nouvelles approches. Nous avons rapporté les résultats relatifs aux techniques d'estimation optimale à base de filtre de Kalman, de façon à constituer un document aussi complet que possible traitant la génération de résidus et l'isolation des défauts dans SCR. Notre contribution consiste, dans un premier temps, à développer un modèle d'état d'un système contrôlé via un réseau. En deuxième temps, nous proposons un générateur de résidus en se basant sur les hypothèses simulant le retard induit par le réseau. Finalement, nous développons un filtre isolateur pour identifier directement les défauts affectant les actionneurs dans un SCR.

Le problème abordé dans cette thèse concerne la productionautomatique de données de test permettant de prouver des propriétés de programmes. Nous nous situons ainsi à mi-chemin entre le domaine du test et celui de la vérification de programmes. Les travaux dans le domaine du test ont conduit à des outils semi-automatiques d'utilisation simple, mais qui reposent sur des hypothèses difficilement vérifiables en pratique. Dans le domaine de la vérification, des outils basés sur des méthodes formelles ont été développés, mais ils nécessitent un utilisateur expert dans les techniques de preuve utilisées par l'outil. Cette situation est due aux problèmes d'indécidabilité engendrés par la puissance des formalismes traités. La thèse que nous présentons est qu'il est possible de développer des méthodes formelles automatiques pour prouver des propriétés de programmes, à condition de considérer des formalismes restreints. Notre principale contribution est une nouvelle approche pour la vérification de programmes, intégrant les techniques de test et d'analyse statique. Nous proposons une méthode formelle de génération de jeux de test finis complets permettant de prouver qu'un programme vérifie une propriété donnée. Cette méthode utilise le texte du programme et de la propriété, qui doivent appartenir à certaines classes de programmes (ou de propriétés). Ces classes sont représentées par des hiérarchies de schémas, qui peuvent être vues comme modélisant des hypothèses de test. Tout programme appartenant à un de nos schémas et passant le jeu de test avec succès vérifie la propriété testée. Pour une propriété donnée, notre méthode est complètement automatique et ne nécessite donc aucune compétence particulière de l'utilisateur. Nous avons implanté cette méthode dans un prototype (traitant un langage fonctionnel restreint), pour le cas de propriétés s'exprimant en termes de longueurs de listes.

Ce travail se place dans le cadre des réacteurs nucléaires de 4ème génération tels que les réacteurs à neutrons rapides et caloporteur gaz (RNR-G), pour lesquels des matériaux réfractaires comme le nitrure de titane (TiN) enroberont le combustible afin de permettre la rétention des produits de fission. Cette étude a porté sur le comportement thermique intragranulaire du xénon dans des échantillons de TiN obtenus par frittage à chaud sous charge. Le rôle de la microstructure sur le comportement thermique du xénon a été étudié. Plusieurs lots ont ainsi été synthétisés sous différentes conditions de température et de composition de la poudre initiale. Le xénon a été introduit par implantation ionique. Les échantillons ont ensuite subi des traitements thermiques entre 1300°C et 1600°C, soient les températures accidentelles envisagées. Un transport majoritaire du xénon vers la surface a été mis en évidence. Ce dernier est ralenti lorsque la température de frittage augmente. Des différences de comportement ont été observées selon les poudres mises en oeuvre dans la synthèse et selon l'orientation cristalline du grain considéré. Le relâchement du xénon a également été corrélé à l'oxydation de TiN. Des bulles de Xe dès 0,38 % atomique ont été observées. Leur taille est proportionnelle à la concentration en Xe et augmente avec la température de recuit, d'où une certaine mobilité du Xe au sein de TiN. Plusieurs mécanismes pouvant expliquer cette mobilité sont proposés. En complément, des calculs ab initio ont confirmé le caractère fortement insoluble du Xe dans TiN et révélé que les bilacunes sont les plus favorables à l'incorporation du xénon au sein de ce matériau.

La biomasse est appelée à représenter une part croissante de la consommation mondiale d'énergie primaire et la recherche de l'optimisation de l'usage d'une telle ressource, abondante mais pas pléthorique, s'impose. Cette thèse pose la question de la place, dans cette optimisation, des biocarburants de deuxième génération, en se focalisant sur la voie thermochimique, et plus particulièrement sur la synthèse de carburants liquides par le procédé Fischer-Tropsch qui permet d'obtenir des hydrocarbures du type naphta, kérosène et gazole. Pour traiter cette question, une démarche d'évaluation est proposée, qui comporte : - une évaluation à l'échelle des procédés, appliquée à une famille comportant au départ une centaine d'options, - une approche systémique pour évaluer l'insertion des procédés dans le système énergétique français futur. La mise en œuvre de cette démarche d'évaluation montre comment : - les procédés thermochimiques de production de biocarburants de deuxième génération permettent d'associer la biomasse et d'autres énergies primaires moins limitées pour maximiser le transfert de carbone renouvelable de la biomasse dans des carburants liquides, mais à des coûts qui restent élevés ; - la réponse à la question de l'optimisation de l'usage de la biomasse et de la place à donner aux biocarburants dépend fortement de l'évolution globale du système énergétique et de la faisabilité du stockage du CO2.

Cette thèse a porté sur le développement pour la biologie de la microscopie par génération de troisième harmonique (THG), qui permet la visualisation sans marquage de cellules et de tissus avec une résolution sub-micrométrique. Son application en biologie était jusqu'à présent limitée par le manque d'études du mode de création du signal dans l'échantillon, des sources de contrastes biologiques endogènes ainsi que de la phototoxicité induite. Le travail présenté ici a essentiellement porté sur ces trois questions. Nous avons d'abord étudié théoriquement et expérimentalement l'influence de la structure de l'échantillon et de la focalisation du faisceau excitateur sur le signal THG. Nous avons montré que l'imagerie THG agit sur l'échantillon comme un filtre passe! -bande pour les fréquences spatiales et qu'ajuster la focalisation de l'excitation permet de moduler la visibilité de structures au sein d'un système complexe selon leur forme. Par ailleurs, nous avons caractérisé les propriétés optiques de différents liquides biologiques, qui prédisent qu'un corps lipidique dans un environnement aqueux doit constituer une source efficace de signal intracellulaire. Nous avons démontré que de telles structures peuvent effectivement être suivies et quantifiées par microscopie THG dans de nombreux types de tissus biologiques non marqués, ouvrant la voie à des applications en physiopathologie. Finalement, nous avons appliqué la microscopie THG à la visualisation in vivo et sans marquage du développement embryonnaire précoce chez la drosophile. Sur ce modèle, nous avons étudié les mécanismes de phototoxicité liés à l'imagerie THG et démontré la possibilité de visualiser les embryons en 3D sans perturbation du développement et de quantifier les mouvements morphogénétiques à partir des séquences obtenues.

La majeure partie des travaux sur les problèmes d'ordonnancement se placent dans le contexte où les ressources sont disponibles en permanence. Ce qui en réalité n'est pas toujours le cas. Nous nous plaçons dans le contexte d'indisponibilités connues ; nous nous intéressons plus particulièrement aux problèmes de type job shop avec des périodes d'indisponibilité flexibles et des tâches pouvant éventuellement être interrompues par les périodes d'indisponibilité. L'intégration de ces contraintes rend les problèmes d'ordonnancement nettement plus difficiles à résoudre. La flexibilité que nous considérons peut être relative à au moins l'un des points suivants : déplacement de la période d'indisponibilité dans une fenêtre de temps, modification de la durée de la période d'indisponibilité, interruption d'une tâche par une période d'indisponibilité, ensuite reprise avec une éventuelle pénalité.Dans cette thèse, nous avons proposé des modèles mathématiques pour le problème. En plus de la résolution des problèmes considérés, le but de ces modélisations est de permettre d'analyser l'impact des différentes contraintes et d'évaluer la qualité des méthodes approchées que nous proposons. Ces dernières permettent de construire très rapidement un ordonnancement en se basant sur des règles de priorité. Les solutions sont aussi utilisées pour notre approche basée sur la génération de colonnes. Cette approche s'adapte bien à différents fonctions objectif et permet d'intégrer relativement facilement plusieurs contraintes. De nombreuses expérimentations ont été menées pour valider les méthodes proposées.

Dans les années 90, la commission européenne a sollicité la mise au point d'un système de contrôle commande et de signalisation ferroviaire commun à tous les réseaux des états membres : le système ERTMS " European Railway Traffic Management System ". Il s'agit d'un système réparti complexe dont le déploiement complet est long et coûteux. L'objectif global consiste à diminuer les coûts de validation et de certification liés à la mise en œuvre de ce nouveau système en Europe. La problématique scientifique réside dans la modélisation formelle de la spécification afin de permettre la génération automatique des scénarios de test. Les verrous scientifiques, traités dans cette thèse, sont liés d'une part à la transformation de modèle semi-formel en modèle formel en préservant les propriétés structurelles et fonctionnelles des constituants réactifs du système réparti, et d'autre part à la couverture des tests générés automatiquement. Les constituants sont sous la forme de boîte noire. L'objectif consiste à tester ces derniers à travers la spécification ERTMS. Nous avons développé une approche de modélisation basée sur le couplage de modèles semi-formels (UML) et de modèles formels (Réseaux de Petri). Ce couplage se fait à travers une technique de transformation de modèles. Nous avons développé ensuite une méthode de génération automatique de scénarios de test de conformité à partir des modèles en réseaux de Petri. Les scénarios de test ont été considérés comme une séquence de franchissement filtrée puis réduite du réseau de Petri interprété représentant la spécification. Ces scénarios ont été exécutés sur notre plateforme de simulation ERTMS

La génération d'harmoniques d'ordre élevé par focalisation d'impulsions laser femtosecondes et intenses dans des gaz permet d'obtenir des trains d'impulsions attosecondes dans l'XUV. Dans cette thèse, nous présentons une technique destinée à optimiser l'efficacité de génération, puis nous montrons comment la caractérisation du rayonnement permet l'étude de la dynamique des molécules en champ fort. Dans une première partie, par une manipulation de sa phase spatiale, nous transformons le profil du faisceau laser infrarouge au foyer afin d'agrandir le volume de génération. Nous mettons en évidence la possibilité de créer un profil carré, élargi d'un facteur 2.5 par rapport au profil gaussien. Nous étudions ensuite la génération d'harmoniques dans les gaz rares par un tel faisceau, à la fois expérimentalement et numériquement. Bien que nous n'ayons pu observer d'augmentation significative du signal harmonique, les simulations effectuées à plus forte énergie indiquent un gain d'efficacité. Dans une seconde partie, nous montrons que le spectre et la phase spectrale du rayonnement harmonique issu d'un ensemble de molécules linéaires alignées présentent des structures liées aux caractéristiques des molécules. Nous mettons en évidence la présence d'un saut de phase lié à un phénomène d'interférences quantiques lors de l'étape de recombinaison. Nous étudions la dépendance de ce saut de phase en fonction de différents paramètres, tels que l'orientation des molécules ou l'éclairement de génération. Ces mesures permettent l'étude de la dynamique électronique lors de la recombinaison du paquet d'ondes électroniques. De plus, elles devront servir de support pour les nouvelles modélisations du comportement des molécules en champ intense.

L'industrie électronucléaire, pour faire face aux besoins énergétiques croissant, à besoin de développer une nouvelle génération de réacteur : la quatrième génération. Parmi les six candidats, on trouve les réacteurs à sels fondus, qui, en configuration rapide, semble avoir de très bonnes propriétés : la régénération est facilement accessible tout en gardant des coefficients de contre-réaction négatifs. Le procédé de retraitement du sel combustible n'est toutefois toujours pas établi de manière définitive. Beaucoup d'incertitude sur les paramètres physicochimiques des sels combustibles empêchent de définir de manière précise chaque étape du procédé. Grâce à la simulation numérique nous avons pu étudier le comportement du cœur du réacteur couplé à une unité de retraitement de référence. De cette manière nous avons pu quantifier les flux de chaleurs et les radiations pour identifier les étapes qui nécessiteront une attention particulière lors du dimensionnement. Nous avons aussi pu identifier les éléments pour lesquels une mauvaise extraction mettrait en péril le bon fonctionnement du réacteur. Enfin, toujours grâce à la simulation numérique, ce travail présente une analyse des sensibilités du procédé de retraitement sur un certain nombre de grandeurs physique représentative du cœur du MSFR.