Le SGS (Système de Gestion de la Sécurité) est présenté dans l'aviation comme l'approche la plus prometteuse pour améliorer la sécurité. Pourtant, son efficacité perçue en tant qu'approche de management de la sécurité est mitigée. Cette thèse explore comment le SMS a été adopté dans l'aviation dans les années 2010, comme un changement radical dans le management de la sécurité et un moyen de réduire les occurrences d'accidents. Plus précisément, deux questions sont abordées : Comment le SGS de l'aviation tient-il ses promesses en matière de sécurité ? Comment le SGS a-t-il atterri dans l'aviation ?Sur la base d'une revue de littérature et d'une analyse des guides et outils pour le SGS produits par les autorités de l'aviation civile de trois régions représentatives, différentes philosophies du SGS sont mises en évidence : d'une approche basée sur la conformité, s'appuyant fortement sur une customisation minimale de documents génériques mis à disposition par les autorités, à une approche réflexive amenant les organisations aéronautiques à réfléchir sur leurs propres pratiques et à proposer leurs propres mesures pour gérer au mieux la sécurité.Une analyse critique de la manière dont le SGS tient ses promesses est alors effectuée. Elle passe en revue des raccourcis conceptuels (ex : confusion entre sécurité et SGS ; assimilation de la sécurité à la gestion des risques), les écueils méthodologiques, et les biais introduits par la mise en œuvre pratique du SGS.Pourtant, malgré ces limites, le SGS a été massivement adopté dans les industries à haut risque. Une recherche complémentaire s’imposait pour dépasser ce constat. Elle a été réalisée au moyen d'une approche socio-historique combinant l'analyse de traces écrites et l'interview de 18 ‘anciens’ du management de la sécurité déjà acteurs du domaine au moment de l'émergence et de la diffusion du SGS (fin des années 70 à 90 essentiellement). Cette analyse met en évidence les motivations des différents acteurs de la sécurité à changer d’approche de management de la sécurité, allant de l'amélioration de la performance globale, à des enjeux de responsabilité et de transparence. Elle souligne également le rôle du contexte global dans la convergence vers une approche de type SGS, en particulier : l'élan sociétal vers le New Public Management basé sur la gestion des risques et les audits généralisés ; la diffusion des systèmes de management de la qualité dans l’industrie. Enfin, l’histoire des idées autour du management de la sécurité est explorée. Elle souligne le rôle des communautés, en particulier des communautés de pratique au sein des industries, des communautés d'utilisateurs et des communautés scientifiques, ainsi que celui de certains individus et mécanismes qui ont favorisé la transversalité entre communautés. Au final, le SGS s'avère être l'émanation d'un contexte complexe mêlant de multiples aspects interdépendants.Ces constats conduisent à proposer trois voies à explorer, allant crescendo dans leur décalage avec les pratiques actuelles : 1/ Une extension du cadre, de l’horizon temporel et de la portée de l'analyse des risques, et des méthodes de travail plus inclusives dans le processus de gestion des risques ; 2/ Une extension de la définition de la sécurité au-delà de la gestion des risques reconnaissant l'incertitude, et le développement de capacités à faire face aux inévitables imprévus. Cela implique une flexibilité des modes d’action et de décision pour s’adapter aux situations et par suite, une évolution des modèles de gouvernance vers des modèles plus contextualisés et plus inclusifs ; 3/ Dépasser le périmètre de la sécurité pour mieux la manager, en appréhendant la complexité du contexte global et les multiples enjeux avec lesquels elle interagit. Par ailleurs, aborder la question des enjeux multiples sous un angle favorisant les synergies entre eux plutôt les tensions. Cela passe notamment par une révision des modes de gouvernance et structures organisationnelles.

