Aujourd'hui, les systèmes embarqués sont de plus en plus utilisés pour contrôler les systèmes complexes. Dans ce travail de thèse, nous nous intéressons aux systèmes embarqués critiques utilisés pour la commande de systèmes de transport comme les systèmes ferroviaires. Le but de ce travail est de permettre la conception de systèmes tolérants aux fautes pour le contrôle-commande des systèmes de transport. Nous proposons une nouvelle approche de modélisation des systèmes embarqués temporisés pour le diagnostic de leurs fautes. Elle est basée sur une décomposition structurelle du système et sur une extension de la diagnosticabilité modulaire au contexte des systèmes temporisés. On distingue deux approches de base pour le diagnostic de fautes des SED, une approche basée sur les diagnostiqueurs et une approche basée sur les signatures temporelles causales (STC). La principale limite de l'approche diagnostiqueur réside dans la gestion de l'explosion combinatoire. Dans ce travail, notre verrou principal est de combattre cette limite. Nous proposons une nouvelle méthode basée sur l'ingénierie par les modèles pour le diagnostic des systèmes embarqués critiques. D'autre part, la limite majeure de l'approche STC est la garantie de la cohérence d'une base de STC. Un deuxième niveau de difficulté réside dans l'interprétation des événements en entrée du système de diagnostic dans le cadre de l'hypothèse de défaillances multiples. Dans ce travail, nous proposons deux méthodes différentes pour la vérification de la cohérence d'une base de STC et nous proposons un algorithme d'interprétation basé sur le concept de monde qui garantit la correction du diagnostic

Cette thèse s'attache à définir une méthodologie globale permettant d'augmenter le niveau de sûreté et de sécurité face à des fautes logiques transitoires (naturelles ou intentionnelles) survenant dans un système intégré matériel/logiciel, de type carte à puce. Les résultats peuvent être appliqués à tout circuit construit autour d'un cœur de microprocesseur synthétisable et d'un ensemble de périphériques spécialisés. Les méthodes de protection portent simultanément, sur le matériel, le logiciel d'application et les couches d'interface (en particulier, le système d'exploitation). Les modifications sur des descriptions de haut niveau on été privilégiées pour leurs avantages en terme de généralité, configurabilité, portabilité et pérennité. L'approche proposée vise un bon compromis entre le niveau de robustesse atteint et les coûts induits, aussi bien au niveau matériel qu'au niveau performances. Elle est appliquée et validée sur un système significatif, représentatif d'un système embarqué monoprocesseur.

Les systèmes embarqués communicants sont de plus en plus présents dans notre environnement quotidien sous formes de PDA, téléphones portables, etc. Ces sytèmes se doivent d'être ouverts afin de pouvoir accueillir de nouvelles applications tout au long de leur cycle de vie. Ils possèdent alors des contraintes fortes de types qualité de service, sécurité, tolérance aux fautes, etc. La programmation à base de composants apparaît comme une solution prometteuse pour le développement de tels systèmes. Cependant, un des frein à l'adoption de ce type de programmation est que les modèles à composants n'intègrent pas les aspects de gestion de qualité de service. <br />Ce travail de thèse présente une architecture de gestion de qualité de service pour les systèmes embarqués mobiles à composants. Cette architecture, appelée Qinna, est définie à l'aide de composants Fractal et permet la mise en œuvre, ainsi que la gestion dynamique, de contrats de qualité de service entre les différents composants d'un système. L'originalité de l'approche proposée permet de prendre en compte la qualité de service quelque soit le niveau considéré du système (niveau applicatif, niveau services, niveau système d'exploitation et niveau ressources).<br />L'architecture Qinna a été validée par une évaluation qualitative à base de patrons génériques d'architecture, puis par une évaluation quantitative permettant de montrer que le coût de l'architecture reste faible.<br />Le travail réalisé ouvre de nombreuses perspectives de recherche notamment celle de généraliser l'approche utilisée (définition d'une architecture abstraite de composant pour la prise en charge de la gestion d'une propriété non-fonctionnelle, ici la QdS) à d'autres propriétés non-fonctionnelles (par exemple la sécurité ou la tolérance aux fautes), et d'en tirer des conclusions sur la définition et la génération de conteneurs ouverts.

