L’efficacité des méthodes d’optimisation modernes, associée à l’augmentation des ressources informatiques, a conduit à la possibilité d’utiliser ces algorithmes d’optimisation en temps réel agissant dans des rôles critiques. Cependant, cela ne peut se produire sans porter une certaine attention à la validité de ces algorithmes. Ce doctorat traite de la vérification formelle des algorithmes d'optimisation convexe lors qu'ils sont utilisés pour la guidance de systèmes dynamiques. En outre, nous démontrons comment les preuves théoriques des algorithmes d'optimisation en temps réel peuvent être utilisées pour décrire les propriétés fonctionnelles au niveau du code, les rendant ainsi accessibles à la communauté des méthodes formelles.

En aéroacoustique numérique, la condition aux limites d’impédance temporelle (TDIBC) peut être utilisée pour modéliser un matériau absorbant acoustique localement réactif. Elle permet de calculer l’effet d’un matériau sur le champ acoustique après une distance d’homogénéisation,ce qui s’avère suffisamment précis pour la prédiction de niveaux sonores. L’objectif général de cette thèse est d’étudier les aspects physiques, mathématiques, et numériques des TDIBC, en partant de la littérature physique.La première partie de cette thèse définit des conditions d’admissibilité pour une TDIBC non-linéaire dans la formulation impédance, admittance, et scattering. Il est ensuite montré que les modèles physiques linéaires ont des transformées de Laplace irrationnelle et admettent dans le domaine temporel une représentation oscillante-diffusive à retard, dont l’interprétation physique est donnée. L’analyse permet d’obtenir la TDIBC discrète la mieux adaptée à chaque modèle physique, par opposition à une approche universelle qui consiste à postuler un modèle discret a priori, et suggère des manières élémentaires de calculer les pôles et les poids. La formulation temporelle proposée se réduit à la composition d’un ensemble d’équations différentielles ordinaires avec une équation de transport.La principale contribution de la seconde partie est la preuve de la stabilité asymptotique d’une équation des ondes multidimensionnelle couplée à diverses classes de TDIBC admissibles,dont la transformée de Laplace est une fonction positive-réelle. La démonstration repose sur la formulation d’un problème de Cauchy abstrait sur un espace d’état étendu en utilisant une réalisation de l’impédance, qui peut être de dimension finie ou infinie. La stabilité asymptotique du semi-groupe de contraction correspondant est ensuite obtenue en vérifiant les conditions spectrales du théorème de Arendt-Batty-Lyubich-V˜u.La troisième et dernière partie de cette thèse s’intéresse à la discrétisation des équationsd’Euler linéarisées avec une TDIBC. Elle démontre l’avantage numérique à utiliser l’opérateur de scattering plutôt que les opérateurs d’impédance et d’admittance, y compris pour les TDIBC non-linéaires. Cela est effectué par une analyse d’énergie semi-discrète de l’imposition faible d’une TDIBC générique et non-linéaire dans une méthode des éléments finis de type Galerkin discontinu. En particulier, l’analyse met en évidence que la seule définition d’un modèle discretn’est pas suffisante pour complètement définir une TDIBC. Pour appuyer l’analyse, un modèle physique non-linéaire élémentaire est obtenu et ses propriétés numériques sont étudiées dans un tube à impédance. Ensuite, l’obtention d’une TDIBC retardée large bande depuis les modèles physiques de coefficients de réflexion est démontrée pour les liners acoustique à un degré de liberté.Une discrétisation d’ordre élevée de la formulation temporelle proposée, qui consiste à composer un ensemble d’équations différentielles ordinaires avec une équation de transport, est appliquée à l’étude numérique de deux conduits aéroacoustiques.

