Dans une optique de réduction du bruit engendré par les avions, de nombreux phénomènes restent encore à mieux comprendre et de nombreuses configurations sont à étudier. Un besoin en outils de simulation précis et efficaces se fait donc ressentir pour répondre à ces problématiques de propagation d'ondes. Une approche envisageable est celle des équations one-way. En effet, cette méthode permet de décomposer la résolution des équations en fonction du sens de propagation des ondes le long d'un axe. Ainsi, au sein d'un écoulement, cet axe est naturellement celui de l'écoulement principal. Cependant, l'application des équations one-way dans le cadre de la mécanique des fluides souffre d'une limitation majeure. La complexité des équations résolues (équations d'Euler ou de Navier-Stokes) impose une hypothèse d'écoulement faiblement variable, limitant de ce fait le domaine d'application d'une telle méthode. Le premier objectif a donc été de développer une reformulation de ces équations one-way, dans le but de pouvoir appliquer certaines méthodes permettant la levée d'une telle hypothèse. Pour cela, l'exploitation de deux conditions aux limites non-réfléchissantes a permis la construction d'une factorisation purement numérique de l'opérateur de propagation. A partir de cette méthode, il est ensuite possible d'appliquer des formalismes comme les équations one-way true amplitude ou les séries de Bremmer, permettant de prendre en compte les ondes réfractées et/ou réfléchies. Le second objectif a été de mettre à l'épreuve ces méthodes sur différentes applications. Ces dernières sont constituées d'écoulements variant le long de l'axe de propagation, de conduits à section variable ou partiellement traités acoustiquement (liners acoustiques) ou encore d'un jet chaud subsonique. Dans tous ces cas, les résultats fournis par les approches one-way montrent un bon accord avec les données expérimentales et avec différentes méthodes numériques plus coûteuses.

L’industrie aérospatiale fait face à un nouveau défi : proposer de nouvelles fonctionnalités et de nouvelles missions autour de la Terre, dans le système Solaire et au-delà. Ces nouveautés ne se feront pas sans une amélioration de la performance à bord des satellites, notamment au niveau de l'architecture de communication. C’est la raison pour laquelle l’industrie aérospatiale envisage un changement radical de ses réseaux embarqués, passant du bus MIL-STD-1553 pour le trafic temps réel et Spacewire pour le trafic haut débit, à un réseau «unifié » reposant sur une technologie unique capable de transporter ces deux types de trafic. Au début de la thèse, IEEE Time Sensitive Networking (TSN), la technologie état de l’art d’Ethernet, a commencé à attirer l’attention de différents acteurs du spatial. De fait, le but de cette thèse a été de mettre en évidence l’adéquation de TSN avec les exigences de l’industrie aérospatiale.Afin de résoudre ce problème, nous avons commencé par identifier un ensemble de technologies – Ethernet, ARINC 664, TTEthernet, Time Sensitive Networking et Spacefibre – a priori capables de répondre aux besoins des futures missions. Nous avons ensuite proposé une comparaison qualitative de ces technologies en se basant sur leur compatibilité avec les futures exigences des satellites. Cette comparaison s’est organisée autour de deux thèmes : qualité de service (i.e. performance réseau et tolérance aux fautes) et gestion du temps. Elle nous amènera à sélectionner trois candidats : TTEthernet, Spacefibre et TSN. Tandis que TTEthernet et Spacefibre étaient déjà connus et commençaient même à être intégrés dans des architectures réseaux embarqués satellite au moment d’écrire ce document, Time Sensitive Networking était lui totalement nouveau pour l’industrie aérospatiale.Ainsi, après cette étape préliminaire, nous avons étudié en profondeur les très nombreux standards de TSN. Nous avons identifié IEEE 802.1Qbv dit Time Aware Shaper comme le standard TSN indispensable pour répondre aux exigences en performance réseau des futurs satellites. Nous avons par ailleurs discuté de l’intérêt d’autres standards TSN (i.e. IEEE 802.1Qci, 802.1CB, 802.1AS, 802.1Qbu) qui sont, avec Qbv, en voie d’être inclus dans un profil TSN dédié à l’industrie aérospatiale.Afin de valider la compatibilité de TSN, nous nous sommes intéressés à la génération de configurations TSN. Cette tâche n’est pas aisée car chaque configuration nécessite d’instancier un très grand nombre de paramètres. De fait, ces configurations sont presque toujours générées de manière automatique. Cette automatisation est un véritable levier dans l’industrialisation du TSN, à la fois dans les satellites, et d’autres domaines d’application. Ainsi, nous nous sommes concentrés sur la configuration automatique du standard Qbv afin d’adresser les besoins en performance, considérant que les fonctions de tolérances aux fautes pouvaient être reléguées au niveau applicatif. Alors que les stratégies automatiques reposant sur des émissions planifiées à date fixe dans tous les équipements du réseau étaient très répandues dans l’état de l’art, nous avons proposé une nouvelle stratégie de configuration intitulée Egress TT. En pratique, les configurations Egress TT reposent sur des émissions planifiées à date fixe seulement dans le dernier équipement du trajet de n’importe quel flot. Le délai d’un message entre sa source et le dernier équipement dans son trajet peut être variable. En effet, il dépend de l’instant auquel le message a été émis à sa source et aux potentiels ralentissements qu’il rencontrerait dans le réseau. Néanmoins, ce délai variable est absorbé par une planification des émissions bien choisie au dernier saut. Cette nouvelle stratégie propose un meilleur passage à l’échelle que les stratégies existantes. Elle permet aussi de réduire l’effort de développement nécessaire pour la mise à jour des logiciels applicatifs vers l’architecture réseau nouvelle génération.

De nos jours les avions ne peuvent se passer d'un important réseau embarqué pour faire communiquer les nombreux capteurs et actionneurs qui y sont disséminés. Ces réseaux ayant une fonction critique, en particulier pour les commandes de vol, il est important d'en garantir certaines propriétés telles des délais de traversée ou l'absence de débordement de buffers. Le calcul réseau est une méthode mathématique permettant de réaliser de telles preuves [2]. Elle a joué un rôle clef dans la certification du réseau AFDX, dérivé de l'ethernet, utilisé à bord des avions les plus récents (A380, A350).Le Calcul Réseau se base sur des résultats mathématiques utilisant l'algèbre tropicale. Ces résultats sont relativement simple mais déjà bien assez subtiles pour qu'il soit très facile de commettre des erreurs ou des omissions lors de preuves papier ou de calcul de valeur concrètes. Par ailleurs, les assistants de preuve sont un bon outil pour réaliser une vérification mécanique de ce genre de preuves et obtenir un très haut niveau de confiance dans leurs résultats. Nous formalisons donc avec un tel outil les notions et propriétés fondamentales de la théorie du Calcul Réseau. Ces résultats font intervenir des propriétés sur les nombres réels, tel que des bornes supérieures et des limites de fonctions linéaires donc nous souhaitons utiliser un outil de formalisation capable d'implémenter untel niveau mathématique. Nous utilisons l'assistant de preuve Coq. Il s'agit d'un outil disposant déjà d'un long développement dont la librairie Mathematical Components qui permet de formaliser de l'analyse sur les nombres réels et la construction de structures algébriques comme celles utilisées dans le Calcul Réseau. Le calcul de valeurs effective repose sur des opérations de l'algèbre min-plus sur des fonctions réelles. Des algorithmes sur des sous-ensembles spécifiques peuvent être trouvés dans la littérature [3]. De tels algorithmes et leurs implémentations sont toutefois compliqués. Plutôt que de développer une preuve de la bonne implémentation de ces algorithmes, nous prenons une implémentation existante comme Oracle et nous donnons des critères de vérifications en Coq.[1] Anne Bouillard, Marc Boyer et Euriell Le Corronc. DeterministicNetwork Calculus : From Theory to Practical Implementation. John Wiley& Sons, Ltd, oct. 2018[2] Assia Mahboubi et Enrico Tassi. Mathematical Components. Zenodo,jan. 2021[3] Anne Bouillard et Eric Thierry. « An Algorithmic Toolbox forNetwork Calculus ». In : Discret. Event Dyn. Syst. 18.1 (2008),p. 3-49.

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 le contexte d'une analyse de fiabilité, pour évaluer la position de retombée d'un étage de lanceur de satellite et pour estimer le risque de défaillance associé, il est souvent nécessaire d'utiliser un code de simulation numérique dont les entrées sont des mesures issues de systèmes embarqués. La méconnaissance des incertitudes affectant ces entrées mesurées peut avoir un impact considérable sur la qualité de l'estimation du risque de défaillance. Ces travaux de thèse ont deux objectifs principaux : - Implémenter un algorithme permettant d'acquérir le maximum de connaissances sur la distribution des entrées (sachant que la seule matière première est un jeu de données de petite taille) avant d'utiliser le résultat de cette apprentissage pour quantifier le risque de défaillance. - Effectuer une analyse de sensibilité permettant de comprendre quelles sont les variables d'entrée ou bien les motifs de dépendance en entrée qui jouent un rôle clé dans le processus d'estimation du risque.

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.

L'objectif de cette thèse est d'offrir des outils d'aide à la certification aéronautique de processeurs COTS multi-cœurs. Ces architectures sont par nature parallèles et peuvent de ce fait largement améliorer les performances de calcul. Cependant elles souffrent d'un grand manque de prédictibilité, au sensoù calculer les pires d'exécution même pour des programmes simples est un problème complexe, voire impossible dans le cas général. En effet, les cœurs partagent l'accès à presque toutes les ressources ce qui provoque des conflits(qualifiés d'interférences) entrainant des variations non maîtrisées des temps d'exécutions. Parmi les mécanismes complexes d'un processeur multi-coeur se trouve la cohérence de caches. Celle-ci assure que tous les cœurs lisant ou écrivant dans un même bloc mémoire ne peuvent pas aveuglement ignorer les modifications appliquées par les autres. Afin de maintenir la cohérence de caches, le processeur suit un protocole pré-déterminé qui définit les messages à envoyer en fonction des actions d'un cœur ainsi que les actions à effectuer lors de la réception du message d'un autre cœur.Cette thèse porte sur l'identification des interférences générées par les mécanismes de cohérence de caches ainsi que sur les moyens de prédiction de leurs effets sur les applications en vue de réduire les effets négatifs temporels. La première contribution adresse les ambiguïtés dans la compréhension que les applicants ont de la cohérence de cache réellement présente dans l'architecture. En effet, la documentation des architectures ne fournit généralement pas suffisamment de détails sur les protocoles. Cette thèse propose une formalisation des protocoles standards, ainsi qu'une stratégie, reposant sur les micro-benchmarks, pour clarifier les choix d'implémentation du protocole de cohérence présent sur l'architecture. Cette stratégie a notamment été appliquée sur le NXP QorIQ T4240. Une fois le protocole correctement identifié, la seconde contribution consiste à réaliser une description bas-niveau de l'architecture en utilisant des automates temporisés afin de représenter convenablement les micro-comportements et comprendre clairement comment le protocole de cohérence de cache agit. Ainsi,un framework de génération de modèles génériques a été développé, capable de supporter plusieurs protocoles de cohérence de cache et de représenter différents agencements d'architectures afin de mieux correspondre à l'architecture choisie par le postulant. La troisième contribution explique comment utiliser cette représentation de l'architecture pour exhiber les interférences. Elle propose une stratégie pour détailler les causes et effets de chaque interférence liée à la cohérence de caches sur les programmes.Commençant par une simple analyse de temps d'exécution, les résultats descendent jusqu'au niveau des instructions pour indiquer comment chaque instruction génère et souffre des interférences. L'objectif étant alors de fournir suffisamment d'information à l'appliquant à la fois pour la certification, mais aussi pour définir une stratégie d'atténuation et de maîtrise des effets temporels.Ainsi, cette thèse fournit l'appliquant des outils pour comprendre les mécanismes de cohérence de cache présent sur une architecture donnée et pour exhiber les interférences associées.

Cette thèse est dédiée à la conception et à l'étude d'une structure de boucle de raffinement auto-adaptative pour résoudre de manière fiable les équations intégrales acoustiques. Notre démarche est de revisiter l'ensemble des briques constitutives de cette architecture pour en améliorer l'efficacité algorithmique ainsi que la facilité d'utilisation, et vue d'en démocratiser son usage.Notre approche consista d'abord à étudier un schéma numérique de Galerkin discontinu. Cette méthode rend en effet possible l'utilisation de maillages $hp$ non-conformes et l'optimisation et la simplification de la construction de l'espace d'approximation. Nous fournissons une étude théorique détaillée de cette méthode et démontrons sa stabilité. Un ensemble d'expériences numériques a permis de confirmer le bon comportement pratique du schéma numérique.Nous avons ensuite adapté une méthode de compression matricielle basée sur une approche par interpolation directionnelle $mathcal{DH}^{2}$ ainsi que sa recompression algébrique. Un ensemble d'optimisations originales a été introduite en vue d'obtenir un algorithme efficace dans le cas de matrices issues du schéma de Galerkin discontinu. Nous obtenons textit{in fine} une compression robuste vis-à-vis de la fréquence et de l'hétérogénéité du maillage. Une analyse de complexité ainsi qu'un nombre conséquent d'expériences numériques, dont des comparaisons avec une $mathcal{H}$-matrice, sont également proposés.La dernière partie de la thèse fut d'abord dédiée à la construction d'un estimateur d'erreur textit{a posteriori} adapté au schéma de Galerkin discontinu qui soit fiable et local. Il est basé sur une approche de type résidu. Cet outil est indispensable pour guider le processus de raffinement local du maillage. Nous avons ensuite exploré un ensemble de procédures de raffinement local en $h$ et en $hp$ non-conformes. Cela permit de confirmer l'intérêt d'un raffinement $hp$ non-conforme, qui offre un meilleur taux de convergence de l'estimateur par rapport au raffinement en $h$ conforme. Une autre contribution originale de notre travail est de proposer un estimateur d'erreur qui prenne en compte l'ensemble des contributions à l'erreur globale : l'erreur de discretisation, l'erreur de résolution du système linéaire et l'erreur de compression. Cette finesse de description de l'erreur nous a permis d'automatiser le réglage de l'ensemble des paramètres de la boucle de raffinement auto-adaptative. Nous aboutissons finalement à une architecture de calcul extrêmement simple d'utilisation.

Les systèmes multi-robots se multiplient dans notre quotidien, par exemple dans la robotique de service ou dans l’assistance industrielle ou agricole. Pour rendre ces systèmes autonomes et sûrs, il est indispensable d’embarquer des modules pour gérer automatiquement les pannes, c’est-à-dire la détection d’anomalies, l’évaluation des causes possibles et la décision d’une réaction appropriée (réessayer, remplacer l’action, remplacer un composant, etc). La thèse vise à développer des outils génériques pour construire un module de gestion automatique des pannes, pour analyser ce module et pour valider son comportement. La première ambition est de modéliser le système multi-robots, le raisonnement pour émettre un diagnostic et les propriétés de sûreté requises. Le travail portera ensuite sur les algorithmes pour construire le module de gestion des pannes et l’analyser. Finalement, les outils développés seront validés par l’application à différents scénarios multi-robots réels et simulés.

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.