Dissertations / Theses on the topic 'Systèmes embarqués (informatique) – Esterel (langage de programmation)'

Esterel est un langage de spécification utilisé dans le développement de systèmes embarqués. Sa sémantique formelle permet des traductions en automates explicites ou en circuits digitaux synchrones, donnant lieu à deux implantations logicielles dont les propriétés essentielles sont héritées du modèle correspondant. Ces méthodes de compilation sont donc sémantiquement complètes, mais en contrepartie n’arrivent pas à générer du code efficace (à la fois compact et rapide) pour des modèles de taille conséquente. Pour cette raison, de nouvelles techniques ont été proposées récemment pour la génération de code C efficace, consistant essentiellement dans la simulation directe des opérations réactives du programme Esterel. Ces nouvelles techniques doivent être conciliées maintenant avec les aspects spécifiques à la sémantique d’Esterel qui sont la causalité constructive et la cyclicité. Elles doivent aussi être munies de techniques adaptées d’analyse et d’optimisation. Pour atteindre ces objectifs, nous proposons une nouvelle technique de compilation dont la puissance découle de l’utilisation d’un nouveau format intermédiaire, nommé GRC. La représentation GRC d’un programme Esterel se compose d’une représentation de l’état hiérarchique du programme et d’un graphe déstructuré de flot de contrôle. Les deux composants, séparés au niveau syntaxique, sont sémantiquement interdépendants. Le nouveau format permet la représentation de tout programme Esterel. Il est un bon support pour des algorithmes d’optimisation efficaces à ce niveau et pour des algorithmes d’implantation (ordonnancement et encodage) efficaces. Notre travail apporte les contributions suivantes : - une définition précise de la sémantique du langage Esterel avec données ; - la définition du format GRC et de la correspondance formelle entre le code GRC et les circuits générés à partir d’Esterel ; - la caractérisation, au niveau du code GRC, de la classe de programmes Esterel générant des circuits cycliques ; - le développement d’un compilateur Esterel-C qui utilise GRC comme unique format intermédiaire. Le prototype traite actuellement les programmes Esterel dont la représentation GRC est acyclique. Le code C est obtenu dans ces cas par une planification statique du graphe de flot de contrôle GRC. Le compilateur implémente un bon nombre de techniques d’optimisation, en partie originales. Une comparaison entre notre prototype et les autres compilateurs montre l’intérêt de l’approche<br>Esterel is a design language for reactive embedded systems. It enjoys a full-fledged formal operational semantics, and can customarily be compiled into either explicit Finite State Machines or Digital Sequential Circuit models, thereby providing implementation codes with very distinctive flavors. While being semantically complete, the model-based techniques do not support the generation of efficient (fast and small) code for large specifications. For this reason, new compilation schemes were proposed for the generation of efficient sequential ( C) code. Consisting essentially in direct actual simulation of the language reactive features, the new approach now needs to be accommodated with similar semantic issues as the previous ones (FSM- and circuit-based). Such issues include dealing with the whole class of constructively causal programs, or performing optimization and analysis of this level. To this end, we propose here a new format/model (named GRC) for the intermediate representation of Esterel programs. The new format has formal constructive semantics, being able to represent all the Esterel programs. It describes with separate (but interdependent) structures the hierarchic state of the Esterel program and its destructured control flow. Thus, it is a good support for both (1) efficient low-cost optimizations based on static analysis that use high-level structural information and (2) low-level control flow optimizations. Finally, the format is a good starting point for efficient scheduling algorithms. Our contribution consists in the following : - The precise definition of the semantics of the full Esterel language ; - The definition of the GRC format (including the formal correspondence between its semantics and the “circuit” semantics) ; - A characterization, at GRC level, of the programs that are translated into cyclic circuits ; - The development of an optimizing GRC-based prototype C code generator. The prototype is currently able to compile the programs whose GRC representation is acyclic. Sequential code is generated in these cases by statically scheduling the acyclic GRC flowgraph. The compiler includes novel optimization algorithms, based on static analysis, and an efficient state encoding technique. The results are encouraging, as our prototype seems to compare well against existing compilers

Ce travail de these vise essentiellement a fournir des methodes et outils pour la conception de systemes temps-reel. Du fait de la forte composante reactive de ces systemes, nous preconisons une approche synchrone. Le domaine du temps-reel etant particulierement vaste, nous nous interessons plus particulierement aux applications de controle ce qui nous a conduit a utiliser le langage esterel. Nous abordons les differentes phases de la modelisation, conception, programmation et realisation en apportant pour chacune d'elles une solution synchrone. Les transitions entre ces phases sont systematiques et sans rupture. Nous proposons de modeliser ces systemes par des boites hierarchiques reactives synchrones (bhrs). Le but d'une bhrs est de fournir une assistance a des non-specialistes des langages, pour la conception synchrone de leurs applications. Ce modele permet une decomposition par niveaux et une description modulaire des systemes. Ce modele est dote d'une semantique comportementale rigoureuse. Le passage du modele vers le langage synchrone esterel s'effectue de maniere systematique par une traduction des comportements des bhrs en esterel. Nous etudions ensuite le probleme de l'implementation effective de programme synchrone. Nous definissons pour cela des environnements d'execution de programmes synchrones qui prennent en compte les caracteristiques temps-reel des systemes. Des specifications de machine d'execution sont fournies. La derniere partie est consacree a la mise en uvre de programmes synchrones sur une architecture cible de type microcontroleur. L'implantation sur ce microcontroleur est realisee de maniere automatique. Lors de cette phase, nous quantifions l'approximation de reactions en temps nul faite par le langage esterel, par une evaluation formelle des performances de l'application. Des supports logiciels sont fournis pour realiser ceci

Les systèmes embarqués sont caractérisés par des ressources matérielles réduites. Bien que ces ressources ne cessent de s’étendre, elles restent tout de même insuffisantes. L’espace mémoire est l’une des ressources les plus critiques. La compression du code dédié aux systèmes embarqués représente une solution intéressante pour réduire l’encombrement mémoire. Notre travail de recherche se focalise sur la compression du code Java sous format de fichiers class Java. Notre contribution consiste à concevoir et mettre en œuvre un système basé sur un profiler pour guider la compression des fichiers class Java. Ce profiler permet d'établir une stratégie de compression efficace offrant le meilleur taux de compression en tenant compte des caractéristiques du code en entrée et des dépendances entre les techniques de compression. La démarche suit quatre points : 1- l'examen du code Java afin d’en extraire les informations utiles pour le guidage du processus de compression. 2 - l'analyse des dépendances des opérations de compression en terme d'interaction mutuelle des unes avec les autres. Pour ce faire, nous avons mis au point deux méthodes, l'une numérique basée sur l'estimation des performances, l'autre analytique permettant de déterminer la nature des dépendances entre les opérations de compression. 3 - l'évaluation statistique des performances permettant le choix de la stratégie de compression. Nous avons, à ce propos, identifié les paramètres relatifs à chaque opération permettant ainsi leur évaluation. 4- La définition d’heuristiques appropriées pour identifier le chemin de compression le plus efficace dans l'espace de recherche représenté par un graphe orienté<br>The embedded systems are characterized by reduced hardware resources. Although these resources are constantly increasing, they remain insufficient. The memory space is one of the most critical resources. The compression of the code designed for embedded systems constitutes an interesting solution to reduce the memory footprint. Our study focuses on the compression of Java code represented by Java Class format files. Our contribution consists in designing and implementing a profiler based system in order to guide the compression of Java class files. Our profiler enables us to set up, on the basis of elementary compression techniques, an efficient compression strategy which delivers the best rate of compression. This strategy takes into consideration the features of the code given in input and dependencies between compression techniques. Our approach is based on four points: 1 - the study of the input files in order to extract the necessary information for the guidance of the compression process. 2 - the analysis of compression techniques dependencies in terms of effects produced by each technique to the others. To do so, we developed two methods: one numerical, based on the estimation of performance, the other analytical in order to determine whether there are common points between the different compression methods. 3 - the statistic performance assessment which allows to choose a strategy of compression: we have identified the parameters, related to each method, that enable this assessment. 4 - the definition of heuristics in order to identify the most efficient compression path in a research space characterized by an oriented graph

