Dans cette thèse, nous étudions l’adéquation de l’architecture distribuée des processeurs pluricoeurs avec les besoins des concepteurs de systèmes temps réels avioniques. Nous proposons d’abord une analyse détaillée d’un processeur sur étagère (COTS), le KALRAY MPPA®-256, et nous identifions certaines de ses ressources partagées comme étant les goulots d’étranglement limitant à la fois la performance et la prédictibilité lorsque plusieurs applications s’exécutent. Pour limiter l’impact de ces ressources sur les WCETs, nous définissons formellement un modèle d’exécution isolant temporellement les applications concurrentes. Son implantation est réalisée au sein d’un hyperviseur offrant à chaque application un environnement d’exécution isolé et assurant le respect des comportements attendus en ligne. Sur cette base, nous formalisons la notion de partition comme l’association d’une application avec un budget de ressources matérielles. Dans notre approche, les applications s’exécutant au sein d’une partition sont garanties d’être temporellement isolées des autres applications. Ainsi, étant donné une application et son budget associé, nous proposons d’utiliser la programmation par contraintes pour vérifier automatiquement si les ressources allouées à l’application sont suffisantes pour permettre son exécution de manière satisfaisante. Dans le même temps, dans le cas où un budget est effectivement valide, notre approche fournit un ordonnancement et un placement complet de l’application sur le sous-ensemble des ressources du processeur allouées à sa partition.

L'objectif de cette thèse est la résolution d’un problème d’optimisation multi-objectif sous incertitudes en présence de simulations numériques coûteuses. Une validation est menée sur un cas test de thermique transitoire. Dans un premier temps, nous développons un algorithme d'optimisation multi-objectif basé sur le krigeage nécessitant peu d’appels aux fonctions objectif. L'approche est adaptée au calcul distribué et favorise la restitution d'une approximation régulière du front de Pareto complet. Le problème d’optimisation sous incertitudes est ensuite étudié en considérant des mesures de robustesse pires cas et probabilistes. Le superquantile intègre tous les évènements pour lesquels la valeur de la sortie se trouve entre le quantile et le pire cas mais cette mesure de risque nécessite un grand nombre d’appels à la fonction objectif incertaine pour atteindre une précision suffisante. Peu de méthodes permettent de calculer le superquantile de la distribution de la sortie de fonctions coûteuses. Nous développons donc un estimateur du superquantile basé sur une méthode d'échantillonnage préférentiel et le krigeage. Il permet d’approcher les superquantiles avec une faible erreur et une taille d’échantillon limitée. De plus, un couplage avec l’algorithme multi-objectif permet la réutilisation des évaluations. Dans une dernière partie, nous construisons des modèles de substitution spatio-temporels capables de prédire des phénomènes dynamiques non linéaires sur des temps longs et avec peu de trajectoires d’apprentissage. Les réseaux de neurones récurrents sont utilisés et une méthodologie de construction facilitant l’apprentissage est mise en place.