L'augmentation du nombre de systèmes interconnectés et l’expansion des données échangées dans les réseaux avioniques ont contribué à la complexification des architectures de communication. Pour gérer cette évolution, une nouvelle solution basée sur un réseau coeur haut débit, e.g., l'AFDX (Avionics Full DupleX), a été implémentée sur l'A380. Cependant, il reste des réseaux bas débit, e.g, CAN ou A429, utilisés pour certaines fonctions spécifiques. Cette architecture réduit le délai de développement, mais en contrepartie, elle conduit à de l’hétérogénéité et à de nouveaux challenges pour garantir les contraintes temps-réel. Pour résoudre ces challenges, une architecture homogène basé sur l'AFDX pourrait apporter de grands avantages, tels que une facilité de l'installation et maintenance, et une réduction de poids et coûts. Cette architecture homogène doit supporter des applications de criticités mixtes, où coexistent les trafics critiques (SCT), Best-effort (BE) et le trafic AFDX actuel (RC). Pour atteindre ce but, nous commençons par évaluer les avantages et les inconvénients des solutions existantes par rapport aux contraintes avioniques. Cela nous conduit à sélectionner le Burst Limiting Shaper (BLS) (proposé par le groupe IEEE Time Sensitive Networking (TSN)) allié à un ordonnanceur Static Priority non-preemptif. Ainsi, nous identifions quatre contributions principales dans cette thèse. Tout d'abord, nous spécifions un AFDX étendu avec le TSN/BLS. Une analyse préliminaire basée sur de la simulation a donné des résultats encourageants pour poursuivre sur cette voie. En second, nous détaillons une analyse temporelle de l'AFDX étendu, grâce au Network Calculus, pour calculer des bornes maximales des délais pire cas des différents types de trafic, pour prouver le déterminisme du réseau et le respect des contraintes temporelles. Une analyse de performance préliminaire montre l'efficacité de la solution à améliorer les délais de RC, tout en garantissant les contraintes. Cependant, cette analyse a aussi montré certaines limitations du modèle en termes de pessimisme. Notre troisième contribution est par conséquent la réduction de ce pessimisme, grâce à une seconde modélisation de l'AFDX étendu, et à une méthode de paramétrage des variables système. Cette méthode permet d'améliorer les performances de RC tout en garantissant les contraintes temporelles du SCT et RC. Finalement, nous validons notre proposition à travers des études de cas avioniques réalistes pour vérifier son efficacité. Les résultats montrent une forte amélioration des délais de RC ainsi que de l'ordonnançabilité de SCT et RC, en comparaison à l'AFDX actuel et au Deficit Round Robin.

Les systèmes dits Sensor Webs sont des middlewares informatiques assurant la communication entre les capteurs et les applications. En tant que véritables médiateurs, la popularité de ces systèmes n’a cessé de grandir depuis l’apparition des tout premiers capteurs. Plus récemment, l’émergence de nouveaux paradigmes tels que l’Internet des Objets (IoT) a complètement révolutionné les systèmes basés sur les capteurs en général. Parmi eux, les Sensor Webs ne dérogent pas à cette règle et doivent désormais répondre à de nouveaux défis, notamment en termes d’intégration, de Qualité des Observations (QoO) et d’adaptation système. Dans ce travail de recherche, nous proposons une nouvelle génération de Sensor Webs capables d’adapter la QoO distribuée de manière autonomique et de manière spécifique à chaque application (QASWS). Premièrement, nous introduisons un framework générique destiné aux chercheurs et développeurs souhaitant concevoir leur propre solution QASWS. Dans un deuxième temps, nous instancions ce framework et proposons un prototype de plateforme d’intégration pour l’évaluation de la QoO à la demande (iQAS). Après avoir évalué ses performances, nous présentons trois cas d’utilisation pour la plateforme iQAS. Finalement, nous concluons cette étude en imaginant l’apport de certains paradigmes transverses vis-à-vis de la QoO dans un futur proche.

