SpaceWire est un standard de réseau embarqué promu par l'Agence Spatiale Européenne qui envisage de l'utiliser comme réseau bord unique dans ses futures satellites. SpaceWire utilise un mécanisme de routage Wormhole pour réduire la consommation mémoire des routeurs et les coûts associés. Cependant, le routage Wormhole peut engendrer des blocages en cascade dans les routeurs et, par conséquent, d'importantes variations des délais de livraison des paquets.Comme le réseau doit être partagé par des flux critiques et non-critiques, les concepteurs réseau ont besoin d'un outil leur permettant de vérifier le respect des contraintes temporelles des messages critiques. Pour réaliser cet outil, nous avons choisi comme métrique une borne supérieure sur le délai pire-cas de bout en bout d'un paquet traversant un réseau SpaceWire. Au cours de la thèse, nous avons proposé trois méthodes permettant de calculer cette borne. Les trois méthodes utilisent des hypothèses différentes et ont chacune des avantages et des inconvénients. D'une part, les deux premières méthodes sont très générales et ne nécessitent pas d'hypothèses restrictives sur le trafic en entrée du réseau. D'autre part, la troisième méthode nécessite des hypothèses plus précises sur le trafic en entrée. Elle est donc moins générale mais donne la plupart du temps des bornes plus serrées que les deux autres méthodes. Dans cette thèse, nous avons appliqué ces différentes méthodes à une architecture de référence fournie par Thales Alenia Space afin d'en comparer les résultats. Nous avons également appliqué ces méthodes à des exemples plus simples afin de déterminer l'influence de différents paramètres sur les bornes fournies par nos méthodes.

Ce travail de thèse s'inscrit dans le projet plus global PRISE (Plate-forme de Recherche pour l'Ingénierie des Systèmes Embarqués) dont l'objectif principal est le développement d'une plateforme d'exécution pour les logiciels embarqués. De tels logiciels sont dits critiques et ils sont, par conséquent, soumis à des règles de conception spécifiques. Notamment, ces logiciels doivent répondre à des contraintes de temps réel et ainsi garantir des comportements temporels prédictifs afin de toujours donner des résultats justes avec le respect d'échéances temporelles. L'objectif de cette thèse est d'évaluer l'utilisation des techniques de la simulation distribuée (et particulièrement de la norme HLA) pour répondre aux besoins de simulation hybride et temps réel de la plate-forme. Afin de respecter ces contraintes et garantir la prédictibilité temporelle d'une simulation distribuée, il faut avoir une vision complète de l'ensemble du problème et notamment des différents niveaux d'actions : applicatif, intergiciel, logiciel, matériel et aussi formel pour la validation du comportement temporel. Cette thèse se base sur la RTI (Run Time Infrastructure, intergiciel HLA) de l'ONERA : le CERTI et propose une démarche méthodologique adaptée à ces différents niveaux d'actions. Des cas d'étude, notamment un simulateur du vol d'un avion, ont été spécifiés, implémentés et expérimentés sur la plate-forme PRISE.

Ce travail de thèse s’inscrit dans le domaine de l’optimisation de structures aéronautiques composites. On cherche à rendre possible le traitement de problèmes de dimensionnement de telles structures, telles que celles rencontrées dans l’industrie aéronautique. Ce type de problèmes présente deux aspects bloquants. En premier lieu, la taille des structures et le type de matériaux rendent le problème d’optimisation à la fois de très grande taille et de variables mixtes (continues, discrètes). D’autre part, le très grand nombre d’analyses de stabilité locale (flambage) nécessaires rend le problème d’optimisation très difficile à traiter en terme de coût de calculs. On cherche donc à résoudre le premier aspect au travers de schémas d’optimisation dits de décomposition qui permettent de décomposer le problème d’optimisation initial en une multitude de sous problèmes d’optimisations pouvant être résolus en parallèle et dont le couplage est résolu par un problème d’optimisation sur un ensemble de variables réduit. L’équivalence théorique entre les différents problèmes d’optimisation (en termes de minima locaux) est prouvée et on présente et développe un schéma adapté à la fois aux spécificités des composites et aux contraintes industrielles. Le second point est résolu de manière originale par le développement d’une stratégie d’approximation des contraintes de stabilité. Cette stratégie de mélanges d’experts se base sur des outils statistiques avancés et se révèle adaptée au comportement des composites. Les deux principales avancées de ce travail sont validées sur des cas test académiques et sur une structure aéronautique réaliste. Le fil directeur de ce travail est la mécanique des structures composites, néanmoins le caractère pluridisciplinaire du sujet nous a conduit à des incursions vers les domaines des statistiques (apprentissage), de l’analyse numérique (étude de l’équation aux dérivées partielles relative au flambage) et enfin de l’optimisation théorique.

