Cette thèse aborde le problème de la calibration d’un ensemble de capteurscomposé d’une centrale inertielle, d’un magnétomètre et d’une caméra, avecpour objectif leur intégration sur un système très compact : un mini-drone.Cette étude expose tout d’abord les contraintes imposées par l’application surle choix des capteurs et les solutions envisagées notamment pour résoudre leproblème de la synchronisation des mesures. Après avoir étudié les techniquesde calibration existantes, une méthode permettant la calibration de l’ensembledes capteurs (accéléromètre, gyromètre, magnétomètre et caméra) est présentée.La solution proposée permet également d’estimer les changements de repèresentre les différents capteurs. Elle a la particularité de ne nécessiter l’emploid’aucun matériel particulier. D’autre part, l’intégration de ces capteurs dans unsystème aussi compact soulève de nouvelles difficultés. Dans ces conditions, leschamps magnétiques créés par les actionneurs du drone perturbent les mesuresdu magnétomètre se trouvant à proximité. Une nouvelle méthode est proposéeafin d’estimer et de compenser dynamiquement ces perturbations magnétiquesen fonction de l’état des actionneurs du drone. Enfin, deux applications dusystème comprenant une centrale inertielle et une caméra sont présentées :la construction de mosaïques d’images géo-référencées et la stabilisation devidéos. Ces deux applications exploitent les mesures des capteurs inertiels afind’effectuer un traitement en temps réel pour un coût calculatoire très faible. / This thesis deal with the issue of the calibration of a group of sensor composedof an inertial unit, a magnetometer and a camera. It aims at integratingthem into a very compact system : a mini-drone. First of all, this study outlinesthe constraints imposed by the application on the choice of the sensors andthe solutions considered to solve the measures synchronization issue. Afterstudying existing calibration techniques, a method for the calibration of allthe sensors (accelerometer, gyroscope, magnetometer and camera) is presented.The proposed solution allows to estimate the frame transformation between thedifferent sensors. It has the advantage of not requiring the use of any specialequipment. Furthermore, the integration of these sensors into a compact systemraises new difficulties. Under these conditions, the magnetic fields created bythe drone actuators disrupt magnetometer measurements. A new method isproposed to estimate and compensate for these magnetic disturbances. Thecompensation is dynamically adapted based on the state of the drone actuators.Finally, two applications of the system including an inertial unit and a cameraare presented : the construction of geo-referenced images mosaic and videostabilization. Both applications use measurements of inertial sensors and precisecalibration to perform a real-time processing for a very low computational cost.

Les systèmes embarqués modernes ont atteint un niveau de complexité qui fait qu'il n'est plus possible d'attendre les premiers prototypes physiques pour valider les décisions sur l'intégration des composants matériels et logiciels. Il est donc nécessaire d'utiliser des modèles, tôt dans le flot de conception. Les travaux présentés dans ce document contribuent à l'état de l'art dans plusieurs domaines. Nous présentons dans un premier temps de nouvelles techniques de vérification de programmes écrits dans des langages généralistes comme C, C++ ou Java. Dans un second temps, nous utilisons des outils de vérification formelle sur des modèles écrits en SystemC au niveau transaction (TLM). Plusieurs approches sont présentées, la plupart d'entre elles utilisent des techniques de compilations spécifiques à SystemC pour transformer le programme SystemC en un format utilisable par les outils. La seconde partie du document s'intéresse aux propriétés non-fonctionnelles des modèles~: performances temporelles, consommation électrique et température. Dans le contexte de la modélisation TLM, nous proposons plusieurs techniques pour enrichir des modèles fonctionnels avec des informations non-fonctionnelles. Enfin, nous présentons les contributions faites à l'analyse de performance modulaire (MPA) avec le calcul temps-réel (RTC). Nous proposons plusieurs connections entre ces modèles analytiques et des formalismes plus expressifs comme les automates temporisés et le langage de programmation Lustre. Ces connexion posent le problème théorique de la causalité, qui est formellement défini et résolu avec un algorithme nouveau dit de " fermeture causale ".