Cette thèse porte sur une nouvelle approche pour le contrôle d’écoulement aérodynamique. Cette nouvelle approche est basée sur l’utilisation d’actionneurs plasma. La modélisation numérique peut être une outil puissante entre les mains des scientifiques et des ingénieurs pour comprendre, optimiser et ainsi ouvrir la voie à la commercialisation et l’application de cette technologie. Le couplage entre l’électromagnétisme, le plasma et l’écoulement, nécessite des modèles et des techniques numériques avancées. Le travail présenté dans cette thèse, a pour principaux objectifs : le développement et la validation de méthodes numériques pour simuler efficacement le fonctionnement de certains des plus importants types d’actionneurs plasma. Nous nous sommes intéressés à trois types d’actionneurs plasma : les décharges micro-ondes, la décharge à barrière diélectrique (DBD) et le jet synthétique plasma (JSP). En ce qui concerne les décharges microondes, les objectifs sont plus fondamentaux que pour les autres types d’actionneurs. Il s’est agit de mieux comprendre la création du plasma, son évolution et de calculer l’efficacité énergétique de dispositifs microondes par la simulation numérique. Un schéma couplé implicite (ADI) - FDTD avec un modèle de plasma fluide simplifié est présenté. Cette formulation conserve la simplicité et la robustesse des systèmes de FDTD, tout en dépassant la barrière du critère de stabilité CFL. Elle conduit à un temps de calcul réduit et la possibilité de réaliser des simulations tridimensionnelles de la formation du plasma et de l’évolution d’un plasma dans un champ micro-ondes. Afin d’étudier l’énergie absorbée par le plasma et le transfert vers le gaz sous forme de chaleur ainsi que le changement consécutif de la densité du gaz, un solveur Euler a été couplé avec le modèle EM-plasma en tenant compte des effets de gaz réel. Diverses validations et applications sont ensuite étudiés. Des simulations tridimensionnelles de formation du plasma sont réalisée qui montrent la formation de structures dans une décharge micro-ondes librement localisée. Les effets de chauffage de gaz sur le développement d’un "streamer" et la durée d’un volume pré-ionisé avec des champs sous-critiques sont également calculés. En ce qui concerne les deux autres groupes d’actionneurs, les objectifs de cette thèse se concentrent sur la modélisation de leur fonctionnement et sur la production d’écoulement qui en résulte. Le Jet Synthétique Plasma a été numériquement étudié par trois modèles couplés. Les résultats obtenus sont prometteurs pour l’optimisation du JSP et une meilleure compréhension des mécanismes qui limitent ses performances. L’actionneur DBD a été modélisée en utilisant deux solveurs différents basés sur des modèles physiques similaires - celui développé à l’ONERA et l’autre à LAPLACE. Des études paramétriques ont montré que les modèles donnent une estimation assez précise de la force produite par le DBD par rapport à des mesures expérimentales. Des applications aérodynamiques de contrôle d’écoulement ont démontré les effets possibles de ces actionneurs pour la transition laminaire - turbulente et l’amélioration de la portance. Ces travaux ouvrent une perspective nouvelle dans la conception et l’optimisation de ces actionneurs.

Le calcul réseau (network calculus) est une théorie basée sur l’algèbre min-plus. Il offre un cadre formel de modélisation des réseaux de communication. Il a été utilisé pour certifier le réseau AFDX embarqué dans l’A380 de Airbus. Seulement, les bornes sur le délai annoncés par ces travaux de certification souffrent d’une sur-approximation dans le cas précis de l’agrégation dans un contexte de priorité statique non préemptive. L’objectif de nos travaux est de réduire cette sur-approximation. Dans cette thèse, nous proposons un service résiduel permettant d’obtenir de meilleurs bornes sur le délai dans le cas de la politique à priorité statique non préemptive et de la politique DRR. Nous montrons aussi comment ces deux politiques peuvent être combinées dans une politique hiérarchique à deux niveaux.

Lors d’un développement logiciel, et plus particulièrement d’un développement d’applications embarquées avioniques, les activités de vérification représentent un coût élevé. Une des pistes prometteuses pour la réduction de ces coûts est l’utilisation de méthodes formelles. Ces méthodes s’appuient sur des fondements mathématiques et permettent d’effectuer des tâches de vérification à forte valeur ajoutée au cours du développement. Les méthodes formelles sont déjà utilisées dans l’industrie. Cependant, leur difficulté d’appréhension et la nécessité d’expertise pour leur mise en pratique sont un frein à leur utilisation massive. Parallèlement au problème des coûts liés à la vérification logicielle, vient se greffer la complexification des logiciels et du contexte de développement. L’Ingénierie Dirigée par les Modèles (IDM) permet de faire face à ces difficultés en proposant des modèles, ainsi que des activités pour en tirer profit. Le but des travaux présentés dans cette thèse est d’établir un lien entre les méthodes formelles et l’IDM afin de proposer à des utilisateurs non experts une approche de vérification formelle et automatique de programmes susceptible d’améliorer les processus de vérification actuels. Nous proposons de générer automatiquement sur le code source des annotations correspondant aux propriétés comportementales attendues du logiciel, et ce, à partir de son modèle de conception. Ces annotations peuvent ensuite être vérifiées par des outils de preuve déductive, afin de s’assurer que le comportement du code est conforme au modèle. Cette thèse CIFRE s’inscrit dans le cadre industriel d’Atos. Il est donc nécessaire de prendre en compte le contexte technique qui s’y rattache. Ainsi, nous utilisons le standard UML pour la modélisation, le langage C pour l’implémentation et l’outil Frama-C pour la preuve du code. Nous tenons également compte des contraintes du domaine du logiciel avionique dans lequel Atos est impliqué et notamment les contraintes liées à la certification. Les contributions de cette thèse sont la définition d’un sous-ensemble des machines à états UML dédié à la conception comportementale de logiciel avionique et conforme aux pratiques industrielles existantes, la définition d’un patron d’implémentation C, la définition de patrons de génération des propriétés comportementales sur le code à partir du modèle et enfin l’implémentation de l’approche dans un prototype compatible avec l’environnement de travail des utilisateurs potentiels en lien avec Atos. L’approche proposée est finalement évaluée par rapport à l’objectif de départ, par rapport aux attentes de la communauté du génie logiciel et par rapport aux travaux connexes.

