La vérification de logiciels est une activité dont l'importance est cruciale pour les logiciels embarqués critiques. Les différentes approches envisageables peuvent être classées en quatre catégories : les méthodes d'analyse statique non formelles, les méthodes d'analyse statique formelles, les méthodes d'analyse dynamique non formelles et les méthodes d'analyse dynamique formelles. L'objectif de cette thèse est de vérifier des propriétés temporelles dans un cadre industriel, par analyse dynamique formelle. La contribution comporte trois parties. Un langage adapté à l'expression des propriétés à vérifier, tirées du contexte industriel d'Airbus, a été dé ni. Il repose notamment sur la logique temporelle linéaire mais également sur un langage d'expressions régulières. La vérification d'une propriété temporelle s'effectue sur une trace d'exécution d'un logiciel, générée à partir d'un cas de test pré-existant. L'analyse statique est utilisée pour générer la trace en fonction des informations nécessaires à la vérification de la propriété temporelle formalisée. Cette approche de vérification propose une solution pragmatique au problème posé par le caractère ni des traces considérées. Des adaptations et des optimisations ont également été mises en œuvre pour améliorer l'efficacité de l'approche et faciliter son utilisation dans un contexte industriel. Deux prototypes ont été implémentés, des expérimentations ont été menées sur différents logiciels d'Airbus.

Depuis quelques années, les réseaux de communication déployés au sein d’aéronefs sont toujours plus vastes et plus complexes. Ces bus numériques multiplexent différents flux de données afin de limiter les câbles, mais cela induit des retards sur les transmissions. Les travaux présentés ici portent sur une approche statistique de l’évaluation des performances du pire temps de traversée d’un réseau embarqué de type AFDX. Il s’agit de définir une nouvelle approche visant à associer à un calcul pire cas, une distribution des temps de transmission des messages, en vue notamment de permettre d’apprécier le pessimisme du calcul pire cas. Les méthodes décrites sont applicables dans le cadre plus général d’un ensemble de tâches. Nous proposons trois contributions dans ces travaux. Tout d’abord, une méthode originale d’évaluation de la distribution de la durée de traversée d’un commutateur AFDX qui s’appuie sur une énumération symbolique des scénarios d’ordonnancement dans la file d’attente. Puis, un algorithme efficace de calcul des délais subis par des messages/tâches périodiques lorsque les déphasages initiaux sont connus. Les délais calculés sont exacts ainsi que la distribution de probabilité. Enfin, le calcul de la distribution des délais subis par des messages/tâches dans un cadre général, à l’aide d’une méthode statistique de type Monte Carlo. Des décalages initiaux sont tirés aléatoirement et permettent de nourrir l’algorithme précédent.

Le développement de tests pour les systèmes d’avioniques met en jeu une multiplicité de langages de test propriétaires, sans aucun standard émergent. Les fournisseurs de solutions de test doivent tenir compte des habitudes des différents clients, tandis que les échanges de tests entre les avionneurs et leurs équipementiers / systémiers sont entravés. Nous proposons une approche dirigée par les modèles pour s’attaquer à ces problèmes: des modèles de test sont développés et maintenus à la place du code, avec des transformations modèle-vers-code vers des langages de test cibles. Cette thèse présente trois contributions dans ce sens. La première consiste en l’analyse de quatre langages de test propriétaires actuellement déployés. Elle nous a permis d’identifier les concepts spécifiques au domaine, les meilleures pratiques, ainsi que les pièges à éviter. La deuxième contribution est la définition d’un méta-modèle en EMF Ecore, qui intègre tous les concepts identifiés et leurs relations. Le méta-modèle est la base pour construire des éditeurs de modèles de test et des motifs de génération de code. Notre troisième contribution est un d´démonstrateur de la façon dont ces technologies sont utilisées pour l’élaboration des tests. Il comprend des éditeurs personnalisables graphiques et textuels pour des modèles de test, ainsi que des transformations basées-motifs vers un langage du test exécutable sur une plateforme de test réelle.