Souvent, dû a l'aspect cyclique des programmes embarqu és, les traces de microcontrôleurs contiennent beaucoup de donn ées. De plus, dans notre contexte de travail, pour l'analyse du comportement, une seule trace se terminant sur une défaillance est disponible. L'objectif du travail pr esent é dans cette th ese est d'aider à l'analyse de trace de microcontrôleurs. La premi ère contribution de cette th èse concerne l'identifi cation de cycles, ainsi que la g én ération d'une description pertinente de la trace. La d étection de cycles repose sur l'identifi cation du loop- header. La description propos ée à l'ing enieur est produite en utilisant la compression bas ée sur la g én ération d'une grammaire. Cette derni ère permet la d etection de r ép étitions dans la trace. La seconde contribution concerne la localisation de faute(s). Elle est bas ée sur l'analogie entre les ex écutions du programme et les cycles. Ainsi, pour aider dans l'analyse de la trace, nous avons adapt é des techniques de localisation de faute(s) bas ée sur l'utilisation de spectres. Nous avons aussi d éfi ni un processus de filtrage permettant de r éduire le nombre de cycles àa utiliser pour la localisation de faute(s). Notre troisi ème contribution concerne l'aide a l'analyse des cas o ù les multiples cycles d'une même ex écution interagissent entre eux. Ainsi, pour faire de la localisation de faute(s) pour ce type de cas, nous nous int eressons à la recherche de r égles d'association. Le groupement des cycles en deux ensembles (cycles suspects et cycles corrects) pour la recherche de r égles d'association, permet de d e finir les comportements jug és correctes et ceux jug és comme suspects. Ainsi, pour la localisation de faute(s), nous proposons à l'ing enieur un diagnostic bas é sur l'analyse des r égles d'association selon leurs degr és de suspicion. Cette th èse pr esente également les évaluations men ées, permettant de mesurer l'efficacit e de chacune des contributions discut ées, et notre outil CoMET. Les r ésultats de ces évaluations montrent l'e fficacit e de notre travail d'aide à l'analyse de traces de microcontrôleurs.

La problématique SLAM (Simultaneous Localization and Mapping) est un thème largement étudié au LAAS depuis plusieurs années. L'application visée concerne le développement d'un système d'aide au roulage sur aéroport des avions de ligne, ce système devant être opérationnel quelques soient les conditions météorologiques et de luminosité (projet SART financé par la DGE en partenariat avec principalement FLIR Systems, Latécoère et Thales). Lors de conditions de visibilité difficile (faible luminosité, brouillard, pluie...), une seule caméra traditionnelle n'est pas suffisante pour assurer la fonction de localisation. Dans un premier temps, on se propose d'étudier l'apport d'une caméra infrarouge thermique. Dans un deuxième temps, on s'intéressera à l'utilisation d'une centrale inertielle et d'un GPS dans l'algorithme de SLAM, la centrale aidant à la prédiction du mouvement, et le GPS à la correction des divergences éventuelles. Enfin, on intègrera dans ce même SLAM des pseudo-observations issues de l'appariement entre des segments extraits des images, et ces mêmes segments contenus dans une cartographie stockée dans une base de données. L'ensemble des observations et pseudo-observations a pour but de localiser le porteur à un mètre près. Les algorithmes devant être portés sur un FPGA muni d'un processeur de faible puissance par rapport aux PC standard (400 MHz), un co-design devra donc être effectué entre les éléments logiques du FPGA réalisant le traitement d'images à la volée et le processeur embarquant le filtre de Kalman étendu (EKF) pour le SLAM, de manière à garantir une application temps-réel à 30 Hz. Ces algorithmes spécialement développés pour le co-design et les systèmes embarqués avioniques seront testés sur la plate-forme robotique du LAAS, puis portés sur différentes cartes de développement (Virtex 5, Raspberry, PandaBoard...) en vue de l'évaluation des performances