Ce travail porte sur la programmation de systèmes de Contrôle-Commande. Ces systèrnes sont constitués d’une boucle de controle qui acquiert l’état actuel du système par l'intermédiaire de capteurs, exécute des algorithmes de contrôle à partir de ces données et calcule en réaction les commandes à appliquer sur les actionneurs du système dans le but de réguler son état et d'accomplir une mission donnée. Les logiciels de commandes de vol d’un aéronef sont des exemples typiques de systèmes de Contrôle-Commande ayant pour objectif de contrôler la position, la vitesse et l’attitude de l'aéronef durant le vol. Les systèmes considérés sont critiques, dans le sens où leur mauvais fonctionnement peut avoir des conséquences catastrophiques. Leur implantation doit donc être déterministe, non seulement sur le plan fonctionnel (produire les bonnes sorties en réponse aux entrées) mais aussi sur le plan temporel (produire les données aux bonnes dates). Nous avons défini un langage formel et son compilateur permettant de programmer de tels systemes. Le langage se situe à un niveau d’abstractron élevé et se présente comme un langage d'architecture logicielle temps réel. Il permet de spécifier avec une sémantique synchrone l'assemblage des composants fonctionnels d’un système multi-rythme. Un programme consiste en un ensemble d'opérations importées, implantées à l'extérieur du programme, reliées par des dépendances de données. Le langage permet de spécifier de multiples contraintes de périodicité ou d’échéance sur les opérations. Il définit de plus un ensemble réduit d’opérateurs de transition de rythme permettant de décrire de manière précise et non ambiguë des schémas de communication entre opérations de périodes différentes. La sémantique du langage est définie formellement et la correction d'un programme, c'est à dire l'assurance que sa sémantique est bien définie, est vérifiée par un ensemble d'analyses statiques. Un programme correct est compilé en un ensemble de tâches temps réel implantées sous forme de threads C communicants. Le code d’un thread est constitué du code (externe) de l'opération correspondante, complété par un protocole de communication gérant les échanges de données avec les autres threads. Le protocole, basé sur des mécanismes de copies dans des mémoires tampons, est non bloquant et déterministe. Le code généré s’exécute à l'aide d’un Systeme d’Exploitation Temps Réel classique disposant de la politique d'ordonnancement EDF. Les opérations du programme s’exécutent de manière concurrente et peuvent donc être préemptées en cours d’éxecution en faveur d’une opération plus urgente. Le protocole de communication proposé permet d’assurer que, malgré les préemptions, l'exécution du programme généré est prédictible et correspond exactement à la sémantique formelle du programme d'origine.

Les contrats basés sur les notions d'hypothèses/garanties constituent un paradigme expressif pour une conception modulaire et compositionnelle de spécification de programmes. Dans cette thèse, nous élaborons des fondements pour la mise en oeuvre de systèmes embarqués basée sur la notion de contrats. Nous proposons ainsi une algèbre de contrats basée sur deux concepts simples : les hypothèses et les garanties des composants sont définies par des filtres, les filtres sont caractérisés par une structure d'algèbre booléenne. Les choix effectués pour définir la structure des filtres permettent de définir une algèbre de Heyting sur l'ensemble des contrats. Un cadre de travail est ainsi défini, dans lequel les contrats sont utilisés pour vérifier la correction des hypothèses faites sur le contexte d'utilisation d'un composant, et pour fournir à l'environnement les garanties qui lui sont demandées. Nous illustrons cette présentation avec la spécification d'un moteur à quatre temps<br>Contract-based design is an expressive paradigm for a modular and compositional specification of programs. In this thesis, we elaborate new foundations for contract-based embedded system design by proposing a general-purpose algebra of assume/guarantee contracts based on two simple concepts: first, the assumption or guarantee of a component is defined as a filter and, second, filters enjoy the structure of a Boolean algebra. This yields a structure of contracts that is a Heyting algebra. In this framework, contracts are used to negotiate the correctness of assumptions made on the definition of a component at the point where it is used and provides guarantees to its environment. We put this algebra to work for the definition of a general purpose module system whose typing paradigm is based on the notion of contract. We illustrate this presentation with the specification of a simplified 4-stroke engine model

La méthodologie présentée distingue dans le logiciel temps-réel une partie commande et une partie opérative. Elle se base sur l'utilisation des réseaux de Petri pour spécifier la partie commande et sur un environnement de programmation pour générer quasi automatiquement le logiciel final

La problématique abordée dans ce travail est celle de la gestion mémoire automatique pour des programmes Java temps-réel embarqués. Dans des langages comme le C ou le C++, la mémoire est typiquement gérée explicitement par le programmeur, ce qui est la source de nombreuses erreurs d'exécution causées par des manipulations hasardeuses. Le coût de correction de telles erreurs est très important car ces erreurs sont rarement reproductibles et donc difficiles à appréhender. En Java la gestion mémoire est entièrement automatique, ce qui facilite considérablement le développement. Cependant, les techniques classiques de recyclage de la mémoire, typiquement basées sur l'utilisation d'un ramasse-miettes, sont souvent considérées comme inapplicables dans le contexte des applications temps-réel embarquées, car il est très difficile de prédire leur temps de réponse. Cette incompatibilité est un frein important à l'adoption de langages de haut niveau comme Java dans ce domaine.<br />Pour résoudre le problème de la prévisibilité du temps d'exécution des opérations mémoire, nous proposons une approche fondée sur l'utilisation d'un modèle mémoire en régions. Cette technique, en groupant physiquement les objets de durées de vie similaires dans des zones gérées d'un seul bloc, offre en effet un comportement temporel prévisible. Afin de décider du placement des objets dans les différentes régions, nous proposons un algorithme d'analyse statique qui calcule une approximation des relations de connexion entre les objets. Chaque structure de données est ainsi placée dans une région distincte. L'analyse renvoie également au programmeur des informations sur le comportement mémoire du programme, de façon à le guider vers un style de programmation propice à la gestion mémoire en régions, tout en pesant le moins possible sur le développement. <br />Nous avons implanté un gestionnaire mémoire automatique en régions dans la machine virtuelle JITS destinée aux systèmes embarqués à faibles ressources. Les résultats expérimentaux ont montré que notre approche permet dans la plupart des cas de recycler la mémoire de façon satisfaisante, tout en présentant un comportement temporel prévisible. Le cas échéant, l'analyse statique indique au développeur quels sont les points problématiques dans le code, afin de l'aider à améliorer son programme.