Les longueurs d’onde optiques sont une alternative aux liens radio-fréquences pour les transmissions satellite-sol du futur. Elles sont envisagées pour les futurs systèmes de télémesure satellitaires (liens optiques descendants en provenance de satellites LEO) ou de communication (liens optiques bi-directionnels avec des satellites GEO). A sa traversée de l’atmosphère l’onde optique peut être profondément affectée par la turbulence atmosphérique. Elle subit des variations spatiales et temporelles d’amplitude et de phase. Les variations d’amplitudes se traduisent par des variations de la puissance lumineuse collectée (scintillations). Les perturbations de la phase affectent la distribution spatiale de la puissance au foyer du système de détection, qui n’est alors plus limitée par la diffraction. Des pertes peuvent en découler lors du couplage du flux incident à un détecteur optronique ou à une fibre optique monomode. Ces pertes se traduisent par des atténuations du signal reçu et donc par la perte d’informations. Pour s’en abstraire, les études de faisabilité les plus récentes mettent en avant l’utilisation de systèmes d’optique adaptative et de techniques numériques adaptées (codage/entrelacement). Pour limiter la complexité et le coût des systèmes de liens optiques, la définition des techniques de compensation des atténuations peut être menée conjointement. C’est l’objectif principal de cette thèse. Il s’agit d’investiguer les complémentarités des techniques de compensation physiques (optique adaptative) et numériques (entrelacement, codes correcteurs) pour disposer des éléments permettant de définir les systèmes de correction les mieux adaptés.

Au cours des dernières décennies, l’étude de la dynamique autour des points de Lagrange des systèmes Terre-Lune (EMLi) et Terre-Soleil (SELi) a ouvert de nouvelles possibilités pour les orbites et les transferts spatiaux. Souvent modélisés comme des Problèmes à Trois Corps (CR3BP) distincts, ces deux systèmes ont également été combinés pour produire des trajectoires à faible coût dans le système Terre-Lune-Soleil étendu. Cette approximation (PACR3BP) a permis de mettre en évidence un réseau à faible énergie de trajectoires (LEN) qui relie la Terre, la Lune, EML1,2 et SEL1,2. Cependant, pour chaque trajectoire calculée, le PACR3BP nécessite une connexion arbitraire entre les CR3BPs, ce qui complique son utilisation systématique. Cette thèse vise à mettre en place une modélisation à quatre corps non autonome pour l’étude du LEN basé sur un système Hamiltonien périodique cohérent, le Problème Quasi-Bicirculaire (QBCP). Tout d’abord, la Méthode de Paramétrisation est appliquée afin d’obtenir une représentation semi-analytique des variétés invariantes autour de chaque point de Lagrange. Une recherche systématique de connexions EML1,2-SEL1,2 peut alors être effectuée dans l’espace des paramètres : les conditions initiales sur la variété centrale-instable de EML1,2 sont propagées et les trajectoires résultantes sont projetées sur la variété centrale de SEL1,2 . Un transfert est détecté lorsque la distance de projection est proche de zéro. Les familles de transfert obtenues sont corrigées dans un modèle newtonien haute-fidélité du système solaire. La structure globale des connections est largement préservée et valide l’utilisation du QBCP comme modèle de base du LEN.

La sûreté de fonctionnement occupe une place prépondérante dans la conception de systèmes critiques, puisqu'un dysfonctionnement peut être dangereux pour les utilisateurs ou l'environnement. Les concepteurs doivent également démontrer aux autorités de certification que les risques encourus sont acceptables. Pour cela, le concepteurs définissent une architecture contenant un ensemble de mécanismes de sûreté permettant de mitiger ou tout du moins limiter la probabilité d’occurrence des risques identifiés. L'objectif de ce travail est de développer une méthode automatique et générique de synthèse d’architecture assurant formellement le respect d’exigences de sûreté. Cette activité de synthèse est formalisée comme un problème d'exploration de l'espace des architectures c'est-à-dire trouver un candidat appartenant à un espace de recherche fini, respectant les exigences de sûreté. Ainsi nous proposons un processus de résolution complet et correct des problèmes d'exploration basé sur l'utilisation des solveurs SMT. Les contributions principales sont: 1- La formalisation de la synthèse comme un problème de Satisfiabilité Modulo Théorie (SMT) afin d’utiliser les solveurs existants pour générer automatiquement une solution assurant formellement le respect des exigences; 2- Le développement de méthodes d’analyse spécialement conçues pour évaluer efficacement la conformité d’une architecture vis-à-vis d’un ensemble d’exigences; 3- La définition d'un langage KCR permettant de formuler les problèmes d'exploration et l'implantation des méthodes de résolution au sein de l'outil KCR Analyser.