Le travail présenté dans cette thèse porte sur la conception de logiciels pour systèmes embarqués. Outre les contraintes de programmation provenant des faibles quantité de mémoire et capacité de calcul, ces plates-formes matérielles ne disposent parfois que de peu d'énergie pour fonctionner. Les applications usuelles de ces systèmes imposent de plus des objectifs en matière de réactivité et de durée de vie. Par ailleurs, quelques-unes des ressources fournies sont partagées entre les composants, qu'il s'agisse de l'énergie délivrée par une batterie, ou encore des bus de communication qui les relient. Il est donc nécessaire de pouvoir assurer des propriétés globales portant sur l'ensemble de la plate-forme, telles que le contrôle des accès aux bus, ou encore la maîtrise de la puissance électrique consommée. Cependant, les pilotes des différents périphériques sont d'ordinaire programmés individuellement. La connaissance nécessaire à l'implantation d'une politique de contrôle global est alors distribuée parmi diverses portions du logiciel. Nous exposons une solution au problème du contrôle global des ressources, basée sur une vue centralisée des états des composants matériels de la plate-forme. Bâtie sur un principe de para-virtualisation, notre approche consiste en l'introduction d'une couche de contrôle ; le système d'exploitation invité est adapté afin de communiquer avec le matériel à l'aide de celle-ci. La couche de contrôle incorpore les pilotes des périphériques, conçus à partir d'automates dont les états correspondent aux modes de fonctionnement ou de consommation du composant géré. Un contrôleur est ajouté, dont le rôle est d'assurer les propriétés globales. L'ensemble de ces automates est programmé à l'aide d'un langage synchrone, puis compilé en code séquentiel. Nous proposons une implantation de la couche de contrôle pour une architecture de nœuds de réseaux de capteurs sans fil, qui constitue une plate-forme représentative des systèmes embarqués contraints. Nous évaluons qualitativement et quantitativement ce prototype afin de montrer la viabilité de l'approche. Son impact sur le reste du logiciel est également apprécié, que celui-ci soit construit selon un modèle d'exécution purement événementiel ou multi-fils. Enfin, nous passons en revue plusieurs extensions possibles, et identifions quelques bonnes pratiques pour son usage dans d'autres contextes.

Cette thèse présente Lion, un système de navigation utilisant des informations visuelles et inertielles pour l'atterrissage planétaire de précision. Lion est conçu pour voler au-dessus de n'importe quel type de terrain, plat ou accidenté, et ne fait pas d'hypothèse sur sa topographie. Faire un atterrir un véhicule d'exploration planétaire autonome à moins de 100 mètres d'un objectif cartographié est un défi pour la navigation. Les approches basées vision tentent d'apparrier des détails 2D détectés dans une image avec des amers 3D cartographiés pour atteindre la précision requise. Lion utilise de façon serrée des mesures venant d'un nouvel algorithme d'appariement imagecarte afin de mettre à jour l'état d'un filtre de Kalman étendu intégrant des données inertielles. Le traitement d'image utilise les prédictions d'état et de covariance du filtre dans le but de déterminer les régions et échelles d'extraction dans l'image où trouver des amers non-ambigus. Le traitement local par amer de l'échelle image permet d'améliorer de façon significative la répétabilité de leur détection entre l'image de descente et l'image orbitale de référence. Nous avons également conçu un banc d'essai matériel appelé Visilab pour évaluer Lion dans des conditions représentatives d'une mission lunaire. L'observabilité des performances de navigation absolue dans Visilab est évaluée à l'aide d'un nouveau modèle d'erreur. Les performances du systèmes sont évaluées aux altitudes clés de la descente, en terme de précision de navigation et robustesse au changement de capteurs ou d'illumination, inclinaison de la caméra de descente, et sur différents types de relief. Lion converge jusqu'à une erreur de 4 mètres de moyenne et 47 mètres de dispersion 3 RMS à 3 kilomètres d'altitude à l'échelle.

L’objectif de ce projet de recherche est de développer une technologie d’agents mobiles pour systèmes embarqués. Dans un premier temps, une plateforme d’agents mobiles pour systèmes embarqués homogènes est réalisée et, ensuite dans un deuxième temps, une application d’informatique diffuse qui exploite la mobilité du contexte d’exécution est mise en œuvre pour valider cette plateforme. La mobilité d’un agent est définie comme suit: son exécution est interrompue sur le nœud courant, appelé nœud source, ensuite les données représentant l’état de l’agent sont transférées du nœud source vers un nœud destination et enfin, arrivé au nœud destination, son exécution se poursuit là où elle avait été interrompue sur le nœud de départ. Cette opération, appelée migration du contexte d’exécution, est intégrée aux fonctionnalités d’un noyau temps réel, permettant ainsi la mobilité d’agents logiciels au sein d’une grappe de systèmes embarqués homogènes. Les applications visées par le projet relèvent du domaine de l’informatique diffuse et plus particulièrement de son application à l’espace intelligent.