Ces travaux concernent la modélisation formelle d’exigences et les interactions entre agents. Nous y avons développé un langage de modélisation pour les exigences d’un système à élaborer, KHI. En s’inspirant notamment des méthodes KAOS et TROPOS-i*, KHI synthétise les concepts essentiels relatifs aux buts et aux agents. Il permet en particulier d’exprimer la question de la capacité effective des agents à assurer la satisfaction des spécifications qui leurs sont assignées. Nous appelons cette question le problème de l’assignation. Dans KHI, nous exprimons ce problème comme la question de la satisfaction d’un certain nombre de critères de correction par un modèle. Pour donner un formalisme aux concepts de KHI et un moyen de résolution du problème de l’assignation, nous introduisons également une logique temporelle multi-agents, USL. Elle s’inspire des travaux dans le domaine, en particulier ATL*sc et SL. Comme ces derniers formalismes, elle utilise des contextes de stratégies pour exprimer des capacités d’agents à assurer la satisfaction de propriétés temporelles. Elle se distingue des autres formalismes existants principalement par deux aspects : d’abord elle utilise des stratégies non-déterministes. Nous les appelons des multi-stratégies. Nous pouvons ainsi exprimer des propriétés de raffinement entre les multi-stratégies. Par ailleurs, nous utilisons pour USL des exécutions du système qui ne sont pas nécessairement infinies. Nous pouvons alors formaliser les notions d’engagement contradictoire pour un agent et de capacités d’actions conflictuelles pour un ensemble d’agents. Nous réduisons ensuite la satisfaction des critères de correction qui expriment le problème de l’assignation dans KHI à des instances du problème de model-checking pour une version adéquate de USL, USLKHI . Nous donnons un algorithme de résolution pour ce problème, il tourne en espace polynomial. L’ensemble des concepts et des outils présentés est par ailleurs illustré par un cas d’étude décrivant des missions d’observation spatiale.

Ce travail porte sur la vérification de composants logiciels dans les systèmes embarqués critiques avioniques. Les conséquences d’une erreur dans de tels systèmes pouvant s'avérer catastrophiques, il se doivent de respecter leur spécification. La vérification formelle tend à prouver cette adéquation si elle est vraie, ou à produire un contre-exemple si elle ne l’est pas. Les méthodes actuelles ne sont pas capable de traiter les les systèmes industriels. La découverte d’informations supplémentaires (invariants) sur le système permet de réduire l’espace de recherche afin de renforcer l’objectif de preuve: les informations découvertes sont suffisantes pour conclure “facilement”. Nous définissons une architecture parallèle permettant à des méthodes de découverte d’invariants de collaborer autour d’un moteur de kinduction. Dans ce contexte nous proposons HullQe, une nouvelle heuristique de génération d’invariants potentiels combinant un calcul de pré-image par élimination de quantificateurs et des calculs d’enveloppes convexes. Nous montrons que HullQe est capable, automatiquement, de renforcer des objectifs de preuve correspondant à la vérification de patrons de conception courants en avionique. Pour autant que nous sachions, les méthodes actuelles sont incapables de conclure sur ces problèmes. Nous détaillons nos améliorations de l’algorithme d’élimination de quantificateurs de Monniaux afin d’assurer le passage à l’échelle sur nos systèmes. Notre framework formel Stuff est une implémentation de notre architecture parallèle composée de HullQe, d'une technique de découverte d’invariants basée sur des templates, et d'une généralisation de PDR à l’arithmétique.

