La logique temporelle linéaire du premier ordre (FOLTL) offre un cadre naturel pour la spécification de systèmes à états infinis mais n'est pas décidable (ni même semi-décidable). Dans cette thèse, nous cherchons à exploiter des fragments décidables de FOLTL pour vérifier, idéalement automatiquement, la correction de systèmes à états infinis. Notre approche s'appuie de manière centrale sur une variante de la propriété du modèle fini. Cette propriété d'un fragment d'une logique affirme que, pour toute formule du fragment, il est possible de calculer une borne telle que, si cette formule est satisfiable, alors elle l'est dans un modèle de taille inférieure ou égale à cette borne. La variante que nous considérons, appliquée à FOLTL, ne borne que le domaine du premier ordre, et pas l'horizon temporel. Ceci permet en pratique de réduire le problème de satisfiabilité de FOLTL à celui, décidable, de LTL. Nos travaux s'organisent en trois étapes. Dans un premier temps, nous exhibons divers fragments relativement expressifs de FOLTL possédant cette propriété. Toutefois, ces fragments seuls ne sont pas suffisant pour y spécifier des exemples réels de systèmes à états infinis. C’est pourquoi, dans un second temps, nous définissons trois transformations permettant d’abstraire des spécifications de systèmes à états infinis vers les fragments décrits précédemment ou existant déjà dans la littérature. Une de ces transformations est totalement automatique tandis que les deux autres requièrent une entrée de la part du spécifieur. Enfin, nous présentons dans un dernier temps l'implémentation et l'évaluation de ces méthodes. Pour ce faire, nous définissons un langage de spécification permettant la modélisation de système à états infinis et adapté à l'application de nos trois transformations. Un prototype permet, en exploitant nos résultats, de générer un problème de satisfisabilité LTL dont la résolution est déléguée à un model checker. Cette approche est ensuite évaluée sur un ensemble de spécifications de systèmes tirées de la littérature.

Dans un contexte de changement climatique, le secteur de l’aéronautique doit réduire ses émissions de CO2. Le gain technologique est l’un des leviers sur lequel peut jouer le secteur pour maitriser ses émissions. Les motoristes ont fortement été impactés par ces contraintes et doivent faire face à des défis importants. Pour remplir ces objectifs, une des pistes potentielles d’amélioration se situe en sommet de roue mobile de la turbine basse pression des turbofans double corps/doubles flux actuels. En effet, il est possible d’ajouter une pièce mécanique en tête de pale de rotor, appelée talon, afin de supprimer l’écoulement de jeu, générateur de pertes, qui prend naissance dans le jeu radial d’une configuration classique de pale. Cela a des conséquences bénéfiques sur le rendement des étages de turbines basse pression, mais ces aménagements entraînent l’apparition de nouveaux phénomènes physiques, eux aussi générateurs de pertes, dont il faut améliorer la compréhension. On retrouve dans la littérature deux principaux phénomènes générateurs de pertes associés à ces géométries. Le premier entraine des pertes de charge lorsque le fluide traverse le talon. Cette physique se déroule en dehors de la veine et n’est donc pas au cœur de l’étude menée au cours de cette thèse. Le second est l’interaction entre le débit dans la veine et celui sortant du talon. Les deux fluides ont des propriétés de vitesse différentes et cela engendre des pertes de mélange. Ce mécanisme est important car il modifie également les conditions d’alimentation des aubages en aval. On retrouve aussi, en marge mais bien présent, des interactions entre le fluide présent dans la veine et celui dans les cavités de la géométrie de talon.Ces conclusions sont principalement issues d’une analyse stationnaire du problème à l’aide de bancs d’essais ou de simulations numériques. Aussi, on ne retrouve que des études pour des points de fonctionnement adaptés. Cette thèse a pour objectifs d’apporter une analyse instationnaire de ces écoulements et d’observer le comportement de ces géométries à des conditions hors-adaptation qui sont susceptibles de modifier les différents mécanismes. Pour cela, deux configurations de turbine basse pression avec pales talonnées, de complexité différentes, ont été utilisées. Des calculs stationnaires et instationnaires ont été réalisés afin de comparer ces deux méthodes. De plus, les géométries réelles ont été comparées à des cas idéaux où le jeu en tête de pale de rotor est considéré comme nul. Cela permet d’isoler l’influence de l’effet technologique sur l’écoulement principal. Ces simulations numériques ont été réalisées à l’aide du code de calcul elsA développé par l’ONERA.Les résultats de ces simulations ont permis de retrouver certaines conclusions de la littérature comme le fait que pour une configuration mono-étage les prédictions de performance faite par un calcul stationnaire sont très proches de celles faites par un calcul instationnaire. Ce n’est plus forcément le cas pour une configuration multi-étage ou bien à des conditions de fonctionnement hors-adaptation comme observé au cours de ces travaux. D’autres résultats sont nouveaux pour la littérature associée à cette problématique. Notamment la mise en évidence d’instabilité dans les cavités du talon. Ces dernières étaient plus ou moins attendues car les géométries rencontrées sont semblables à celles des configurations de cavités de purge dans lesquelles des instabilités peuvent prendre naissance.