Cette thèse expose nos travaux de certification d'une partie d'un programme C/C++ nommé SimSoC (Simulation of System on Chip), qui simule le comportement d'archi- tectures basées sur des processeurs tels que ARM, PowerPC, MIPS ou SH4. Un simulateur de System on Chip peut être utilisé pour developper le logiciel d'un système embarqué spécifique, afin de raccourcir les phases des développement et de test, en particulier quand la vitesse de simulation est réaliste (environ 100 millions d'instructions par seconde par cœur dans le cas de SimSoC). Les réductions de temps et de coût de développement obtenues se traduisent par des cycles de conception interactifs et rapides, en évitant la lourdeur d'un système de développement matériel. SimSoC est un logiciel complexe, comprenant environ 60 000 de C++, intégrant des parties écrites en SystemC et des optimisations non triviales pour atteindre une grande vitesse de simulation. La partie de SimSoC dédiée au processeur ARM, l'un des plus répandus dans le domaine des SoC, transcrit les informations contenues dans un manuel épais de plus de 1000 pages. Les erreurs sont inévitables à ce niveau de complexité, et certaines sont passées au travers des tests intensifs effectués sur la version précédente de SimSoC pour l'ARMv5, qui réussissait tout de même à simuler l'amorçage complet de linux. Un problème critique se pose alors : le simulateur simule-t-il effectivement le matériel réel ? Pour apporter des éléments de réponse positifs à cette question, notre travail vise à prouver la correction d'une partie significative de SimSoC, de sorte à augmenter la confiance de l'utilisateur en ce similateur notamment pour des systèmes critiques. Nous avons concentré nos efforts sur un composant particulièrement sensible de SimSoC : le simulateur du jeu d'instructions de l'ARMv6, faisant partie de la version actuelle de SimSoC. Les approches basées sur une sémantique axiomatique (logique de Hoare par exemple) sont les plus répandues en preuve de programmes impératifs. Cependant, nous avons préféré essayer une approche moins classique mais plus directe, basée sur la sémantique opérationnelle de C : cela était rendu possible en théorie depuis la formalisation en Coq d'une telle sémantique au sein du projet CompCert et mettait à notre disposition toute la puissance de Coq pour gérer la complexitité de la spécification. À notre connaissance, au delà de la certification d'un simulateur, il s'agit de la première expérience de preuve de correction de programmes C à cette échelle basée sur la sémantique opérationnelle. Nous définissons une représentation du jeu d'instruction ARM et de ses modes d'adressage formalisée en Coq, grâce à un générateur automatique prenant en entrée le pseudo-code des instructions issu du manuel de référence ARM. Nous générons égale- ment l'arbre syntaxique abstrait CompCert du code C simulant les mêmes instructions au sein de Simlight, une version allégée de SimSoC. À partir de ces deux représentations Coq, nous pouvons énoncer et démontrer la correction de Simlight, en nous appuyant sur la sémantique opérationnelle définie dans CompCert. Cette méthodologie a été appliquée à au moins une instruction de chaque catégorie du jeu d'instruction de l'ARM. Au passage, nous avons amélioré la technologie disponible en Coq pour effectuer des inversions, une forme de raisonnement utilisée intensivement dans ce type de situation.

L’objet de cette thèse porte sur la modélisation mathématique des générateurs physiques de nombres aléatoires, tout particulièrement dans le contexte des systèmes embarqués. Les axes principaux sont les modèles stochastiques des sources d'entropie, l’établissement de tests statistiques adaptés et l’exploitation des défauts détectés / The purpose of this thesis focuses on the mathematical modeling of physical random number generators, especially in the context of embedded systems. The main axes are the stochastic modeling of entropy sources, the establishment of appropriate statistical tests and the exploitation of detected weaknesses.