Le contexte dans lequel s'inscrivent ces travaux est le projet européen MUSIS, et plus précisément la gestion de satellites équipés d'instruments d'observation optique à haute résolution. Un premier objectif était de concevoir un algorithme capable de construire, en une seule passe et en un temps limité, un plan qui couvre toutes les activités de satellites agiles d'observation de la Terre (observation de zones au sol, manoeuvres orbitales, pointages héliocentriques et géocentriques, vidage de données en parallèle, activations des instruments), qui respecte toutes les contraintes physiques (y compris celles liées à la trajectoire en attitude), et qui satisfasse autant que possible les requêtes d'utilisateurs. Le second objectif était de traiter la version dynamique du problème qui se pose lorsque des requêtes urgentes d'observation arrivent en cours d'exécution du plan journalier, en tenant compte des exigences de qualité et de stabilité des plans et de temps de calcul cette fois très limité. L'algorithme de planification élaboré est une succession de recherches chronologiques en avant, avec des règles de décision dédiées et des mécanismes de backtrack en cas de violation de contraintes. Une approche pragmatique a également été proposée pour résoudre le problème de replanification. Elle consiste à utiliser l'algorithme de planification journalière en jouant uniquement sur les priorités, les poids et les observations candidates. Un environnement expérimental intégrant les mécanismes de décision retenus a été développé. Les expérimentations effectuées sur des instances réalistes attestent des bonnes performances de l'algorithme en termes de temps de calcul et de qualité des résultats, en modes planification et replanification.

Les satellites de communication apparaissent comme une solution particulièrement intéressante pour fournir une connectivité à large bande à un grand nombre d'utilisateurs. La propriété de diffusion naturelle des satellites (et ses bandes de fréquence Ku/Ka) rend leur utilisation évidente pour les services de multidiffusion, multimédia, ainsi que pour l’interconnexion de réseaux à haut débit. Toutefois, les signaux de cette bande de fréquence sont beaucoup plus sensibles aux interférences atmosphériques. La principale innovation permettant de résoudre ces problèmes a été l'adoption du codage et de la modulation adaptatifs. Ceci est le principal moteur de cette thèse car cette adaptabilité rend les systèmes par satellite traditionnels inefficaces. Nous nous concentrons sur un paradigme différent pour traiter ces nouveaux défis. Celui-ci est basé sur l’optimisation conjointe des couches de la pile de protocoles. L'idée fondamentale est le fait que l'adaptabilité de la couche physique doit être suivi au niveau des couches supérieures afin de réaliser une gestion efficace des ressources, ceci afin de respecter les exigences strictes (QoS) des nouveaux services. Nous couvrons plusieurs aspects liés à "l’optimisation réseau"; réaliser une allocation efficace des ressources qui maximise le débit tout en assurant l'équité entre tous les utilisateurs, et ce, en fonction des conditions de canal. Nous avons également mis l'accent sur le choix de la meilleure méthodologie permettant de choisir les outils mathématiques appropriés, l'architecture la plus efficace, des technologies adaptatives sur les couches supérieures, ainsi que la meilleure approche de conception "crosslayer".