Face à la multiplication et la diversification des services informatisés proposés aux individus, la personnalisation devient un élément majeur de différentiation pour les fournisseurs. Grâce à ses propriétés de sécurité et de mobilité, la carte à puce dispose du potentiel nécessaire pour jouer un rôle clef dans le déploiement de services personnalisés nomades. Les plates-formes logicielles des cartes. à puce de prochaine génération offrent des possibilités accrues en terme de programmation et d'intégration au sein des infrastructures informatiques. Cette évolution des applications encartées nécessite à la fois un enrichissement et une modernisation du processus industriel de personnalisation. Les travaux décrits dans cette thèse constituent une proposition d'approche novatrice, fournissant aux développeurs les moyens méthodologiques et techniques de réaliser une personnalisation fonctionnelle à grande échelle de leurs applications. Dans la perspective d'optimiser le processus industriel de personnalisation, les concepts de code personnalisable et de code personnalisé sont introduits : le second résulte du tissage entre le premier et un ensemble de données utilisateurs structurées dans des profils. Le code des applications encartées personnalisées est produit de manière semi automatisée sur la base d'une démarche exploitant la complémentarité entre les techniques de modélisation et le développement logiciel génératif. Un ensemble de méta-modèles structurés de manière à respecter la séparation des préoccupations permet d'exprimer les besoins de personnalisation, tandis qu'un cadre de conception permet d'implémenter les transformations et les tissages de modèles en Java.

Les systèmes embarqués sont largement utilisés de nos jours. Pour des raisons d'efficacité, les plus contraints en termes de ressources sont toujours programmés en C et en assembleur. L'adoption de langages de plus haut niveau tels que C# ou Java offrirait plus d'abstraction au programmeur, ce qui réduirait les temps de développement et par conséquent le coût de ces systèmes. Certains d'entre eux ont déjà migré vers de tels langages, comme les téléphones mobiles ou les tablettes tactiles, mais ils sont équipés d'une grande quantité de mémoire externe et ne reflètent pas la majorité des systèmes embarqués.Cette thèse s'intéresse à l'implémentation de Java et .NET pour l'embarqué, et plus spécifiquement à la compilation efficace du polymorphisme. Ce polymorphisme génère un certain coût à l'exécution, comme des indirections dans le cas des appels de méthodes (polymorphisme d'inclusion), ou de la duplication de code dans le cas de la généricité (polymorphisme paramétrique). De nombreuses techniques d'implémentation ont été proposées, notamment pour Java. Il reste cependant à identifier lesquelles sont applicables pour le type de systèmes que nous ciblons, et à en concevoir de nouvelles pour certains aspects comme la généricité. Nous partons du principe que les techniques globales (hypothèse du monde clos) sont les mieux adaptées. Par l'analyse de types, nous détectons qu'une partie importante des programmes est monomorphe et qu'elle peut donc être compilée sans surcoût. Pour implémenter le polymorphisme restant, nous choisissons la technique la mieux adaptée au matériel cible. Nous proposons également une implémentation de la généricité qui est adaptée aux systèmes embarqués. D'après nos évaluations, l'impact négatif du polymorphisme sur l'efficacité est largement réduit. L'efficacité du code optimisé devrait s'approcher de celle du C, et les techniques que nous employons pourraient être applicables dans le contexte plus général du chargement dynamique<br>Nowadays, embedded systems are ubiquitous. For efficiency reasons, most constrained systems are still programmed in C and assembly. Adopting higher-level languages such as C# or Java should enhance the level of abstraction offered to programmers and reduce development time and cost for these systems. A small part of them have migrated to such languages, like smartphones and tablet computers, but they have a large amount of external memory available and do not represent the majority of embedded systems.This thesis focuses on the implementation of Java and .NET for embedded systems, and more especially on the efficient compilation of polymorphism. Polymorphism generates an overhead at run-time, such as indirections when methods are invoked (inclusion polymorphism) or code duplication in the case of generics (parametric polymorphism). Many implementation techniques have been proposed, especially for Java. However, it remains to identify which ones are applicable in the context of low-end embedded systems. We consider that whole program optimization (closed-world assumption) is well-suited in this context. Using type analysis, we observe that most part of programs is monomorph, therefore it can be compiled with no overhead with respect to C. In order to implement the remaining polymorphism, we choose the technique which is better suited for the target hardware. We also propose an appropriate implementation of run-time generics. Our results show that the negative impact of polymorphism is mostly reduced. The efficiency of the optimized code should be comparable with C, and the techniques we employ could be applicable in the context of dynamic loading (open-world assumption)

Nous nous intéressons dans ce manuscrit au langage ReactiveML, qui est une extension de ML avec des constructions inspirées des langages synchrones. L'idée de ces langages est de diviser l'exécution d'un programme en une suite d'instants logiques discrets. Cela permet de proposer un modèle de concurrence déterministe que l'on peut compiler vers du code séquentiel impératif. La principale application de ReactiveML est la simulation discrète, par exemple de réseaux de capteurs. Nous cherchons ici à programmer des simulations à grande échelle, ce qui pose deux questions : sait-on les programmer de façon simple et modulaire ? sait-on ensuite exécuter ces programmes efficacement ? Nous répondons à la première question en proposant une extension du modèle synchrone appelée domaines réactifs. Elle permet de créer des instants locaux invisibles de l'extérieur. Cela rend possible le raffinement temporel, c'est-à-dire le remplacement d'une approximation d'un système par une version plus détaillée sans changer son comportement externe. Nous développons dans ce manuscrit la sémantique formelle de cette construction ainsi que plusieurs analyses statiques, sous forme de systèmes de types-et-effets, garantissant la sûreté des programmes dans le langage étendu. Enfin, nous montrons également plusieurs implémentations parallèles du langage pour tenter de répondre à la question du passage à l'échelle des simulations. Nous décrivons tout d'abord une implémentation avec threads communiquant par mémoire partagée et basée sur le vol de tâches, puis une seconde implémentation utilisant des processus lourds communiquant par envoi de messages.