Afin d’anticiper de potentiels problèmes thermiques liés à l’éjection de gaz d’échappements à haute température par les moteurs hélicoptères, les industriels ont de plus en plus recours à la simulation numérique. La simulation de la trajectoire et du mélange des gaz d’échappement est cependant complexe et peu intuitive. Elle implique notamment de reproduire correctement les mécanismes physiques tridimensionnels et instationnaires résultant de l’interaction entre le jet chaud issu des moteurs et l’écoulement externe composé du vent relatif, du souffle rotor et d’un potentiel effet de sol. Le jet et l’écoulement externe n’étant généralement pas orientés selon les mêmes directions, l’écoulement résultant peut être assimilé à un écoulement de type jet débouchant. Dans ce contexte, l’objectif de cette thèse était de proposer des méthodologies de simulation permettant de restituer le mélange et la dynamique de l’écoulement pour des jets débouchants représentatifs d’une application hélicoptère(fort niveaux de température et jet décollé de la paroi). Dans un premier temps, une campagne d’essais a été réalisée dans la soufflerie F2 de l’ONERA. L’objectif était de constituer une base de données expérimentale détaillée pour des jets débouchants représentatifs d’une application hélicoptère. Cette base de données expérimentale a alors été utilisée afin d’évaluer la capacité de plusieurs modélisations RANS à restituer les aspects dynamique et thermique de ce type l’écoulement. L’utilisation de modélisations RANS plus avancées pour le flux de chaleur turbulent a également été étudié. D’autre part,des simulations aux échelles résolues SAS-SST et LES ont été conduites et comparées aux données expérimentales. L’analyse du flux de chaleur turbulent résolu a notamment permis d’évaluer la validité des modèles GDH et GGDH pour ce type d’écoulement. Finalement, une simulation SAS-SST a été réalisée sur une configuration industrielle basée sur une maquette d’hélicoptère.