Ce manuscrit présente des résultats de recherche concernant une certaine classe de systèmes hybrides. Les systèmes hybrides peuvent être utilises pour la modélisation de systèmes physiques complexes et hétérogènes dont l’évolution dans le temps présente des phénomènes discrets, tels que les commutations des convertisseurs ou les impacts des systèmes mécaniques. De la même manière, la théorie hybride peut être utilisée pour concevoir des contrôleurs hybrides, en général plus performants par rapport aux contrôleurs a temps continu. Dans ce cadre, les résultats de ce manuscrit peuvent être divises en trois parties. D'abord des résultats de stabilité par rapport à un indice de performance de type Hinfini sont présentes pour une classe plutôt large de systèmes hybrides Ensuite, nous introduisons de nouvelles architectures de contrôleurs hybrides pour les systèmes à temps continu caractérisées par le fait que leur état peut être réinitialisé en fonction de la trajectoire. Enfin, nous présentons une technique de synthèse convexe pour la conception d'un contrôleur hybride multi-objectif. La comparaison avec les résultats classique met en évidence les avantages en termes de performance par rapport aux contrôleurs a temps continu classiques, tout en préservant la propriété de robustesse et la simplicité de conception. Bien que la théorie hybride soit en plein développement, ces travaux généralisent certains résultats existants, en améliorant la simplicité d’implémentation des solutions grâce à l'utilisation de la programmation semi-definie. En plus les architectures de contrôleurs hybrides présentées ont l'avantage de simplifier la généralisation de quelques résultats classiques concernant la synthèse optimale par rapport à des indices de performance communs.

Dans ce mémoire, nous présentons une stratégie basée sur une approche hybride dans le domaine temporel, couplant une méthode de résolution des équations de Maxwell dans le domaine 3D (FDTD) avec une méthode de résolution des équations de ligne de transmission, afin de pouvoir simuler des problèmes électromagnétiques de grande échelle. Le mémoire donne les éléments d’hybridation pour deux cadres d’utilisation de cette approche : une approche multi-domaine et une approche multi-résolution ou d’échelle. L’approche multi-domaine est une extension de la méthode FDTD 3D à plusieurs sousdomaines reliés par des structures filaires sur lesquelles on résout une équation de lignes de transmission par un formalisme FDTD 1D. La difficulté est d’abord d’avoir une définition implicite du champ électromagnétique dans la théorie des lignes de transmission, et d’autre part de prendre en compte les effets du sol sur les courants induits au niveau des lignes et sur les champs électromagnétiques. L’approche multi-résolution ou d’échelle est conçue pour étendre les capacités de la méthode FDTD au traitement du routage de câbles complexes ayant une section plus petite que la taille de la cellule. Ce mémoire présente différentes techniques pour évaluer les paramètres de la ligne, basées sur la résolution d’un problème de Laplace 2D, ainsi qu’une méthode de couplage champs/câbles basée sur le courant de mode commun. L’ensemble de ce travail nous a permis de proposer une méthode numérique efficace pour calculer les effets électromagnétiques induits par une source (type onde plane ou dipolaire) sur des sites de grande dimension, composés de plusieurs bâtiments reliés entre eux par un réseau de câbles. Dans ce cadre une application à la foudre a été réalisée.

La principale difficulté pour la navigation autonome d'un robot dans un environnement partiellement ou totalement inconnu vient naturellement du manque d'informations sur l'environnement : on ne peut assurer que le chemin calculé soit aussi court et aussi sûr que le chemin calculé avec une connaissance parfaite de l'environnement. Les informations sur l'environnement sont obtenues au fur et à mesure de la navigation avec un degré variable de certitude qui dépend de l'environnement lui-même, des capacités de perception et la localisation du véhicule, et c'est l'acquisition des informations pertinentes pour la tâche de navigation qui conditionne sa bonne réalisation. Les travaux proposés sont réalisés dans ce contexte : ils définissent une stratégie de navigation qui est basée sur la détermination des zones où l'information est nécessaire au robot pour atteindre le but.

Un grand nombre d'écoulements naturels et industriels mettent en jeu des particules (sédimentation, lit fluidisé, sprays...). Les écoulements chargés en particules sont bien décrits numériquement sous l'hypothèse des particules plus petites que toutes les échelles de l'écoulement. Cette thèse consiste à simuler numériquement une turbulence homogène et isotrope soutenue chargée en particules dont la taille est supérieure à l'échelle de Kolmogorov. Pour se faire une méthode de simulation a été développée au sein du code Thétis puis validée. L'originalité de cette méthode consiste en l'utilisation d'une approche de pénalisation associée à la viscosité dans la zone solide. Les particules sont transportées de façon lagrangienne. Les principaux résultats concernent trois simulations faisant varier le rapport de densité entre le fluide et le solide. Chaque simulation simule le mouvement de 512 particules avec un diamètre 22 fois plus grand que l'échelle spatiale de Kolmogorov remplissant ainsi 3% du volume total. La dispersion des particules est étudiée et montre des comportements comparables à ceux observés pour des particules ponctuelles. Un intérêt particulier est porté sur le régime collisionnel. On observe que la corrélation des vitesses avec le fluide environnant réduit le nombre de chocs frontaux par rapport au cas théorique de particules d'un gaz dense. L'effet de la prise en compte du fluide visqueux entre les particules (couche de lubrification) lors de la collision a été étudiée. L'écoulement moyen à l'échelle des particules est aussi analysé, mettant en évidence l'existence d'une couche de dissipation autour des particules.