Développer des analyseurs statiques nécessite une manipulation intensive de structures d'arbres et de graphes représentant le programme. La finalité de cette thèse est de proposer des constructions de langage dédiées au prototypage d'outils d'analyse et de transformation de programmes et inspirées de la réécriture de termes et de termes-graphes. L'originalité de notre approche est d'embarquer ces nouvelles constructions dans les langages généralistes sous la forme d'un langage dédié embarqué. Les travaux de cette thèse se fondent sur le langage Tom qui propose d'embarquer des constructions de réécriture dans des langages généralistes comme Java. La première contribution de cette thèse a été de formaliser les langages embarqués sous le concept de langage îlot. Ce formalisme a ainsi permis de certifier la compilation du langage Tom. Nos travaux sur l'analyse de Bytecode nous ont ensuite conduit à réfléchir à la représentation et la manipulation de graphes de flot de programmes et nous avons alors proposé des constructions de langage inspirées de la réécriture de termes-graphes. Une autre contribution de cette thèse est la conception d'un langage de stratégies adapté à l'expression de propriétés sur un programme. Associé au filtrage, ce langage permet d'exprimer de manière déclarative des analyses et des transformations sur des arbres ou des graphes. Enfin, l'ensemble des propositions de cette thèse a été intégré au langage Tom sous la forme de nouvelles constructions syntaxiques ou d'améliorations de constructions existantes et a ainsi pu être appliqué à l'analyse du langage Java.

Aujourd'hui, nous observons une croissance constante de la complexité des systèmes temps-réel. Les développeurs doivent faire face aux contraintes imposées par le domaine dans pratiquement toutes les classes de logiciels. Pour faire face à ce défi, les spécifications Java pour le temps-réel (RTSJ) ont été proposées. Cependant, ces spécifications introduisent de nombreuses règles et restrictions non-intuitives résultant en un modèle de programmation hautement sujet aux erreurs. La vision qui sous-tend cette thèse tient à réduire l'écart entre la programmation temps-réel et les technologies innovantes issues de l'ingénierie logicielle. Une première contribution de cette thèse consiste en l'introduction de "composants de domaine" permettant de manière unifiée l'expression et la manipulation de préoccupations spécifiques à un domaine tout le long du cycle de vie du logiciel.En second lieu, nous proposons SOLEIL, un canevas de conception orienté composants pour le développement de systèmes RTSJ. Ce canevas introduit un cadre méthodologique allégeant la complexité introduite par le modèle de programmation de RTSJ. Enfin, les concepts capturés par les composants de domaine ainsi que les règles et restrictions inhérentes à RTSJ sont formalisées à l'aide du langage Alloy, permettant de vérifier la compatibilité des logiciels développés avec notre approche avec les spécification RTSJ<br>Over the last decade we witness a steady grow of complexities in real-time systems. Today, developers have to face real-time constraints in almost every software system, from embedded software to financial systems, internet services, and computer entertainment industry. To address this widespread challenge, the Real-Time Specification for Java (RTSJ) has been proposed. However, RTSJ itself introduces many nonintuitive rules and restrictions that doom its programming model to be highly error-prone. Moreover, in contrast to the approaches for mainstream software development, the engineering technologies, tools, and frameworks for real-time systems are nowhere near as groundbreaking. The vision behind this dissertation is to ultimately close the gap between real-time programming and today's software technology. Therefore, this dissertation investigates scalable software engineering techniques for RTSJ programming. As the main contribution of this thesis, we introduce Domain Components - an approach to unified expression and manipulation of domain-specific concerns along the software development lifecycle. To validate the approach, we conduct several case studies challenging our proposal from different perspectives. First, performed benchmarks show that the overhead of the Soleil framework is minimal in comparison to manually written object-oriented applications while providing more extensive functionality. Second, considering the state-of-the-art RTSJ programming methods, we achieve better separation of functional and RTSJ concerns, thus increasing efficiency of the development process

Dans cette thèse nous nous intéressons à la problématique de l'ordonnancement temps réel à priorité fixe des systèmes embarqués récupérant leur énergie de l'environnement. Ces derniers collectent l'énergie ambiante de l'environnement et la stockent dans un réservoir d'énergie afin d'alimenter un appareil électronique. Cette technologie est utilisée dans les petits systèmes embarqués qui nécessitent une longue autonomie. Les réseaux de capteurs et les implants médicaux sont des applications typiques de cette technologie. La majorité des systèmes qui opèrent avec cette technologie doivent exécuter des tâches récurrentes dans un temps imparti. Ainsi, ces systèmes sont soumis à des contraintes dites temps réel où le respect des contraintes temporelles est aussi important que l'exactitude des résultats. Cette thèse traite l'ordonnancement préemptif à priorité fixe de ce genre de systèmes sur des plateformes monoprocesseur. La problématique ici est de trouver des algorithmes d'ordonnancement performants ainsi que des conditions d'ordonnançabilité qui vérifient l'ordonnançabilité d'un système donné dans une configuration d'énergie donnée. La première contribution de cette thèse est la proposition de l'algorithme PFPasap. Il s'agit d'une adaptation de l'ordonnancement préemptif classique à priorité fixe aux contraintes énergétiques. Cela consiste à exécuter les tâches dès que l'énergie est suffisante pour exécuter au moins une unité de temps et à seulement recharger dans le cas échéant. Les périodes de rechargement sont aussi longues que nécessaire pour pouvoir exécuter une seule unité de temps. On prouve que PFPasap est optimal mais uniquement dans le cas des systèmes dits non-concrets où la date de la première activation des tâches et le niveau initial du réservoir d'énergie ne sont connus qu'au moment de l'exécution, et quand toutes les tâches consomment plus d'énergie pendant leur exécution que le système n'en collecte. Une condition d'ordonnançabilité nécessaire et suffisante pour ce type de systèmes est également proposée. Malheureusement, si l'on relâche l'hypothèse sur le profil de consommation d'énergie des tâches, en considérant des tâches qui consomment plus que le rechargement et d'autres qui consomment moins, l'algorithme PFPasap n'est plus optimal et l'activation synchrone n'est plus le pire scénario ce qui rend la condition d'ordonnançabilité précédemment citée seulement nécessaire. Pour cela, nous proposons de borner le pire temps de réponse des tâches afin de construire des conditions suffisantes. Concernant l'optimalité, nous explorons différentes idées dans le but de construire un algorithme optimal en considérant tous les types de systèmes de tâches et tous les profils de consommation d'énergie. Nous montrons aussi que la plupart des idées intuitives n'aboutissant pas à des algorithmes optimaux. Dans le but de mieux comprendre notre problématique, nous proposons d'explorer les solutions proposées pour des problématiques similaires, en particulier celles où le retardement des exécutions est parfois nécessaire pour respecter certaines contraintes. L'ordonnancement avec contraintes thermiques est l'une de ces problématiques. Cette dernière consiste à exécuter les tâches de tel sorte qu'une certaine température maximale n'est jamais atteinte. Cela passe par la suspension des exécutions de temps en temps pour rajouter des temps de refroidissement afin d'éviter que la température maximale ne soit atteinte. Comme première étape, nous proposons d'adapter les solutions proposées pour les systèmes à énergie renouvelable aux systèmes à contraintes thermiques. Ainsi, nous adaptons l'algorithme PFPasap afin que la contrainte thermique soit respectée. Nous proposons également une analyse d'ordonnançabilité basée sur des bornes du pire temps de réponse des tâches. Pour terminer, nous présentons YARTISS : l'outil de simulation développé pendant cette thèse pour évaluer les résultats théoriques<br>In this thesis, we are interested in the real-time fixed-priority scheduling problem of energy-harvesting systems. An energy-harvesting system is a system that can collect the energy from the environment in order to store it in a storage device and then to use it to supply an electronic device. This technology is used in small embedded systems that are required to run autonomously for a very long lifespan. Wireless sensor networks and medical implants are typical applications of this technology. Moreover, most of these devices have to execute many recurrent tasks within a limited time. Thus, these devices are subject to real-time constraints where the correctness of the system depends not only on the correctness of the results but also on the time in which they are delivered. This thesis focuses on the preemptive fixed-task-priority real-time scheduling for such systems in monoprocessor platforms. The problematic here is to find efficient scheduling algorithms and schedulability conditions that check the schedulability of a given task set in a given energy configuration. The first result of this thesis is the proposition of the PFPasap scheduling algorithm. It is an adaptation of the classical fixed-task-priority scheduling to the energy-harvesting context. It consists of executing tasks as soon as possible whenever the energy is sufficient to execute at least one time unit and replenishes otherwise. The replenishment periods are as long as needed to execute one time unit. We prove that PFPasap is optimal but only in the case of non-concrete systems where the first release time of tasks and the initial energy storage unit level are known only at run-time and where all the tasks consume more energy than the replenishment during execution times. A sufficient and necessary schedulability condition for such systems is also proposed. Unfortunately, when we relax the assumption of tasks energy consumption profile, by considering both tasks that consume more energy than the replenishment and the ones that consume less than the replenishment, PFPasap is no longer optimal and the worst-case scenario is no longer the synchronous release of all the tasks, which makes the precedent schedulability test only necessary. To cope with this limitation, we propose to upper bound tasks worst-case response time in order to build sufficient schedulability conditions instead of exact ones. Regarding algorithms optimality, we explore different ideas in order to build an optimal algorithm for the general model of fixed-task-priority tasks by considering all types of task sets and energy consumption profiles. We show through some counter examples the difficulty of finding such an algorithm and we show that most of intuitive scheduling algorithms are not optimal. After that, we discuss the possibility of finding such an algorithm. In order to better understand the scheduling problematic of fixed-priority scheduling for energy-harvesting systems, we also try to explore the solutions of similar scheduling problematics, especially the ones that delay executions in order to guarantee some requirements. The thermal-aware scheduling is one of these problematics. It consists of executing tasks such that a maximum temperature is never exceeded. This may lead to introduce additional idle times to cool down the system in order to prevent reaching the maximum temperature. As a first step, we propose in this thesis to adapt the solutions proposed for energy-harvesting systems to the thermal-aware model. Thus, we adapt the PFPasap algorithm to respect the thermal constraints and we propose a sufficient schedulability analysis based on worst-case response time upper bounds. Finally, we present YARTISS: the simulation tool used to evaluate the theoretical results presented in this dissertation