De nos jours, les robots autonomes sont confrontés à des environnements complexes et incertains nécessitant la planification automatique des différentes tâches devant être accomplies pour mener à bien la mission. Dans cette thèse, nous essayons de résoudre des problèmes dans lesquels l’incertitude est modélisée comme un ensemble d’état initiaux possibles de l’environnement, et nous nousintéressons aux méthodes de planification hors-ligne (avant le départ de la mission), le calcul de plan en ligne entraînant un coût de calcul supplémentaire non négligeable pendant la mission. La planification contingente est une de ces méthodes. Celle-ci consiste à calculer un plan contingent traitant l’incertitude du problème tout en laissant la possibilité d’effectuer des décisions en ligne rapides et conditionnéespar des observations de l’environnement. La planification contingente semble particulièrement adaptée aux missions de robotique autonome du fait de la facilité d’embarquabilité des plans contingents, mais celle-ci présente néanmoins une complexité d’autant plus élevée que le nombre d’observations à réaliser est grand. De plus, la réalisation d’une observation en cours de mission peut être coûteuse pour l’agent devant la réaliser. Cette thèse consiste donc `a développer un planificateur contingent traitant des problèmes comportant de l’incertitude sous forme d’un ensemble d’états initiaux possibles en limitant le nombre d’observations du plan. Pour cela, nous avons proposé d’utiliser un planificateur conformant (dont le but est de calculer un plan menant au but du problème quel que soit l’état initial possible et sans réaliser d’observation) afin de calculer le plus de branches conformantes possibles dans le plancontingent. Si un plan conformant ne peut pas être calculé, l’approche se sert ensuite des informations retournées par le planificateur conformant pour sélectionner l’observation à réaliser. Une première approche a été développée puis améliorée au fil de la thèse afin d’aboutir à un planificateur contingent complet, dot´e d’une représentation compacte des états de croyance, et qui contrairement `a une grande partie des planificateurs contingents de la littérature, n’est pas limité aux problèmes de taille contingenteinférieure à un. Les résultats de la comparaison de notre approche avec les planificateurs contingents de la littérature indiquent que malgré un temps de calcul plus élevé que ces planificateurs sur une grande partie des problèmes étudiés, notre approche limite efficacement le nombre d’observations du plan, rendant les plans générés compétitifs en terme de taille et de profondeur.

Le but de cette thèse est de présenter des algorithmes basés vision pour permettre la navigation autonome de la sonde et la caractérisation d'un astéroïde inconnu avec une camera monoculaire pendant la phase d'approche.L'état de l'art de la navigation des sondes interplanétaires est basé sur un précis suivi radiométrique et des mesures optiques utilisés pour reconstruire la trajectoire relative par rapport à l'astéroïde. Dans le future proche le système de suivi radiométrique, le Deep Space Network (DSN), sera fortement surchargé puisque de plus en plus de missions sont conçues et seront opérées pour explorer le Système Solaire interne. La navigation autonome est une des solution envisagées afin de réduire la charge du DSN puisque ces algorithmes de navigation permettront à la sonde de se localiser pendant toutes les phases de la mission sans le support du sol.En outre, les caractéristiques des astéroïdes ne sont pas très bien connues avant l'arrivée car l'estimation avec observation à distance nécessite des hypothèses sur les propriétés du petit corps, comme l'albedo et la densité. Par conséquent il est nécessaire d'estimer pendant la mission les propriétés de l'astéroïde pour permettre une localisation précise et un retour scientifique maximale.La navigation autonome pourrait se mettre en place avec plusieurs senseurs mais les cameras sont normalement choisies car elles sont plus légères, plus compactes et nécessitent moins de puissance si comparées avec des autres senseurs, comme les LiDARs. Ce choix implique que les budgets de masse et de puissance du satellite ne sont pas fortement affectés pendant la phase de conception. Pour ces raisons, l'utilisation des cameras en combinaison avec des algorithmes de traitement d'image assure des bonnes performances de navigation avec des composants légers et rentables.Pendant l'approche à un petit corps la reconstruction de la forme et l'estimation de l'axe de rotation sont des étapes vitales. D'un côté, la forme permet d'avoir une première estimation du champ gravitationnel, avec l'hypothèse de densité constante. En plus, l'estimation de la forme permet d'utiliser les algorithme de navigation basée modèle. De l'autre côté, la connaissance de l'axe de rotation est centrale pour définir les repères de mission et pour estimer la localisation relative par rapport à l'astéroïde.La recherche poursuivie pendant ce doctorat a été divisée en trois sections:1. Premièrement, un algorithme d'estimation de forme basé silhouettes a été développé avec l'hypothèse de connaitre la localisation relative2. Deuxièmement, an algorithme pour reconstruire la forme de l'astéroïde et son axe de rotation a été conçu avec l'hypothèse de connaitre le facture d'échelle et d'avoir une estimation de la trajectoire inertielle3. Enfin, la quantification des incertitudes sur les harmoniques sphériques générées par une reconstruction de forme stochastique a été mise en place avec l'hypothèse d'avoir une densité constante et connue.