Ce travail de thèse porte sur la modélisation des phénomènes de propagation affectant les signaux de navigation par satellite en environnement urbain dense avec une focalisation particulière sur les multitrajets et l'aspect large bande du canal de propagation espace/Terre. Le simulateur de canal pseudo temps-réel développé, SCHUN (Simplified CHannel for Urban Navigation), repose sur une approche hybride physico-statistique. La composante statistique de la modélisation permet essentiellement de générer une ville virtuelle à partir de distributions de bâtiments connues. Le reste de la modélisation s'appuie sur une approche physique simplifiée où les interactions ondes électromagnétiques/ville virtuelle reposent d'une part sur un modèle de macro-diffusion à l'échelle des façades, (3CM (Three Component Model)), et d'autre part sur un modèle physique de masquage du trajet direct par les bâtiments. Les principales méthodes numériques sous-jacentes sont l'optique physique et la théorie uniforme de la diffraction. Le simulateur de canal SCHUN ouvre aujourd'hui des perspectives intéressantes pour la modélisation large bande du canal de propagation espace/Terre. Optimisé pour des temps de calcul raisonnables, alliant une composante statistique à une composante physique simplifiée, ce simulateur a été conçu et validé par des mesures expérimentales pour répondre à des besoins de simulation des systèmes à diversité de satellite, diversité de réception, diversité de polarisation ou encore diversité de fréquence pour des applications de navigation par satellite.

L'objectif de cette étude est de résoudre les qualités de vol d'une aile volante long courrier, au stade de la conception avion. Le concept d'aile volante promet un gain important en terme de performances et de niveau de finesse par rapport aux configurations classiques. Ce gain est obtenu par l'intégration des quatre fonctions principales de l'avion (portance, contrôle, propulsion, transport) dans un seul corps. Ces choix de configuration entraînent des challenges à relever, dont l'obtention de qualités de vol respectant la certification. La configuration initiale étudiée présente de fortes instabilités longitudinales et latérales, une faible autorité en roulis, et des difficultés à effectuer la manœuvre de rotation au décollage. Dans cette étude sont proposées des solutions, combinant des surfaces de contrôle innovantes et des degrés de libertés originaux, qui tirent profit des avantages de la configuration. Les qualités de vols sont résolues dans un processus de résolution avec aussi peu de boucles que possible, et l'impact sur les performances est minimisé. En sortie de ce processus se trouve l'architecture de surface de contrôle optimisée, qui minimise l'impact des qualités de vol sur le coût de la mission.

Dans un contexte de besoins croissants de moyens de communication pour augmenter la sécurité des vols et répondre aux attentes des compagnies et des passagers, le monde de l’aviation civile cherche de nouveaux systèmes de communication pouvant répondre à ces objectifs. Les systèmes de communication sol-bord existants, que ce soit les solutions par satellites en bande L (SATCOM, ...) ou les solutions cellulaires par liaison directe avec le sol (HF, VHF, ...), présentent des limites en terme de capacité, de couverture et de coût. La proposition avancée dans le cadre de cette thèse est d’utiliser les avions comme relais afin de propager les données jusqu’à une station sol. Ce système peut être vu comme un réseau ad hoc mobile dont les nœuds sont les avions civils en vol. Grâce à plusieurs sauts successifs au travers d’avions relais, chaque avion doit pouvoir joindre le sol sans être à portée directe d’une station. Le réseau ad hoc ainsi formé peut ensuite être utilisé pour différentes classes de communications : contrôle aérien, services pour les compagnies aériennes ou pour les passagers. Une telle solution permettrait d’améliorer la couverture des solutions cellulaires classiques en zone continentale. Elle est également applicable en zone océanique où les seuls moyens disponibles sont actuellement le satellite et la HF. On peut imaginer que les coûts de déploiement et de maintenance seraient relativement bas puisque l’infrastructure sol est limitée. Dans cette thèse, nous avons étudié la faisabilité puis les performances qui peuvent être attendues pour ce système de communication aéronautique innovant.