Les systèmes multi-tâches temps-réels deviennent de plus en plus répandus de nos jours. La correction des systèmes multi-tâches est difficile à assurer, pourtant, la correction est critique pour les logiciels temps-réels. La vérification formelle aide à trouver les erreurs potentielles. Les conflits de partage de ressources qui peuvent produire une incohérence des données sont une sorte d'erreurs. Une solution est le verrouillage exclusif des ressources partagées qui peut mener à des temps d'exécution difficile à prédire, ou à l'interblocage dans le pire cas. La vérification des programmes est souvent effectuée par model checking. Un formalisme répandu de model checking des programmes temps-réels sont les automates temporisés. Ils permettent de vérifier certaines propriétés temporelles dans le modèle du programme et de trouver la séquence d'actions qui mènent à l'erreur. Il existe des algorithmes de vérification effectives pour des automates temporisés qui sont réalisés dans des outils de model checking largement utilisés. Nous avons développé un outil pour l'analyse statique de programmes Java multi-tâches qui trouve des conflits de partage de ressources possibles. Les programmes Java sont annotés avec des informations temporelles, et le modèle du programme est construit, en se basant sur les annotations. Le modèle est un système d'automates temporisés qui est vérifié par le model checker Uppaal. Des conflits de partage de ressources possibles sont trouvés par la vérification. Nous avons développé une étude de cas pour illustrer cette approche. L'analyse est complète: lorsqu'un conflit de partage de ressources peut apparaître dans un programme Java, il est détecté par notre analyse. Le modèle abstrait peut aussi sortir des alertes "faux positifs" qui ne correspondent pas à une configuration accessible dans le programme Java original. Pour s'assurer que la traduction des programmes Java vers des automates temporisés est correcte, nous avons formalisé la traduction dans l'assistant de preuves Isabelle. Nous avons prouvé que la traduction préserve la correspondance entre le programme et son modèle. Pour cela, nous avons développé une sémantique formelle de Java multi-tâche avec des annotations et des automates temporisés. Les preuves montrent que le modèle simule le comportement du programme Java original. Cela veut dire que chaque pas de la sémantique du code Java a une séquence de pas correspondante dans le modèle qui a le même effet sur l'état, c. à. D. Des valeurs des variables, temps ou objets verrouillés. Le code vérifié de traduction est généré à partir de la traduction formalisée en utilisant le générateur de code d'Isabelle. Puis notre outil utilise le code vérifié pour générer le modèle d'un programme Java<br>Multithreaded real-time systems become widespread nowadays. Correctness is critical for real-time applications but it is difficult to ensure by usual methods like testing. Formal verification helps to find possible errors. One kind of errors are resource sharing conflicts which lead to data corruption. A common solution is exclusive locking which can lead to unpredictable delays in execution or even deadlocks in the worst case. Program verification is often done by model checking. A popular model checking formalism for real-time programs are timed automata. It allows to verify certain timing properties in a model of a program and to find a sequence of actions which lead to an error. There exist effective verification algorithms for timed automata which are implemented in widely used model checking tools. We have developed a tool for static analysis of multithreaded Java programs which finds possible resource sharing conflicts. Java programs are annotated with timing information, and a model of the program is built based on the annotations. The model is a system of timed automata which is verified by the Uppaal model checker, and possible resource sharing conflicts are found. A case study has been developed to illustrate the approach. The analysis is complete: whenever a resource sharing conflict occurs in a Java program, it is detected by the our analysis. The abstract model may also output "false positive" warnings which do not correspond to a reachable configuration in the source Java program. In order to make sure that the abstraction of Java programs to timed automata is correct, we have formalized the translation is the Isabelle proof assistant. We have proved that the translation preserve correspondence between a program and its model. For this, we have developed a formal semantics both of multithreaded Java with annotations and of timed automata. The proofs show that the model simulates the behavior of the source Java program. This means that each semantic step made in the Java code has a corresponding sequence of steps in the model which has the same effect on the state, i. E. Variable values, time or locked objects. The verified code for translation is generated from the formalized translation using the Isabelle code generator. Then our tool uses the verified code to generate a model of a Java program