Les phénomènes aéroélastiques ont lieu lorsqu’une structure interagit avec un écoulement qui l’entoure et elles sont une des principaux facteurs qui limitent l’enveloppe de vol des avions.Cette interaction fluide-structure peut entraîner de l’endommagement structurel, immédiat ou du à la fatigue. Depuis le début de l'histoire aéronautique, l'aéroélasticité a toujours été un facteur important dans la conception des avions. De nos jours, les progrès de l'industrie aéronautique conduisent à la conception d'ailes plus efficaces, présentant généralement des géométries plus allongées et l'utilisation de matériaux plus légers et plus flexibles. Ces nouvelles ailes sont plus sujettes que jamais à un comportement aéroélastique, ce qui signifie que le contrôle aéroélastique reste un domaine d'étude important. De plus, les nouveaux designs des drones remettent en question l'aéroélasticité traditionnelle.L'objectif de ce travail est de présenter, analyser et tester une solution innovante qui contrôle le comportement aéroélastique d'une aile d'avion pour des conditions de vol plus sûres et / ou une enveloppe de vol élargie. La solution présentée est basée sur des absorbeurs secondaires utilisés à ce jour sur d'autres applications, comme les ponts suspendus. Le système de contrôle est passif, ce qui signifie qu’aucun apport d'énergie externe n'est requis. Le système est intégré dans l'aile par un volet qui oscille dans l’écoulement. Les avantages de ce volet sont que l'oscillateur secondaire est placé dans l’écoulement pout bénéficier d'un amortissement aérodynamique et qu'il ajoute une masse faible, ce qui est toujours une priorité en aéronautique. Le système de contrôle peut présenter une rigidité non linéaire le rendant efficace aux fréquences large bande. C'est une caractéristique importante car les fréquences de l'aile évolueront avec la vitesse du vent.Afin de présenter et valider ce dispositif de contrôle innovant dans le domaine complexe de l'aéroélasticité non linéaire, une double approche est suivie utilisant à la fois l'analyse expérimentale et des simulations numériques. Concernant l'approche expérimentale, deux bancs d'essais sont créés et testés en soufflerie: une aile bidimensionnelle et une aile tridimensionnelle.Le premier banc expérimental consiste en une configuration d'aile bidimensionnelle à deux degrés de liberté, avec un volet qui peut être bloqué ou débloqué comme troisième degré de liberté, agissant comme oscillateur secondaire. Cette maquette permet de réaliser une preuve de concept du système de contrôle et met en évidence les avantages des caractéristiques non linéaires par rapport à une version linéaire. On observe que l'aile bidimensionnelle présente du flottement classique par coalescence de ses deux modes structuraux. Lorsque le système de commande est débloqué, la vitesse de flottement augmente, ainsi élargissant l'enveloppe de vol. De plus, le système de commande montre de bonnes performances de dissipation des vibrations pendant le régime post-flottement, en particulier lorsqu'il est équipé d'une rigidité non linéaire.

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.

Les assemblages sont le point critique de toutes les industries de construction. Au-delà de permettre la construction de systèmes mécaniques complexes, il en assure la durée de vie, du fait qu’ils ont pour fonction d’assurer le transfert des efforts au sein des structures. Comparée à la technologie d’assemblage par boulonnage, l’assemblage par collage offre des performances mécaniques accrues tout en réduisant la masse embarquée nécessaire au transfert des efforts. Cette technologie intéresse donc particulièrement les industries aéronautiques, spatiales, ferroviaires ou automobiles, pour lesquelles le rapport résistance sur masse est un enjeu majeur. Le sujet consiste à développer des méthodologies permettant de réduire les temps de calcul tout en prenant en compte le comportement réel de l’adhésif pour une meilleure représentativité de la simulation du comportement mécanique sous sollicitation dynamique à l’échelle de la structure. Il est démontré dans la littérature que certains jeux d’hypothèses simplificatrices permettent une représentation précise du comportement mécanique des assemblages collés au travers d’un schéma de résolution analytique. Néanmoins, le champ d’application de ces approches analytiques est souvent trop restrictif. Des schémas de résolution semi-analytique doivent alors être employés pour résoudre le système d’équations différentielles issu des judicieuses hypothèses simplificatrices. A notre connaissance, la technique par macro-élément, développée depuis 15 ans à l’Institut Clément Ader, est une des deux approches semi-analytiques qui existent dans la littérature. Aujourd’hui, cette technique est applicable dans le cadre d’une cinématique de poutre et peut être utilisée pour des éprouvettes de caractérisation ou des assemblages chargés dans le plan. L’objectif de cette thèse est d’étendre la technique par macro-élément à une cinématique de plaque, impliquant alors un système d’équations aux dérivées partielles, afin de pouvoir simuler des assemblages de structures minces sous chargement statique et dynamique quelconque.