Les systèmes critiques comme les commandes de vol peuvent entraîner des désastres en cas de dysfonctionnement. D'où l'intérêt porté à la fois par le monde industriel et académique aux méthodes de preuve formelle capable d'apporter, plus ou moins automatiquement, une preuve mathématique de correction. Parmi elles, cette thèse s'intéresse particulièrement à l'interprétation abstraite, une méthode efficace pour générer automatiquement des preuves de propriétés numériques qui sont essentielles dans notre contexte. Il est bien connu des automaticiens que les contrôleurs linéaires sont stables si et seulement si ils admettent un invariant quadratique (un ellipsoïde, d'un point de vue géométrique). Ils les appellent fonction de Lyapunov quadratique et une première partie propose d'en calculer automatiquement pour des contrôleurs donnés comme paire de matrices. Ceci est réalisé en utilisant des outils de programmation semi-définie. Les aspects virgule flottante sont pris en compte, que ce soit dans les calculs effectués par le programme analysé ou dans les outils utilisés pour l'analyse. Toutefois, le véritable but est d'analyser des programmes implémentant des contrôleurs (et non des paires de matrices), incluant éventuellement des réinitialisation ou des saturations, donc non purement linéaires. L'itération sur les stratégies est une technique d'analyse statique récemment développée et bien adaptée à nos besoins. Toutefois, elle ne se marrie pas facilement avec les techniques classiques d'interprétation abstraite. La partie suivante propose une interface entre les deux mondes. Enfin, la dernière partie est un travail plus préliminaire sur l'usage de l'optimisation globale sur des polynômes basée sur les polynômes de Bernstein pour calculer des invariants polynomiaux sur des programmes polynomiaux.

Cette thèse s'intéresse à l'adaptation des lois de pilotage d'un avion de transport civil aux différentes incertitudes qui peuvent affecter sa dynamique. Le procédé de pilotage adaptatif est censé fonctionner en temps réel à bord de l'avion afin d'optimiser la performance boucle fermée en fonction des conditions dans lesquelles il évolue. Les incertitudes peuvent être liées à la méconnaissance des conditions de vol (par exemple la vitesse et l'altitude), à des non-linéarités aérodynamiques inconnues ou encore à la méconnaissance du pilote aux commandes. Les procédés adaptatifs qui répondent à ces problèmes se doivent d'être performants sur l'ensemble du domaine opérationnel de l'avion en présence de perturbations réalistes. D'autres contraintes spécifiques peuvent être ajoutées en fonction du contexte (par exemple des charges limites, la stabilité aéroélastique, etc.). Plusieurs méthodes adaptatives sont testées afin d'adapter le système aux larges incertitudes qui le composent. Elles associent en général un estimateur en ligne (aussi appelé loi de mise-à-jour) à une loi de commande structurée. La synthèse de ces deux éléments peut être réalisée simultanément pour les méthodes adaptatives dites " directes ", comme par exemple le Model Reference Adaptative Control qui utilise la stabilité au sens de Lyapounov. Mais cette synthèse peut aussi être découplée pour les méthodes adaptatives dites "indirectes", ce qui offre un large choix de techniques pour chaque élément (comme les Moindres Carrés pour l'estimation de paramètres physiques incertains et la synthèse sous forme LFR pour le correcteur). Le choix de la méthode dépend fortement du contexte applicatif et des nombreuses contraintes associées. Trois applications sont au cœur de ce mémoire. Elles traitent de l'ajustement de lois de guidage à un modèle pilote inconnu, du contrôle longitudinal de non-linéarités de l'avion, et de la mise au point de lois longitudinale et latérale de pilotage manuel qui s'adaptent à des conditions de vol inconnues. Des méthodes avancées d'analyse linéaire et non-linéaire (dérivées de la µ-analyse et d'algorithmes d'optimisation) sont aussi mises en place pour valider ces systèmes sophistiqués adaptatifs en temps réel. D'une façon générale, les méthodes adaptatives indirectes ont donné le plus de satisfaction. Leur performance est aussi bonne que celle des méthodes directes, mais le fait qu'elles estiment en ligne des paramètres physiques facilite la surveillance temps réel du procédé adaptatif et sa validation.

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.