L’imagerie à haute-vitesse sans distorsions spatiales est devenue cruciale pour une large gamme d’applications comme la vision industrielle, la reconnaissance du mouvement et l’imagerie de la Terre depuis l’espace. La technologie d’imagerie CMOS a donc évolué vers une modalité de prise de vue appelée « snapshot », grâce au développement des Capteurs d’Image à Obturation Globale. Néanmoins, ce type d’imageurs présente une dégradation des performances due à une sensibilité à la lumière parasite non-négligeable du Nœud de Stockage, qui en limite l’exploitation. Bien que beaucoup de travaux aient été consacrés à la réduction de la Sensibilité à la Lumière Parasite, il existe des interrogations et des manquements relatifs à la caractérisation et la modélisation de cette figure de mérite.Ces travaux s’intéressent au développement d’un cadre pour la modélisation, la caractérisation et l’atténuation de la Sensibilité à la Lumière Parasite dans les imageurs CMOS à Obturation Globale.Le cadre se base sur le développement d’une métrique pour la caractérisation, d’une méthode de simulation et de différentes méthodes de correction en post-traitement dans le but de faire émerger des recommandations pour la conception et d'augmenter les performances des imageurs de manière efficace et peu coûteuse.

Dans de nombreuses applications qui présentent un problème de décision ou d'optimisation combinatoire, il est utile de raisonner à différents niveaux d'abstraction. C'est tout d'abord le cas pour des missions d'exploration multi-robots, où l'on peut s'intéresser premièrement à la répartition de tâches d'exploration entre différents robots, puis à la manière dont chaque robot enchaîne les tâches qui lui sont allouées, et enfin à la décomposition de ces enchaînements de tâches sous la forme de déplacements à coordonner pour éviter des collisions ou pour maintenir des liens de communication. C'est aussi le cas pour la gestion d'une constellation de satellites d'observation de la Terre, pour lesquels on peut décider dans un premier temps de la répartition des tâches d'acquisition candidates entre les différents satellites, puis de l'enchaînement de ces acquisitions pour chaque satellite de la constellation, et enfin des commandes élémentaires à envoyer aux instruments pour réaliser effectivement cet enchaînement. C'est encore le cas pour l'implémentation de fonctions sur une architecture avionique, avec en premier lieu une décision concernant l'allocation de fonctions sur des unités de calcul temps réel, puis une décision concernant l'ordonnancement des fonctions sur chaque unité de calcul, et enfin une décision sur la stratégie de routage des données échangées entre fonctions sur un réseau disponible. D'un point de vue général, il est ainsi nécessaire dans ce type d'applications de considérer différents niveaux de décision couvrant allocation des tâches sur des ressources et ordonnancement des tâches sur ces mêmes ressources. Chaque tâche à considérer peut de plus se décomposer en plusieurs sous-tâches, dans le sens par exemple où une tâche de calcul d'une fonction correspond à l'enchaînement d'une tâche de lecture des données utilisées par la fonction, d'une tâche de calcul proprement dite, et d'une tâche d'écriture des sorties de la fonction dans une zone mémoire donnée. En plus de cela, les contraintes des problèmes de décision à résoudre peuvent être représentées avec différents niveaux d'abstraction. Par exemple, en exploration multi-robots, il existe des contraintes portant sur l'énergie disponible pour les robots. Au moment de la répartition des tâches d'exploration entre les robots, il n'est pas forcément possible pour des considérations combinatoires de considérer un modèle dynamique complexe reliant l'énergie disponible à la puissance consommée à chaque instant. On considère alors une consommation d'énergie forfaitaire pour chaque activité et une capacité maximale pour chaque robot. Le modèle d'énergie complexe peut être pris en compte dès lors que les tâches ont été réparties et que l'on synthétise les déplacements des robots. De manière analogue, pour l'agencement des observations d'un satellite, on peut considérer en première approximation qu'il existe une durée forfaitaire requise pour passer d'une observation à la suivante, avant de considérer des modèles cinématiques plus complexes prenant en compte les capacités des actionneurs gyroscopiques et les caractéristiques des zones à imager. Ce sujet de thèse s'intéresse à la définition de modèles et d'algorithmes de décision utilisables pour gérer ces problématiques de décision hiérarchique.