Lors de la rentrée atmosphérique d’un véhicule hypersonique, l’écoulement présente une onde de choc détachée enveloppant le véhicule et une couche limite visqueuse au voisinage de la paroi qui conduit à son échauffement. Dans les basses couches de l’atmosphère, l'écoulement évolue d'un régime laminaire à un régime turbulent en raison de l’augmentation du nombre de Reynolds. L’échauffement de la paroi conduit à la détérioration du matériau sous l’effet de l’ablation et de réactions chimiques susceptibles de modifier l’état de surface. Dans le cas d’un écoulement pleinement turbulent, l'effet des rugosités de paroi se traduit par une augmentation du frottement et des échanges de chaleur. Actuellement, on dispose de modèles avec différents degrés de sophistication et de validation qui reproduisent cet effet par augmentation de la turbulence en proche paroi. Concernant le soufflage en paroi, des modèles existent qui permettent de reproduire l'effet d'injection de fluide à la paroi sur le développement de la turbulence. L’objectif de cette thèse est de mettre au point un modèle permettant de tenir compte d'effets conjoints/couplés de rugosité et de soufflage adapté à des approches RANS (Reynolds Averaged Navier-Stokes) de la turbulence, par exemple modèle à deux équations de type k-ω;, dans le contexte d’écoulements hypersoniques. La thèse se déroulera en 3 ans dans le cadre d’une collaboration entre le CEA-CESTA (à proximité de Bordeaux) et l’ONERA-DMAE (Toulouse). Le déroulement se fera comme suit: - Tout d'abord une revue bibliographique la plus exhaustive possible sera entreprise sur la problématique des parois rugueuses avec soufflage. Cette revue doit aboutir à l'élaboration d'une base de données détaillée. On distinguera notamment les écoulements subsoniques incompressibles des écoulements supersoniques et hypersoniques. A partir de cette base de données, la seconde étape de la thèse sera la construction d'un modèle de rugosité/soufflage. - Dans un premier temps, on adoptera une approche avec un couplage faible entre les effets de rugosité et de soufflage. Ainsi, les modèles de rugosité actuels seront couplés à des conditions limites de soufflage pour voir dans quelle mesure une telle approche peut s'appliquer. - Ensuite, on considèrera des approches où les effets de soufflage, notamment sur la turbulence de proche paroi, seront pris en compte en supplément des effets de rugosités dans la formulation du modèle de turbulence. Enfin, on envisage le développement d'un modèle directement à partir de la base de données collectée, dans lequel les effets de rugosité et de soufflage sont fortement couplés. Les différents modèles identifiés seront développés dans un code de couche limite (code CLICET de l'ONERA) puis dans un solveur Navier-Stokes (code CEA). Une phase de validation sur des cas pertinents d'application sera ensuite menée.

Ces dernières années, le développement du système aérien sans pilote (UAS) impliquant des essaims de véhicules aériens sans pilote (UAV) a connu des progrès sans précédent. Cependant, les systèmes de réseau mis en œuvre dans les UAS commerciaux actuels sont souvent des variantes des systèmes de réseau existants. Ainsi, des vulnérabilités préexistantes peuvent persister, tandis que de nouvelles vulnérabilités émergeant des nouvelles propriétés des UAS, telles que la mobilité et l'interconnectivité, sont encore plus préoccupantes. Étant donné que les UAS opèrent dans l'espace aérien civil, la sûreté et la sécurité sont essentielles.Cette thèse a été créée en réponse à une demande croissante. Dans ce rapport de thèse, trois stratégies sont explorées pour chercher à résoudre différentes attaques que l'on peut s'attendre à observer dans un UAS.La première partie de la thèse implique l'utilisation de théories cybernétiques : des techniques d'observation robustes pour réaliser une détection robuste d'anomalies dans un réseau TCP (Transmission Control Protocol). Les travaux se sont concentrés sur la conception d'un observateur robuste basé la méthode des fonctionnelles de Lyapunov-Krasovkii et d'un système de gestion de file d'attente active (AQM) dans un réseau TCP. En exploitant la dynamique du réseau TCP, nous pouvons détecter un trafic réseau anormal.La deuxième partie de la thèse utilise la théorie multifractale pour identifier les trafics présentant une anomalie. Les travaux se sont concentrés sur la conception d'un prototype d'IDS fonctionnel basé sur l'analyse Wavelet Leader Multifractal (WLM) pour identifier des anomalies telles que la congestion du réseau générée par une attaque DoS. Dans l'expérience, nous observons que la signature WLM d'un réseau UAS simulé peut être radicalement différente entre un trafic normal et un trafic affecté par une attaque DoS. Par une simple comparaison analytique entre les différentes signatures, nous pouvons identifier le trafic avec ou sans attaque.La troisième partie de la thèse consiste à utiliser l'intelligence artificielle (IA) pour améliorer les performances de détection. Nous avons introduit un réseau de classification Long Short-Term memory (LSTM) (et d'autres réseaux de neurones) pour augmenter la qualité de détection. Ici, au lieu de cibler une attaque évidente, telle que l'attaque DoS, nous avons tourné notre attention vers une attaque plus délicate, telle que l'attaque Man in the Middle (MITM). En adaptant l'analyse WLM et les principes d'apprentissage automatique, nous avons constaté qu'il est possible d'atteindre un niveau de détection prometteur pour une attaque de falsification des coordonnées géographiques des drones dans un réseau UAS simulé.

Gaz ionisés composés d’électrons, d’ions et de neutres, les décharges plasmas ont déjà démontré leur potentialité pour le développement de systèmes radiofréquences et micro-ondes. Plus particulièrement, le contrôle de la densité électronique et l’aspect allumage/extinction (mode ON/OFF) des décharges plasmas suscitent un intérêt croissant pour le développement d’antennes furtives reconfigurables en fréquence et/ou en diagramme de rayonnement. Ces antennes exploitent principalement deux comportements électromagnétiques des décharges plasmas, le comportement électrique, pour lequel la partie réelle de la permittivité relative du plasma est grandement négative, et le comportement diélectrique lorsque cette dernière est comprise entre 0 et 1.Récemment, un nouveau type d’antenne plasma miniature a été proposé et expérimentalement étudié en bande VHF [1]. Dans son utilisation, le plasma ne se comporte ni comme un bon conducteur électrique, ni comme un matériau diélectrique, mais comme un mauvais conducteur aussi appelé matériau ENG (Epsilon NéGatif). L’antenne consiste alors en un monopole miniature couplé à un résonateur ENG hémisphérique de dimension sub-longueur d’onde obtenu grâce à une décharge plasma. Les travaux présentés dans [1], issus d’une précédente thèse [2], permirent de mettre en évidence un phénomène de résonance associé à un rayonnement électromagnétique de l’antenne plasma miniature. La reconfigurabilité en fréquence de l’antenne a également été observée en modifiant la puissance électromagnétique communiquée au plasma et donc sa densité électronique.Dans ces travaux de thèse, nous poursuivons le développement de cette antenne plasma miniature. Plus spécifiquement, ce travail de recherche a pour but de : • comprendre le phénomène physique opérant au sein du plasma à l’origine du rayonnement électromagnétique de l’antenne plasma miniature • mettre en œuvre des dispositifs de mesure pour évaluer ses performances antennaires, • étudier expérimentalement les propriétés potentielles de durcissement électromagnétique de l’antenne • proposer une modélisation numérique de cette antenne non-standard.Au cours de cette thèse, les différents travaux de recherche ayant été menés afin de répondre aux objectifs sont : • un état de l’art sur les antennes à plasma • le développement d’un modèle analytique afin de proposer une description phénoménologique de la résonance plasmonique, phénomène physique à l’origine du rayonnement électromagnétique de l’antenne • l’élaboration de dispositifs de mesure dédiés à la caractérisation des propriétés de cette antenne • la mesure des performances de l’antenne plasma miniature ainsi que la mise en évidence expérimentale de ses propriétés de durcissement électromagnétique • la mise en œuvre d’une stratégie pour modéliser numériquement cette antenne plasma miniature

Dans cette thèse de doctorat, nous nous intéressons à l'estimation robuste de la phase de la porteuse en utilisant le filtrage bayésien variationnel. La mesure de la phase porteuse est devenue une tâche fondamentale dans de nombreuses applications d'ingénierie telles que le positionnement précis dans le domaine du GNSS. Malheureusement, les mesures de phase obtenues par les techniques traditionnelles de poursuite de phase peuvent être fortement mises à mal par la présence de sauts de phase ambigus, appelés sauts de cycle. Ces derniers peuvent durement impacter les performances des algorithmes de poursuite conduisant, dans le pire des cas, à une perte permanente de verrouillage du signal. Un processus de ré-acquisition est alors nécessaire qui affecte les performances de suivi. Par conséquent, pour résoudre ce problème, nous proposons un filtre non linéaire robuste de poursuite de phase basé sur l'inférence de Bayes variationnelle. Tout d'abord, l'algorithme est développé en supposant une dynamique lente de phase (c'est-à-dire la boucle au premier ordre), puis, son ordre est augmenté en estimant un vecteur d'état formé par la phase et ses dérivées. Les performances de ce nouvel algorithme sont comparées avec celles de techniques conventionnelles (tels que la DPLL (Digital Phase Lock Loop) et la KF (Kalman Filter)-DPLL) en terms de précision d'estimation et d'occurence de sauts de cycle. La comparaison est d'abord effectuée à l'aide de données synthétiques, puis de données GNSS réelles dans un récepteur radio logicielle GNSS. Les résultats montrent que la méthode proposée a de meilleures performances par rapport aux filtres linéaires conventionnels, lorsque le rapport signal sur bruit est faible.

Supposons qu'on image en transmission ou en rétrodiffusion un milieu éclairé en lumière cohérente. Supposons également que ce milieu est tel que la phase du champ rétrodiffusé apparaît en tout point comme aléatoire. On obtient alors un motif également aléatoire constitué de grains: du speckle.Si, de plus, le milieu varie au cours du temps, le signal de speckle fluctue également. Imager certaines statistiques temporelles du signal peut alors permettre d'imager le mouvement: c'est l'objet de l'imagerie de speckle dynamique. Ses applications sont nombreuses : étude de suspensions colloïdales, de séchage de peinture, imagerie médicale. Elle s'appuie souvent sur l'autocorrélation temporelle du signal: la forme de cette dernière renseigne sur le type de mouvement, et son temps caractéristique de décroissance est lié à la vitesse de fluctuation du milieu.Cependant, faute de caméras suffisamment rapides, il a longtemps été impossible d'accéder directement à l'autocorrélation temporelle des signaux rencontrés expérimentalement. L'accès aux caractéristiques du mouvement n'était donc possible que via des méthodes indirectes, comme le contraste, assez imprécises et qualitatives. Toutefois, ces dernières années, la diffusion de plus en plus large de caméras haute cadence (jusqu'à plusieurs dizaines de kHz), a changé la donne. La voie s'est ainsi ouverte à un raffinement considérable des modèles et à des gains importants en précision et en rapidité de traitement.Une telle caméra a été utilisée dans le cadre de ces travaux de thèse. Elle a permis d'imager la vascularisation sous-cutanée sur des zones variées du corps humain. On a ainsi pu évaluer la pertinence de plusieurs paramètres pour imager qualitativement le mouvement: l'efficacité du premier terme de la fonction d'autocorrélation, par exemple, a été mise en évidence. Dans le même temps, on a aussi pu constater certaines limites du speckle dynamique que la très haute cadence ne permettait pas de lever. Ainsi, au-delà d'un certain seuil, augmenter la cadence n'apporte plus d'information, tandis que l'hypothèse de stationnarité du signal est ébranlée par les effets de la pulsation cardiaque. Ces limites ne remettent pas en question l'apport considérable de la haute cadence, mais illustrent à quel point il s'agit d'un changement de paradigme.Pour en prendre la pleine mesure et exploiter au maximum le gain en résolution temporelle permis par les caméras rapides, il est nécessaire, en parallèle des études expérimentales, d'affiner les modèles existants. C'est dans cette optique qu'un travail de modélisation et de simulation du système d'imagerie a été mené. Notre but était de relier le plus précisément possible un type de dynamique du milieu aux statistiques du signal obtenu. Ainsi, il a été possible de redémontrer rigoureusement et de nuancer des résultats tenus pour phénoménologiques dans la littérature, tels que certains modèles d'autocorrélation temporelle. Ces résultats fondent la possibilité, à terme, de remonter à des grandeurs physiques fiables à partir d'un signal de speckle dynamique.Enfin, comme les modèles inverses de speckle dynamique s'appuient sur des statistiques parfois complexes sur les signaux, il convient de s'assurer que celles-ci ne sont pas altérées par des traitements tiers. En particulier, beaucoup d'opérations de traitement du signal, notamment de rééchantillonnage (sur-échantillonnage, sous-échantillonnage, recalage) sont effectuées sans conscience des effets considérables qu'elles peuvent avoir sur les statistiques du signal. Un troisième axe de ces travaux a donc consisté à caractériser ces effets en fonction des méthodes utilisées. Il a par exemple été établi qu'un filtre passe-bas (préalable à un sous-échantillonnage) tend à générer d'autant plus de corrélation longue distance qu'il est resserré en fréquence --- et donc qu'il permet d'éviter l'aliasing. Le même type de résultat a été établi avec les méthodes d'interpolation.

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.