Pour certifier un système aéronautique, des études de Sûreté de Fonctionnement (SdF) visent à démontrer qu’il répond à des exigences de sécurité de haut niveau. La complexité des systèmes étudiés ayant évolué, les exigences à démontrer devenant toujours plus nombreuses, les analyses actuelles (e.g. arbre de défaillance) peuvent aujourd’hui présenter des limites d’utilisation. Pour aller à l’encontre de ces limites, l’Ingénierie Dirigée par les Modèles s’est développée et s’intéresse aux études de SdF. L’objectif est alors de 1) modéliser dans un langage adapté (le langage AltaRica a ici été utilisé) les comportements fonctionnels et dysfonctionnels d’un système et de ses composants en présence de défaillances, 2) s’assurer que le modèle est une abstraction valide du système réel et 3) vérifier la tenue des exigences du système par le modèle. Les travaux effectués dans cette thèse se sont intéressés aux deux premiers points. Une méthodologie a été proposée pour spécifier l’abstraction du comportement de composants de systèmes multi physiques. Des bibliothèques AltaRica ont été réalisées pour modéliser des sous-systèmes d’un turbomoteur d’hélicoptère. Les résultats obtenus via le modèle ont été comparés avec ceux des analyses existantes de SdF. Pour les projets futurs où celles-ci ne seraient plus disponibles, un processus de validation a été proposé pour caractériser le degré de revue atteint lors de la simulation d'un jeu de tests sur le modèle. Inspiré du « génie logiciel », ce processus s’étend sur trois niveaux de validation (unitaire ; intégration des composants ; modèle complet) et propose des critères de couvertures applicables et mesurables sur un modèle AltaRica.

Depuis l'avènement de la théorie de l'information, la question de la fiabilisation des transmissions est allée de pair avec l'évolution des technologies et des applications. La fiabilisation des transmissions couvre l'ensemble des techniques permettant de lutter contre les erreurs et les pertes d'un canal de transmission. Parmi les mécanismes existants, la fiabilisation pro-active consiste à mettre en place une redondance au niveau d'un émetteur, celle-ci permettant de compenser à priori les pertes subies par le canal. La fiabilisation pro-active trouve son sens lorsque l'émetteur ne peut avoir d'information sur l'état actuel du canal de transmission, ou lorsque elle est inutile du fait de contraintes temporelles, mais aussi lorsqu'un émetteur doit s'adapter aux contraintes de plusieurs récepteurs. Initialement, les mécanismes de fiabilisation pro-actifs utilisant cette redondance sont connus sous le nom de codes correcteurs. La problématique associée à ces codes est alors une problématique d'optimisation : il s'agit de créer des codes flexibles permettant une génération rapide de la redondance par l'émetteur et une récupération des données initiales par le récepteur à faible coût, tout en conservant la meilleure capacité de correction possible. Par extension, la question de la fiabilisation concerne également l'étude de l'impact de mécanismes de suppression de redondance sur la fiabilité d'un système. Dans des réseaux plus spécifiques, où la question de l’utilisation de la bande passante est cruciale, des mécanismes de compression protocolaire peuvent être mis en place afin de diminuer la proportion de trafic engendrée par les en-têtes protocolaires.