La blockchain est un registre distribué et décentralisé, permettant de stocker et d’échanger des informations de façon sécurisée, sans tiers de confiance. Pour cela,les informations, appelées transactions, sont regroupées au sein de blocs, qui sont ensuite liés entre eux de façon immuable grâce à des procédés cryptographiques. Le registre sert d’historique de toutes les actions menées par les participants du réseau depuis sa création.C’est une technologie en plein essor, de plus en plus utilisée au quotidien. Cet engouement croissant entraîne une explosion du nombre de transactions, ayant pour conséquence directe une forte augmentation de la taille des principales blockchains.Celles-ci deviennent donc plus compliquées à stocker dans leur intégralité, ce qui peut décourager certains nœuds de stocker toute la blockchain et ainsi réduire le niveau de décentralisation.Dans cette thèse, nous proposons un nouveau type de nœud, appelé low storage(LS) node, qui ne stocke plus les blocs en entier, mais des fragments de ceux-ci codés avec un code à effacement. Pour retrouver le bloc initial, un nœud LS commence par télécharger suffisamment de fragments codés depuis d’autres nœuds LS du réseau,puis procède au décodage.L’intérêt de cette approche est qu’elle permet à certains nœuds de stocker une version codée moins volumineuse de la blockchain tout en contribuant à la décentralisation de la blockchain. Elle facilite ainsi le passage à l’échelle des blockchains qui pose actuellement problème.Ce manuscrit présente également BlockHouse, un système complet permettant la location d’espace de stockage libre entre particuliers. La principale innovation est l’utilisation de contrats intelligents (smart contracts) déployés sur la blockchain qui permettent des paiements automatiques et sécurisés basés sur des preuves de récupérabilité des données régulièrement fournies par les serveurs de stockage.

De nos jours, la conception avant-projet en aéronautique repose majoritairement sur des modèles numériques faisant interagir de nombreuses disciplines visant à évaluer les performances de l’avion. Ces disciplines, comme l’aérodynamique, la structure et la propulsion, sont connectées entre elles afin de prendre en compte leurs interactions. Cela produit un processus d’évaluation des performances de l’avion coûteux en temps de calcul. En effet, une évaluation peut prendre de trente secondes pour les modèles de basse fidélité jusqu’à plusieurs semaines pour les modèles de plus haute fidélité. De plus, à cause de la multi-disciplinarité du processus et de la diversité des outils de calcul, nous n’avons généralement pas accès aux propriétés ou au gradient de cette fonction de performance. En outre, chaque discipline utilise ses propres variables de conception et doit respecter des contraintes d’égalité ou d’inégalité qui sont souvent nombreuses et multimodales. On cherche finalement à trouver la meilleur configuration possible dans un espace de conception donné. Cette recherche peut se traduire mathématiquement par un problème d’optimisation boite noire sous contraintes d’inégalité et d’égalité, aussi connues comme contraintes mixtes, dépendant d’un grand nombre de variables de conception. De plus, les contraintes et la fonction objective sont coûteuses à évaluer et leur régularité n’est pas connue. C’est pourquoi, on s’intéresse aux méthodes d’optimisations sans dérivées et particulièrement celles reposant sur les modèles de substitution. Les méthodes d’optimisation Bayésienne, utilisant des processus gaussiens, sont notamment étudiées car elles ont montré des convergences rapides sur des problèmes multimodaux. En effet, l’utilisation d’algorithmes d’optimisation évolutionnaire ou reposant sur le gradient n’est pas envisageable du fait du coût de calcul que cela implique : trop d’appels pour générer des populations de points, ou pour approcher le gradient par différences finies. Cependant la méthode d’optimisation Bayésienne est classiquement utilisée pour des problèmes d’optimisation sans contrainte et de faible dimension. Des extensions ont été proposées pour prendre en compte ce verrou de manière partielle. D’une part, des méthodes d’optimisation ont été introduites pour résoudre des problèmes d’optimisation à contraintes mixtes. Toutefois, aucune d’entre elles n’est adaptable à la grande dimension, aux problèmes multi-modaux et aux contraintes mixtes. D’autre part, des méthodes d’optimisation ont été développées pour la grande dimension pouvant aller jusqu’aumillion de variables de conception. De même, ces méthodes ne s’étendent que difficilement aux problèmes contraints à cause du temps de calcul qu’ils nécessitent ou de leur caractère aléatoire. Une première partie de ce travail repose sur le développement d’un algorithme d’optimisation Bayésienne résolvant les problèmes d’optimisation sans contrainte en grande dimension. Il repose sur une stratégie d’apprentissage adaptatif d’un sous-espace linéaire réalisée conjointement à l’optimisation. Ce sous-espace linéaire est ensuite utilisé pour réaliser l’optimisation. Cette méthode a été testée sur des cas tests académiques. Une deuxième partie de ce travail traite du développement d’un algorithme d’optimisation Bayésienne pour résoudre les problèmes d’optimisation multi-modaux sous contraintes mixtes. Il a été comparé aux algorithmes de la littérature de manière intensive sur une grande batterie de tests académiques. Finalement, on a confronté le second algorithme à deux cas tests aéronautiques. Le premier cas test est une configuration classique d’avion moyen-courrier à propulsion hybride électrique développé par l’ONERA et l’ISAE-SUPAERO. Le second cas test est une configuration classique d’avion d’affaire développée par Bombardier Aviation. Ce cas test repose sur une optimisation à deux niveaux de fidélité. Un niveau de fidélité conceptuel et un niveau de fidélité préliminaire pour lesquels le problème est respectivement évalué en trente secondes et 25 minutes. Cette dernière étude a été réalisée lors d’une mobilité internationale chez Bombardier Aviation à Montréal (CA). Les résultats ont montré l’intérêt de la méthode mise en place