The ever-increasing functional and nonfunctional requirements in real-time safety-critical embedded systems call for new design flows that solve the specification, validation, and synthesis problems. Ensuring key properties, such as functional determinism and temporal predictability, has been the main objective of many embedded system design models. Dataflow models of computation (such as KPN, SDF, CSDF, etc.) are widely used to model stream-based embedded systems due to their inherent functional determinism. Since the introduction of the (C)SDF model, a considerable effort has been made to solve the static-periodic scheduling problem. Ensuring boundedness and liveness is the essence of the proposed algorithms in addition to optimizing some nonfunctional performance metrics (e.g. buffer minimization, throughput maximization, etc.). However, nowadays real-time embedded systems are so complex that real-time operating systems are used to manage hardware resources and host real-time tasks. Most of real-time operating systems rely on priority-driven scheduling algorithms (e.g. RM, EDF, etc.) instead of static schedules which are inflexible and difficult to maintain. This thesis addresses the real-time scheduling problem of dataflow graph specifications; i.e. transformation of the dataflow specification to a set of independent real-time tasks w.r.t. a given priority-driven scheduling policy such that the following properties are satisfied: (1) channels are bounded and overflow/underflow-free; (2) the task set is schedulable on a given uniprocessor (or multiprocessor) architecture. This problem requires the synthesis of scheduling parameters (e.g. periods, priorities, processor allocation, etc.) and channel capacities. Furthermore, the thesis considers two performance optimization problems: buffer minimization and throughput maximization.

Dans cette thèse, nous proposons un algorithme pour la localisation d’une flotte de UAVs autonomes dans le cadre de l’architecture des Systèmes-de-Systèmes. En particulier, notre objectif est que les UAVs autonomes puissent se localiser et générer une carte d’un environnement inconnu en utilisant le moins possible de capteurs embarqués sur chaque UAV : une caméra monoculaire dirigée vers l’avant et une centrale inertielle. Cette problématique est cruciale pour des applications telles que l’exploration de zones inconnues ou de missions de sauvetage et de reconnaissance. Les choix de conception algorithmique sont motivés par une étude de l’état de l’art dans les domaines des systèmes multi-robots réalisant de la localisation, de la cartographie, de la navigation et/ou de l’exploration, ainsi que des approches de SLAM visuel, monoculaire, temps réel et monoculaire-inertiel. Le traitement des mesures en vision monoculaire, par nature, n’est pas capable d’estimer des distances métriques à cause de la perte d’information sur la profondeur lors de la projection de l’environnement sur le plan image. Bien que cela ne représente pas un problème majeur pour la plupart des systèmes simple-robot, l’obtention de distances métriques est nécessaire pour permettre la collaboration inter-robots. De plus, lorsque les problématiques de contrôle, de navigation et d’exploration sont ajoutées au problème initial, les distances métriques deviennent d’autant plus importantes. Dans cette thèse, nous proposons une nouvelle approche pour estimer des distances métriques pour un système mobile embarquant seulement une caméra monoculaire et une centrale inertielle via une fusion lâche des mesures.Ce travail de recherche explore également la conception d’un système de localisation pour une flotte de UAVs soumise à des hypothèses minimales : pas de connaissance a priori sur les poses initiales et terminales, pas de connaissance sur l’environnement et pas de mesures absolues ou extérieures aux robots. De plus, notre système est capable de gérer des trajectoires agressives, des changements de vitesse et de cap abrupts ainsi que des mesures bruitées telles que des images floues. Dans les systèmes multi-robots, la gestion des repères est critique et nécessite une attention particulière. La plupart des travaux simplifie ce problème dans un premier temps, en représentant l’ensemble des repères par rapport à un repère « monde » arbitraire. Toutefois, ce genre d’hypothèse nécessite soit des mesures de capteurs que nous n’utilisons pas dans notre système car externes aux robots, soit une connaissance a priori sur l’environnement ou les conditions expérimentales que nous n’avons pas. Dans notre système, chaque robot évolue dans son propre repère, l’ensemble des relations entre les repères nécessaires à la collaboration inter-robots est estimé par notre algorithme. De ce fait, nous pouvons nous abstraire de système de positionnement absolu tel que le GPS. Dans ce but, nous proposons une généralisation du concept de fermeture de boucle bien connu dans le SLAM traditionnel (simple-robot) aux systèmes de SLAM multi-robots. Dans le cadre de cette généralisation, nous mettons en exergue les nouveaux phénomènes induits et leurs conséquences. Cela est démontré expérimentalement, et mis en correspondance avec un système simple-robot. De plus, nous présentons les résultats expérimentaux obtenus dans la recherche de l’amélioration de la localisation en intégrant les nouvelles contraintes de fermeture de boucle<br>In this thesis, we provide a scheme for localization of a fleet of autonomous UAVs (unmanned autonomous vehicles) within a Technological System-of-Systems architecture. Specifically, we aim for a fleet of autonomous UAVs to localize themselves and to obtain a map of an unknown environment using a minimal set of sensors on each UAV: A front monocular camera and an Inertial Measurement Unit. This is a critically important problem for applications such as exploration of unknown areas, or search and rescue missions. The choices for designing such a system are supported by an extensive study of the scientific literature on two broad fronts: First, about the multi-robot systems performing localization, mapping, navigation and exploration, and second, about the monocular, real-time and inertial-monocular SLAM (Simultaneous Localization and Mapping) algorithms. Processing monocular camera frames suffers the drawback of lacking the capability of providing metric estimates as the depth dimension is lost when the frames are photographed by the camera. Although, it is usually not a critical problem for single-robot systems, having accurate metric estimates is required for multi-robot systems. This requirement becomes critical if the system is designed for control, navigation and exploration purposes. In this thesis, we provide a novel approach to make the outputs of monocular SLAM algorithms metric through a loosely-coupled fusion scheme by using the inertial measurements. This work also explores a design for a fleet of UAVs to localize each robot with minimal requirements: No a priori knowledge about the environment, information about neither the position nor the moment in time the UAV takes off and land is required. Moreover, the system presented in the thesis handles aggressive UAV trajectories having dramatic changes in speed and altitude. In multi-robot systems, the question of the coordinate frames require more attention than in single robot systems. In many studies, the coordinate frame problem is simplified to the representation of the fleet and the expression of the measurements in a global coordinate frame. However, this kind of hypothesis implies either the use of additional sensors to be able to measure the transformations to the global coordinate frame or additional experimental constraints, for example about the starting position of the robots. Our system does not require absolute measurements like GNSS positioning or knowledge about the coordinate frame of each UAV. As each UAV of the fleet estimates its location and produces a map in its own coordinate frame, relations between those coordinate frames are found by our scheme. For that purpose, we extend the well known concept of loop-closures in single-robot SLAM approaches, to multi-robot systems. In this research work, we also provide an overview of the new effects due to the extended definition of loop-closures we provide in comparison with the loop-closures scheme that can be found in single robot SLAM algorithms. In addition to the coordinate frame problem, we provide experimental results about the possibilities for improving the location estimate of a fleet by considering the places visited by several UAVs. By searching for similar places using each UAV imagery, using the 2-D information encapsulated in the images of the same sceneryfrom different view points, and the 3-D map locally estimated by each UAV, we add new constraints to the SLAM problem that is the main scheme that can be used to improve the UAV location estimates. We included experiments to assess the accuracy of the inter-UAV location estimation. The system was tested using datasets with measurements recorded on board UAVs in similar conditions as the ones we target