Les services de localisation de personnes et de matériels sont de plus en plus demandés. En environnement extérieur, les outils GPS offrent une réponse à cette demande croissante, avec une précision de l'ordre du mètre en espace dégagé. En intérieur, il n'existe pas d'outil aussi performant. Les solutions commerciales sont coûteuses en équipement. Les propositions de recherche, quant à elles, font appel soit à du matériel coûteux soit à une infrastructure lourde. Enfin, le succès actuel des téléphones mobiles “intelligents” auprès du grand public d'une part, et l'émergence des réseaux de capteurs dans le monde académique nous amènent à étudier des solutions viables y compris pour des mobiles ne disposant que de la réception de signaux radio. L'objectif de cette thèse est de proposer une mécanisme de localisation en intérieur à la fois peu coûteux, sans recours à des équipements dédiés du type UWB ni à des infrastructures supplémentaires, tout en offrant une précision de l'ordre du mètre. Pour cela, nous faisons l'hypothèse que l'utilisateur désirant se localiser est environné de pairs sachant estimer leur position, éventuellement de façon grossière, et que l'utilisateur peut patienter quelques instants pendant que l'algorithme de localisation s'exécute. L'utilisateur collecte alors de façon opportuniste les informations de localisation de tous ces pairs. Dans cette thèse nous étudions les performances en termes de précision d'une méthode de localisation utilisant des inégalités matricielles linéaires (LMI), en faisant varier un grand nombre de paramètres. Nous comparons systématiquement ces performances à celles de l'une des solutions les plus simples, celle du centre de gravité de tous les pairs à portée. Nous améliorons ensuite l'approche LMI en la couplant à une moyenne pondérée dans le temps, qui permet d'obtenir une bien meilleure précision proche du mètre. Enfin, nous terminons par des considérations d'implémentation. Les travaux de cette thèse ont été menés dans le cadre du projet ANR Fusion d'Information de Localisation (FIL).

Cette thèse s'intéresse aux systèmes multiagents dans lesquels les agents échangent des informations de façon à atteindre un but commun. Lors de l'échange d'informations entre agents, il est souhaitable que les agents aient un comportement coopératif, c'est-à-dire qu'ils ne se transmettent que les informations qui leur sont utiles. Nous définissons donc en logique modale quelles sont les informations utiles pour un agent étant donné un besoin en information de celui-ci. A partir de ces travaux, nous travaillons sur la notion d'agent coopératif et en proposons plusieurs définitions. Les échanges des agents sont en général réglementés par une politique d'échange d'informations. Pour qu'une telle politique soit efficace, il faut qu'elle soit cohérente et complète. Nous formalisons ces deux notions en logique déontique pour des réglementations générales. Nous proposons ensuite une méthode pour raisonner avec des réglementations incomplètes et appliquons nos résultats aux politiques d'échange d'informations. Finalement, nous analysons dans quelle mesure il est possible d'être à la fois coopératif et obéissant à une politique d'échange d'informations.

Le système de commande de vol (CDV) est un des systèmes les plus critiques à bord d'un avion. Les fonctions logicielles de ce système sont donc soumises à un effort de vérification important. Chez Airbus, le développement des fonctions critiques suit une approche basée sur des modèles formels, à partir desquels la majeure partie du code embarqué est générée. Certaines vérifications peuvent ainsi s'effectuer dès le niveau de la modélisation formelle, et sont aujourd'hui réalisées par test des modèles dans un environnement de simulation. L'objet de cette thèse est d'étudier comment une technique formelle, le model-checking, s'insère dans ces vérifications amonts. La contribution comporte trois parties. La première partie tire le bilan des études passées d'Airbus sur l'application du Model Checking au système de CDV. Nous analysons notamment les caractéristiques des fonctions de CDV, et leur impact sur l'applicabilité de la technologie. Le deuxième partie complète la précédente par une nouvelle étude, expérimentant le Model Checking sur la fonction Ground Spoiler de l'A380. Les expérimentations ont permis de consolider notre analyse du positionnement du Model Checking dans le processus Airbus. Un des problèmes pratiques identifiés concerne l'exploitation des contre-exemples retournés par le model-checker, en phase de mise au point d'un modèle. La troisième partie propose une solution à ce problème, basée sur l'analyse structurelle des parties d'un modèle activées par le contre-exemple. Il s'agit, d'une part d'extraire l'information pertinente pour expliquer la violation de la propriété cible et, d'autre part de guider le model-checker vers l'exploration de comportements différents, activant d'autres parties du modèle. Un algorithme d'analyse structurelle est défini, et implémenté dans un prototype afin d'en démontrer le concept.