La fusion nucléaire contrôlée par confinement magnétique dans les réacteurs de type Tokamak et le spatial avec les charges utiles des satellites ont en commun d’utiliser des systèmes haute-fréquence (HF) de forte puissance (du kilowatt au mégawatt) et fonctionnant sous vide. La puissance transmissible par de tels systèmes P_max est limitée par l’effet multipactor, qui apparaît quand les électrons présents dans le système entrent en résonance avec le signal HF. Si leur énergie est suffisante, d’autres électrons peuvent être extraits des parois et la population électronique peut croitre de manière exponentielle. Ce nuage électronique peut perturber le signal transmis, dégrader des surfaces voire provoquer un arc électrique. Bien maîtrisée dans les configurations les plus simples (e.g. : guide d’onde rectangulaire métallique), la prévision du phénomène multipactor est plus difficile dans les scénarios complexes, notamment en présence de champs magnétiques et/ou de matériaux de type diélectriques. Ces deux paramètres influencent aussi bien les trajectoires des électrons que les phénomènes d’émission secondaire à l’origine de l’augmentation de la population électronique. L’objectif de la thèse est de modéliser et comprendre l’apparition du multipactor dans ces configurations complexes. Dans ce cadre, j’ai développé le modèle POTOMAC (Physical simulatiOn TOol for Multipactor in Advanced Configurations). Grâce à POTOMAC, j’ai tout d’abord pu montrer que la précision du modèle d’émission électronique utilisé avait une importance capitale, et ce d’autant plus que la configuration étudiée utilise des matériaux diélectriques. Pour modéliser des géométries réalistes, j’ai proposé une extension en trois dimensions du modèle de Dionne, qui est le seul modèle d’émission électronique capable de prendre en compte la charge déposée dans les diélectriques. Enfin, j’ai montré que l’accumulation de charges électriques à la surface des diélectriques avait un impact considérable sur l’apparition du multipactor, en favorisant ou défavorisant certains modes multipactor. Cette influence a été partiellement vérifiée de manière expérimentale, en collaboration avec un partenaire industriel.