Dans cette thèse nous étudions l'isolation mémoire et les mesures de communications efficaces par passage de message dans le contexte des environnements à mémoire partagée et la programmation orientée-objets. L'état de l'art en la matière se base presque exclusivement sur deux techniques complémentaires dites de propriété des objets (ownership) et d'unicité de références (reference uniqueness) afin d'adresser les problèmes de sécurité dans les programmes concurrents. Il est frappant de constater que la grande majorité des travaux existants emploient des méthodes de vérification statique des programmes, qui requirent soit un effort d'annotations soit l'introduction de fortes contraintes sur la forme et les références vers messages échangés. Notre contribution avec SIAAM est la démonstration d'une solution d'isolation réalisée uniquement à l'exécution et basée sur le modèle de programmation par acteurs. Cette solution purement dynamique ne nécessite ni annotations ni vérification statique des programmes. SIAAM permet la communication sans copie de messages de forme arbitraire. Nous présentons la sémantique formelle de SIAAM ainsi qu'une preuve d'isolation vérifiée avec l'assistant COQ. L'implantation du modèle de programmation pour le langage Java est réalisé dans la machine virtuelle JikesRVM. Enfin nous décrivons un ensemble d'analyses statiques qui réduit automatiquement le cout à l'exécution de notre approche.

La navigation autonome est un axe de recherche principal dans le domaine de la robotique mobile. Dans ce contexte, le robot doit disposer des algorithmes qui lui permettent d’évoluer de manière autonome dans des environnements complexes et inconnus. Les algorithmes de SLAM permettent à un robot de cartographier son environnement tout en se localisant dans l’espace. Les algorithmes SLAM sont de plus en plus performants, mais aucune implémentation matérielle ou architecturale complète n’a eu. Une telle implantation d’architecture doit prendre en considération la consommation d’énergie, l’embarquabilité et la puissance de calcul. Ce travail scientifique vise à évaluer des systèmes embarqués impliquant de la localisation ou reconstruction de scène. La méthodologie adoptera une approche A3 (Adéquation Algorithme Architecture) pour améliorer l’efficacité de l’implantation des algorithmes plus particulièrement pour des systèmes à fortes contraintes. Le système SLAM embarqué doit disposer d’une architecture électronique et logicielle permettant d’assurer la production d’information pertinentes à partir de données capteurs, tout en assurant la localisation de l’embarquant dans son environnement. L’objectif est donc de définir, pour un algorithme choisi, un modèle d’architecture répondant aux contraintes de l’embarqué. Les premiers travaux de cette thèse ont consisté à explorer les différentes approches algorithmiques permettant la résolution du problème de SLAM. Une étude plus approfondie de ces algorithmes est réalisée. Ceci nous a permet d’évaluer quatre algorithmes de différente nature : FastSLAM2.0, ORB SLAM, RatSLAM et le SLAM linéaire. Ces algorithmes ont été ensuite évalués sur plusieurs architectures pour l’embarqué afin d’étudier leur portabilité sur des systèmes de faible consommation énergétique et de ressources limitées. La comparaison prend en compte les temps d’exécutions et la consistance des résultats. Après avoir analysé profondément les évaluations temporelles de chaque algorithme, le FastSLAM2.0 est finalement choisi, pour un compromis temps d’exécution-consistance de résultat de localisation, comme candidat pour une étude plus approfondie sur une architecture hétérogène embarquée. La second partie de cette thèse est consacré à l’étude d’un système embarqué implémentant le FastSLAM2.0 monoculaire dédié aux environnements larges. Une réécriture algorithmique du FastSLAM2.0 a été nécessaire afin de l’adapter au mieux aux contraintes imposées par les environnements de grande échelle. Dans une démarche A3, le FastSLAM2.0 a été implanté sur une architecture hétérogène CPU-GPU. Grâce à un partitionnement efficace, un facteur d’accélération global de l’ordre de 22 a été obtenu sur une architecture récente dédiée pour l’embarqué. La nature du traitement de l’algorithme FastSLAM2.0 pouvait bénéficier d’une architecture fortement parallèle. Une deuxième instance matérielle basée sur une architecture programmable FPGA est proposée. L’implantation a été réalisée en utilisant des outils de synthèse de haut-niveau afin de réduire le temps de développement. Une comparaison des résultats d’implantation sur cette architecture matérielle par rapport à des architectures à base de GPU a été réalisée. Les gains obtenus sont conséquent, même par rapport aux GPU haut-de-gamme avec un grand nombre de cœurs. Le système résultant peut cartographier des environnements larges tout en garantissant le compromis entre la consistance des résultats de localisation et le temps réel. L’utilisation de plusieurs calculateurs implique d’utiliser des moyens d’échanges de données entre ces derniers. Cela passe par des couplages forts. Ces travaux de thèse ont permis de mettre en avant l’intérêt des architectures hétérogènes parallèles pour le portage des algorithmes SLAM. Les architectures hétérogènes à base de FPGA peuvent particulièrement devenir des candidats potentiels pour porter des algorithmes complexes traitant des données massives<br>Autonomous navigation is a main axis of research in the field of mobile robotics. In this context, the robot must have an algorithm that allow the robot to move autonomously in a complex and unfamiliar environments. Mapping in advance by a human operator is a tedious and time consuming task. On the other hand, it is not always reliable, especially when the structure of the environment changes. SLAM algorithms allow a robot to map its environment while localizing it in the space.SLAM algorithms are becoming more efficient, but there is no full hardware or architectural implementation that has taken place . Such implantation of architecture must take into account the energy consumption, the embeddability and computing power. This scientific work aims to evaluate the embedded systems implementing locatization and scene reconstruction (SLAM). The methodology will adopt an approach AAM ( Algorithm Architecture Matching) to improve the efficiency of the implementation of algorithms especially for systems with high constaints. SLAM embedded system must have an electronic and software architecture to ensure the production of relevant data from sensor information, while ensuring the localization of the robot in its environment. Therefore, the objective is to define, for a chosen algorithm, an architecture model that meets the constraints of embedded systems. The first work of this thesis was to explore the different algorithmic approaches for solving the SLAM problem. Further study of these algorithms is performed. This allows us to evaluate four different kinds of algorithms: FastSLAM2.0, ORB SLAM, SLAM RatSLAM and linear. These algorithms were then evaluated on multiple architectures for embedded systems to study their portability on energy low consumption systems and limited resources. The comparison takes into account the time of execution and consistency of results. After having deeply analyzed the temporal evaluations for each algorithm, the FastSLAM2.0 was finally chosen for its compromise performance-consistency of localization result and execution time, as a candidate for further study on an embedded heterogeneous architecture. The second part of this thesis is devoted to the study of an embedded implementing of the monocular FastSLAM2.0 which is dedicated to large scale environments. An algorithmic modification of the FastSLAM2.0 was necessary in order to better adapt it to the constraints imposed by the largescale environments. The resulting system is designed around a parallel multi-core architecture. Using an algorithm architecture matching approach, the FastSLAM2.0 was implemeted on a heterogeneous CPU-GPU architecture. Uisng an effective algorithme partitioning, an overall acceleration factor o about 22 was obtained on a recent dedicated architecture for embedded systems. The nature of the execution of FastSLAM2.0 algorithm could benefit from a highly parallel architecture. A second instance hardware based on programmable FPGA architecture is proposed. The implantation was performed using high-level synthesis tools to reduce development time. A comparison of the results of implementation on the hardware architecture compared to GPU-based architectures was realized. The gains obtained are promising, even compared to a high-end GPU that currently have a large number of cores. The resulting system can map a large environments while maintainingthe balance between the consistency of the localization results and real time performance. Using multiple calculators involves the use of a means of data exchange between them. This requires strong coupling (communication bus and shared memory). This thesis work has put forward the interests of parallel heterogeneous architectures (multicore, GPU) for embedding the SLAM algorithms. The FPGA-based heterogeneous architectures can particularly become potential candidatesto bring complex algorithms dealing with massive data