Dans les systèmes informatiques temps réel, les tâches logicielles sont contraintes par le temps. Pour garantir la sûreté du système critique controlé par le système temps réel, il est primordial d'estimer de manière sûre le pire temps d'exécution de chaque tâche. Les performances des processeurs actuels du commerce permettent de réduire en moyenne le temps d'exécution des tâches, mais la complexité des composants d'optimisation de la plateforme rendent difficile l'estimation du pire temps d'exécution. Il existe différentes approches d'estimation du pire temps d'exécution, souvent ségréguées et difficilement généralisables ou au prix de modèles coûteux. Les approches probabilistes basées mesures existantes sont vues comme étant rapides et simples à mettre en œuvre, mais souffrent d'un manque de systématisme et de confiance dans les estimations qu'elles fournissent. Les travaux de cette thèse étudient les conditions d'application de la théorie des valeurs extrêmes à une suite de mesures de temps d'exécution pour l'estimation du pire temps d'exécution probabiliste, et ont été implémentées dans l'outil diagxtrm. Les capacités et les limites de l'outil ont été étudiées grâce à diverses suites de mesures issues de systèmes temps réel différents. Enfin, des méthodes sont proposées pour déterminer les conditions de mesure propices à l'application de la théorie des valeurs extrêmes et donner davantage de confiance dans les estimations.

La complexité et le besoin en bande passante des architectures de communication avionique ne cessent de croitre avec le nombre des calculateurs et l’expansion des données échangées. La technologie AFDX a été introduite pour offrir des communications haut débit (100Mbps) pour les avions de nouvelle génération. Cependant, ce réseau commuté est déployé de manière entièrement redondante, ce qui conduit à des quantités importantes de câbles, augmentant le poids et les coûts d’intégration. Pour faire face à ces problèmes, on propose dans cette thèse l’intégration d’un réseau Ethernet en anneau comme une solution principale pour diminuer le poids et la complexité liés au câblage. Dans ce contexte, notre objectif est de concevoir et valider un nouveau réseau de communication avionique, AeroRing, basé sur de l’Ethernet Gigabit avec une topologie anneau.

L’analyse de compromis d’un modèle système a pour but de minimiser ou de maximiser différents objectifs tels que le coût ou les performances. Les méthodes actuelles de type OOSEM avec SysML ou ARCADIA sont basées sur la classification ; il s’agit de définir les différentes variantes de l’architecture d’un système de base puis d’analyser ces variantes. Dans ces approches, les choix d’architecture sont contraints : la plateforme d’exécution et la topologie sont déjà figées. Nous proposons la notion de « points de décision » pour modéliser les différents choix du système, en utilisant de nouveaux stéréotypes. L’avantage est d’avoir une modélisation plus « compacte » des différentes variantes et de piloter l’exploration des variantes en utilisant des contraintes. Lorsque le concepteur définit l’architecture du système, des points de décisions sont insérés dans le modèle du système. Ils permettent de modéliser la redondance ou le choix d’une instance pour un composant, les variations des attributs d’un composant, ou l’allocation des activités sur les blocs. Les fonctions objectifs sont définies dans un contexte d’optimisation à l’aide du diagramme paramétrique de SysML. Nous proposons des transformations du modèle SysML vers un problème de satisfaction de contraintes pour l’optimisation (CSMOP) dont la résolution nous permet d’obtenir l’ensemble des architectures optimales. Cette transformation est implantée dans un démonstrateur (plug-in Eclipse) permettant une utilisation conjointe de l’outil Papyrus et de solveurs, disponibles sous forme de logiciels libres. La méthode est illustrée avec des cas d’étude constitués d’une caméra stéréoscopique puis d’un drone, l’ensemble étant modélisé avec Papyrus.