Cette thèse propose des solutions aux problématiques inhérentes au contrôle de formations aériennes de type leader­-suiveur pour des flottes de quadrirotors. Au regard des travaux existants, les stratégies qui sont proposés dans notre travail, considère que le(s) leader{s) a une interaction avec les suiveurs. En outre, les rôles de leader et de suiveur sont interchangeables lors de la formation. Dans un premier temps, la modélisation mathématique d'un seul quadrirotor et celle de la formation de quadrirotors est développée. Ensuite, le problème de suivi de trajectoire pour un seul quadrirotor est étudié. Au travers de l'analyse de 1, dynamique du système pour la conception d'une commande par platitude, il apparait que le suivi de trajectoire pour chaque quadrirotor équivaut à déterminer les sorties plates désirées. Un contrôleur pour système plats permettant l'asservissement des drones pour le suivi de trajectoire est donc proposé. Étant donné la propriété de double-boucle de la dynamique du quadrirotor en boucle fermée, un contrôleur d'attitude avec des grands gains est conçu, selon la théorie « singular perturbation system ». Puisque la dynamique du quadrirotor en boucle fermée fonctionne sur deux échelles de temps, la dynamique de rotation (boundary-layer mode) est contrôlée sur l'échelle de temps la plus rapide. La conception du contrôleur de formation dépend seulement de la dynamique de translation (modèle réduit dans une échelle de temps lente). Ce résultat a simplifié la conception du contrôleur de formation, de telle sorte que le modèle réduit du quadrirotor est utilisé au lieu du modèle complet. Étant donné que le modèle réduit du quadrirotor a une caractéristique de double-intégrateur, un algorithme de consensus pour des systèmes caractérisés par de multiple double-intégrateurs est proposé. Pour traiter le problème de la formation leader-suiveur, une matrice d'interaction est initialement proposée basée sur la matrice de Laplacienne. Nous montrons que la condition de convergence et la vitesse de convergence de l'erreur de formation dépendent de la plus petite valeur propre de la matrice d'interaction. Trois stratégies de contrôle de la formation avec une topologie fixe sont ensuite proposées. Le contrôle de formation par platitude est proposé pour obtenir une formation agressive, tandis que les dérivées de grands ordres de la trajectoire désirée pour chaque UAV sont estimées en utilisant un observateur; la méthode Lyapunov redesign est implémentée pour traiter les non-linéarités de la dynamique de la translation des quadrotors; une loi de commande bornée par l'utilisation, entre autre, de la fonction tangente hyperbolique est développée avec un feedback composite non linéaire, afin d'améliorer les performances de la formation. De plus, une commande de commutation saturée de la formation est étudiée, car la topologie de la formation est variable. La stabilité du système est obtenue grâce aux théories “convex hull » et « common Lyapunov function ». Cette stratégie de commande de commutation permet le changement des leaders dans la formation. Inspirée par certains travaux existants, tels que le contrôle de la formation avec des voisins anonymes, nous proposons, finalement, une loi de commande avec des voisins pondérés, qui montre une meilleure robustesse que le contrôle avec des voisins anonymes. Les résultats de simulation obtenus avec Matlab illustrent premièrement nos stratégies de contrôle que nous proposons De plus, en utilisant le langage de programmation C ++, nos stratégies sont mises en œuvre dans un framework de simulation et d'expérimentation développé au laboratoire Heudiasyc. Grâce aux nombreux tests variés que nous avons réalisés en simulation et en temps-réel, l'efficacité et les avantages de nos stratégies de contrôle de la formation proposées sont présentés<br>In this thesis, we address a leader-follower (L-F) formation control problem for multiple UAVs, especially quadrotors. Different from existing works, the strategies, which are proposed in our work, consider that the leader(s) have interaction with the followers. Additionally, the leader(s) are changeable during the formation. First, the mathematical modeling of a single quadrotor and of the formation of quadrotors is developed. The trajectory tracking problem for a single quadrotor is investigated. Through the analysis of the flatness of the quadrotor dynamical model, the desired trajectory for each quadrotor is transferred to the design of the desired at outputs. A flatness-based trajectory tracking controller is, then, proposed. Considering the double-loop property of the closed-loop quadrotor dynamics, a high-gain attitude controller is designed, according to the singular perturbation system theory. Since the closed-loop quadrotor dynamics performs in two time scales, the rotational dynamics (boundary-layer model) is controlled in a fast time scale. The formation controller design is then only considered for the translational dynamics: reduced model in a slow time scale. This result has simplified the formation controller design such that the reduced model of the quadrotor is considered instead of the complete model. Since the reduced model of the quadrotor has a double-integrator characteristic, consensus algorithm for multiple double-integrator systems is proposed. Dealing with the leader-follower formation problem, an interaction matrix is originally proposed based on the Laplacian matrix. We prove that the convergence condition and convergence speed of the formation error are in terms of the smallest eigenvalue of the interaction matrix. Three formation control strategies with fixed formation topology are then proposed. The flatness-based formation control is proposed to deal with the aggressive formation problem, while the high-order derivatives of the desired trajectory for each UAV are estimated by using an observer; the Lyapunov redesign is developed to deal with the nonlinearities of the translational dynamics of the quadrotors; the hyperbolic tangent-based bounded control with composite nonlinear feedback is developed in order to improve the performance of the formation. In an additional way, a saturated switching control of the formation is investigated, where the formation topology is switching. The stability of the system is obtained by introducing the convex hull theory and the common Lyapunov function. This switching control strategy permits the change of the leaders in the formation. Inspired by some existing works, such as the anonymous neighbor-based formation control, we finally propose a weighted neighbor-based control, which shows better robustness than the anonymous neighbor-based control. Simulation results using Matlab primarily illustrate our proposed formation control strategies. Furthermore, using C++ programming, our strategies are implemented on the simulator-experiment framework, developed at Heudiasyc laboratory. Through a variety of tests on the simulator and real-time experiments, the efficiency and the advantages of our proposed formation control strategies are shown. Finally, a vision-based inter-distance detection system is developed. This system is composed by an on-board camera, infrared LEDs and an infrared filter. The idea is to detect the UAVs and calculate the inter-distance by calculating the area of the special LEDs patterns. This algorithm is validated on a PC, with a webcam and primarily implemented on a real quadrotor