L'utilisation d'équipes de robots a pris de l'ampleur ces dernières années. Cela est dû aux avantages que peut offrir une équipe de robot par rapport à un robot seul pour la réalisation d'une même tâche. Cela s'explique aussi par le fait que ce type de plates-formes deviennent de plus en plus abordables et fiables. Ainsi, l'utilisation d'une équipe de véhicules aériens devient une alternative viable. Cette thèse se concentre sur le problème du déploiement d'une équipe de Micro-Véhicules Aériens (MAV) pour effectuer des missions de surveillance sur un terrain inconnu de morphologie arbitraire. Puisque la morphologie du terrain est inconnue et peut être complexe et non-convexe, les algorithmes standards ne sont pas applicables au problème particulier traité dans cette thèse. Pour y remédier, une nouvelle approche basée sur un algorithme d'optimisation cognitive et adaptatif (CAO) est proposée et évaluée. Une propriété fondamentale de cette approche est qu'elle partage les mêmes caractéristiques de convergence que les algorithmes de descente de gradient avec contraintes qui exigent une connaissance parfaite de la morphologie du terrain pour optimiser la couverture. Il est également proposé une formulation différente du problème afin d'obtenir une solution distribuée, ce qui nous permet de surmonter les inconvénients d'une approche centralisée et d'envisager également des capacités de communication limitées. De rigoureux arguments mathématiques et des simulations étendues établissent que l'approche proposée fournit une méthodologie évolutive et efficace qui intègre toutes les contraintes physiques particulières et est capable de guider les robots vers un arrangement qui optimise localement la surveillance. Finalement, la méthode proposée est mise en œuvre sur une équipe de MAV réels pour réaliser la surveillance d'un environnement extérieur complexe.

Dans cette thèse, nous nous sommes intéressés aux design, vérification et implémentation des systèmes à base de composants. Nous proposons d'abord une méthodologie de design et de vérification compositionelle et incrémentale à base de contrats pour les systèmes de composants. Nous proposons ensuite une implémentation distribuée qui permet de préserver certaines properiétés globales de ces systèmes. La méthodologie de design proposée utilise les contrats comme un moyen de contraindre, raffiner et d'implémenter les systèmes. Elle est basée sur un formalisme de contracts générique, que nous instancions pour un formalisme de composants permettant la description des propriétés de progrés. Nous étendons cette méthodologie pour raisonner sur des systèmes de taille arbitraire et nous prouvons son utilité pour vérifier des propriétés de sûreté et de progrés d'un réseau de noeuds distribués. Dans le contexte des systèmes distribués, les systèmes doivent être implémenter de manière distribuée. Nous proposons dans cette thèse un protocole qui permet l'exécution distribuée des systèmes tout en préservant certaines propriétés globales à savoir des synchronisations et des priorités et où les composants interagissent par échange de messages. Nous proposons également une implémentation du protocole pour une plateforme particulière. / The goal of the thesis is to provide theory, methods and tools for the design and implementation of component-based systems. To master the complexity of systems of components, we first propose a contract-based design and verification approach which is both compositional and incremental. Then we provide a distributed implementation of these systems allowing to preserve some global properties. The proposed verification approach uses contracts as a means to constrain, refine and implement systems. It is based on a generic contract framework that we instantiate for a component framework allowing to express progress properties. We also extend the approach to reason about systems of arbitrary size and we show its usefulness for proving safety and progress properties in networked systems. In the context of distributed settings, these systems must later be executed in a distributed fashion. We also propose in this thesis a protocol that allows executing systems in a distributed way while preserving some global requirements namely priorities and synchronizations and where components interact by message exchange. Then, we provide an implementation of this protocol in a particular platform.

Nous avons étudié dans le cadre de cette thèse le design, la vérification et l'implémentation des systèmes à composants. Nous nous sommes intéressés en particulier aux formalismes exprimant des interactions complexes, dans lesquels les connecteurs servent non seulement au transfert de données mais également à la synchronisation entre composants. 1. DESIGN ET VÉRIFICATION Le design par contrat est une approche largement répandue pour développer des systèmes lorsque plusieurs équipes travaillent en parallèle. Les contrats représentent des contraintes sur les implémentations qui sont préservées tout au long du développement et du cycle de vie d'un système. Ils peuvent donc servir également à la phase de vérification d'un tel système. Notre but n'est pas de proposer un nouveau formalisme de spécification, mais plutôt de définir un ensemble minimal de propriétés qu'une théorie basée sur les contrats doit satisfaire pour permettre certains raisonnements. En cela, nous cherchons à séparer explicitement les propriétés spécifiques à chaque formalisme de spécification et les règles de preuves génériques. Nous nous sommes attachés à fournir des définitions suffisamment générales pour exprimer un large panel de langages de spécification, et plus particulièrement ceux dans lesquels les interactions sont complexes, tels que Reo ou BIP. Pour ces derniers, raisonner sur la structure du système est essentiel et c'est pour cette raison que nos contrats ont une partie structurelle. Nous montrons comment découle de la propriété nommée raisonnement circulaire une règle pour prouver la dominance sans composer les contrats, et comment cette propriété peut être affaiblie en utilisant plusieurs relations de raffinement. Notre travail a été motivé par les langages de composants HRC L0 et L1 définis dans le projet SPEEDS. 2. IMPLÉMENTATION Synthétiser un contrôleur distribué imposant une contrainte globale sur un système est dans le cas général un problème indécidable. On peut obtenir la décidabilité en réduisant la concurrence: nous proposons une méthode qui synchronise les processus de façon temporaire. Dans les travaux de Basu et al., le contrôle distribué est obtenu en pré-calculant par model checking la connaissance de chaque processus, qui reflète dans un état local donné toutes les configurations possibles des autres processus. Ensuite, à l'exécution, le contrôleur local d'un processus décide si une action peut être exécutée sans violer la contrainte globale. Nous utilisons de même des techniques de model checking pour pré-calculer un ensemble minimal de points de synchronisation au niveau desquels plusieurs processus partagent leur connaissance au court de brèves périodes de coordination. Après chaque synchronisation, les processus impliqués peuvent de nouveau progresser indépendamment les uns des autres jusqu'à ce qu'une autre synchronisation ait lieu. Une des motivations pour ce travail est l'implémentation distribuée de systèmes BIP. / In this thesis, we have studied how component-based systems are designed, verified and then implemented. We have focused in particular on formalisms involving complex interactions, where connectors are not only used to transfer data but also play a role in the synchronization of components. 1. DESIGN AND VERIFICATION Contracts are emerging as a concept of choice when systems are designed by teams working independently. They are design constraints for implementations which are maintained throughout the development and life cycle of the system, thus being also useful for verification. Our goal is not to propose a new design framework but rather to define a minimal set of properties which a given contract theory should satisfy to offer some reasoning rules. In that sense, we aim at a separation of concerns between framework-dependent properties and generic proof rules. We have focused on finding definitions expressive enough to encompass a great variety of existing specification formalisms, and in particular those in which interaction is complex, like Reo and BIP. For those, reasoning about the structure of the system is essential and this is why our contracts have a structural part. We show how so-called circular reasoning entails a rule for proving dominance (refinement between contracts) without composing contracts and how it can be relaxed by combining several refinement relations. Our work has a practical motivation in the component frameworks HRC L0 and L1 defined in the SPEEDS IP project. 2. IMPLEMENTATION The problem of synthesizing a distributed controller that imposes some global constraint on a system is, in general, undecidable. One can achieve decidability at the expense of reducing concurrency: we propose a method that synchronizes processes temporarily. In Basu et al., distributed control is achieved by first using model checking to precalculate the knowledge of each process, which reflects in a given local state all the possible situations of the other processes. Then, at runtime, the local controller of a process decides whether an action of that process can be executed without violating the imposed constraint. We use model checking techniques as well to precalculate a minimal set of synchronization points, where joint knowledge, i.e., knowledge common to several processes, can be achieved during short coordination phases. After each synchronization, the participating processes can again progress independently until a further synchronization is called for. One practical motivation for this work is the distributed implementation of BIP systems.

Dans cette thèse, nous nous sommes intéressés aux design, vérification et implémentation des systèmes à base de composants. Nous proposons d'abord une méthodologie de design et de vérification compositionelle et incrémentale à base de contrats pour les systèmes de composants. Nous proposons ensuite une implémentation distribuée qui permet de préserver certaines properiétés globales de ces systèmes. La méthodologie de design proposée utilise les contrats comme un moyen de contraindre, raffiner et d'implémenter les systèmes. Elle est basée sur un formalisme de contracts générique, que nous instancions pour un formalisme de composants permettant la description des propriétés de progrés. Nous étendons cette méthodologie pour raisonner sur des systèmes de taille arbitraire et nous prouvons son utilité pour vérifier des propriétés de sûreté et de progrés d'un réseau de noeuds distribués. Dans le contexte des systèmes distribués, les systèmes doivent être implémenter de manière distribuée. Nous proposons dans cette thèse un protocole qui permet l'exécution distribuée des systèmes tout en préservant certaines propriétés globales à savoir des synchronisations et des priorités et où les composants interagissent par échange de messages. Nous proposons également une implémentation du protocole pour une plateforme particulière.

Nous avons étudié dans le cadre de cette thèse le design, la vérification et l'implémentation des systèmes à composants. Nous nous sommes intéressés en particulier aux formalismes exprimant des interactions complexes, dans lesquels les connecteurs servent non seulement au transfert de données mais également à la synchronisation entre composants. 1. DESIGN ET VÉRIFICATION Le design par contrat est une approche largement répandue pour développer des systèmes lorsque plusieurs équipes travaillent en parallèle. Les contrats représentent des contraintes sur les implémentations qui sont préservées tout au long du développement et du cycle de vie d'un système. Ils peuvent donc servir également à la phase de vérification d'un tel système. Notre but n'est pas de proposer un nouveau formalisme de spécification, mais plutôt de définir un ensemble minimal de propriétés qu'une théorie basée sur les contrats doit satisfaire pour permettre certains raisonnements. En cela, nous cherchons à séparer explicitement les propriétés spécifiques à chaque formalisme de spécification et les règles de preuves génériques. Nous nous sommes attachés à fournir des définitions suffisamment générales pour exprimer un large panel de langages de spécification, et plus particulièrement ceux dans lesquels les interactions sont complexes, tels que Reo ou BIP. Pour ces derniers, raisonner sur la structure du système est essentiel et c'est pour cette raison que nos contrats ont une partie structurelle. Nous montrons comment découle de la propriété nommée raisonnement circulaire une règle pour prouver la dominance sans composer les contrats, et comment cette propriété peut être affaiblie en utilisant plusieurs relations de raffinement. Notre travail a été motivé par les langages de composants HRC L0 et L1 définis dans le projet SPEEDS. 2. IMPLÉMENTATION Synthétiser un contrôleur distribué imposant une contrainte globale sur un système est dans le cas général un problème indécidable. On peut obtenir la décidabilité en réduisant la concurrence: nous proposons une méthode qui synchronise les processus de façon temporaire. Dans les travaux de Basu et al., le contrôle distribué est obtenu en pré-calculant par model checking la connaissance de chaque processus, qui reflète dans un état local donné toutes les configurations possibles des autres processus. Ensuite, à l'exécution, le contrôleur local d'un processus décide si une action peut être exécutée sans violer la contrainte globale. Nous utilisons de même des techniques de model checking pour pré-calculer un ensemble minimal de points de synchronisation au niveau desquels plusieurs processus partagent leur connaissance au court de brèves périodes de coordination. Après chaque synchronisation, les processus impliqués peuvent de nouveau progresser indépendamment les uns des autres jusqu'à ce qu'une autre synchronisation ait lieu. Une des motivations pour ce travail est l'implémentation distribuée de systèmes BIP.

L'utilisation d'équipes de robots a pris de l'ampleur ces dernières années. Cela est dû aux avantages que peut offrir une équipe de robot par rapport à un robot seul pour la réalisation d'une même tâche. Cela s'explique aussi par le fait que ce type de plates-formes deviennent de plus en plus abordables et fiables. Ainsi, l'utilisation d'une équipe de véhicules aériens devient une alternative viable. Cette thèse se concentre sur le problème du déploiement d'une équipe de Micro-Véhicules Aériens (MAV) pour effectuer des missions de surveillance sur un terrain inconnu de morphologie arbitraire. Puisque la morphologie du terrain est inconnue et peut être complexe et non-convexe, les algorithmes standards ne sont pas applicables au problème particulier traité dans cette thèse. Pour y remédier, une nouvelle approche basée sur un algorithme d'optimisation cognitive et adaptatif (CAO) est proposée et évaluée. Une propriété fondamentale de cette approche est qu'elle partage les mêmes caractéristiques de convergence que les algorithmes de descente de gradient avec contraintes qui exigent une connaissance parfaite de la morphologie du terrain pour optimiser la couverture. Il est également proposé une formulation différente du problème afin d'obtenir une solution distribuée, ce qui nous permet de surmonter les inconvénients d'une approche centralisée et d'envisager également des capacités de communication limitées. De rigoureux arguments mathématiques et des simulations étendues établissent que l'approche proposée fournit une méthodologie évolutive et efficace qui intègre toutes les contraintes physiques particulières et est capable de guider les robots vers un arrangement qui optimise localement la surveillance. Finalement, la méthode proposée est mise en œuvre sur une équipe de MAV réels pour réaliser la surveillance d'un environnement extérieur complexe.

Cette thèse porte sur des stratégies distribuées pour systèmes multi-robot. Tout d'abord, nous nous focalisons sur des algorithmes de consensus pour des systèmes hétérogènes qui représente, par exemple, différents modèles ou générations de robots. Dans la suite, nous proposons deux solutions pour améliorer les propriétés de connectivité du système. Tout d'abord, nous montrons comment améliorer la vitesse de convergence des algorithmes de consensus en modifiant les protocoles classiques. Plus précisément, nous appliquons le principe de retard stabilisant et nous montrons comment de l'information échantillonné convenablement peut être utilisée dans la design du contrôleur. Enfin, nous concevons et analysons un algorithme pour le déploiement d'agents compact. Dans cette approche, qui augmente le nombre de connexions du graphe, la configuration souhaitée de l'ensemble des robots est entièrement spécifiée par les angles inter-agents. La stratégie proposée est un algorithme complètement distribué, uniquement basée sur l'information locale qui permet l'auto-organisation du système.

L'utilisation d'équipes de robots a pris de l'ampleur ces dernières années. Cela est dû aux avantages que peut offrir une équipe de robot par rapport à un robot seul pour la réalisation d'une même tâche. Cela s'explique aussi par le fait que ce type de plates-formes deviennent de plus en plus abordables et fiables. Ainsi, l'utilisation d'une équipe de véhicules aériens devient une alternative viable. Cette thèse se concentre sur le problème du déploiement d'une équipe de Micro-Véhicules Aériens (MAV) pour effectuer des missions de surveillance sur un terrain inconnu de morphologie arbitraire. Puisque la morphologie du terrain est inconnue et peut être complexe et non-convexe, les algorithmes standards ne sont pas applicables au problème particulier traité dans cette thèse. Pour y remédier, une nouvelle approche basée sur un algorithme d'optimisation cognitive et adaptatif (CAO) est proposée et évaluée. Une propriété fondamentale de cette approche est qu'elle partage les mêmes caractéristiques de convergence que les algorithmes de descente de gradient avec contraintes qui exigent une connaissance parfaite de la morphologie du terrain pour optimiser la couverture. Il est également proposé une formulation différente du problème afin d'obtenir une solution distribuée, ce qui nous permet de surmonter les inconvénients d'une approche centralisée et d'envisager également des capacités de communication limitées. De rigoureux arguments mathématiques et des simulations étendues établissent que l'approche proposée fournit une méthodologie évolutive et efficace qui intègre toutes les contraintes physiques particulières et est capable de guider les robots vers un arrangement qui optimise localement la surveillance. Finalement, la méthode proposée est mise en œuvre sur une équipe de MAV réels pour réaliser la surveillance d'un environnement extérieur complexe. / The use of multi-robot teams has gained a lot of attention in recent years. This is due to the extended capabilities that the teams offer compared to the use of a single robot for the same task. Moreover, as these platforms become more and more affordable and robust, the use of teams of aerial vehicles is becoming a viable alternative. This thesis focuses on the problem of deploying a swarm of Micro Aerial Vehicles (MAV) to perform surveillance coverage missions over an unknown terrain of arbitrary morphology. Since the terrain's morphology is unknown and it can be quite complex and non-convex, standard algorithms are not applicable to the particular problem treated in this thesis. To overcome this, a new approach based on the Cognitive-based Adaptive Optimization (CAO) algorithm is proposed and evaluated. A fundamental property of this approach is that it shares the same convergence characteristics as those of constrained gradient-descent algorithms, which require perfect knowledge of the terrain's morphology to optimize coverage. In addition, it is also proposed a different formulation of the problem in order to obtain a distributed solution, which allows us to overcome the drawbacks of a centralized approach and to consider also limited communication capabilities. Rigorous mathematical arguments and extensive simulations establish that the proposed approach provides a scalable and efficient methodology that incorporates any particular physical constraints and limitations able to navigate the robots to an arrangement that (locally) optimizes the surveillance coverage. The proposed method is finally implemented in a real swarm of MAVs to carry out surveillance coverage in an outdoor complex area.

Cette thèse porte sur des stratégies distribuées pour systèmes multi-robot. Tout d'abord, nous nous focalisons sur des algorithmes de consensus pour des systèmes hétérogènes qui représente, par exemple, différents modèles ou générations de robots. Dans la suite, nous proposons deux solutions pour améliorer les propriétés de connectivité du système. Tout d'abord, nous montrons comment améliorer la vitesse de convergence des algorithmes de consensus en modifiant les protocoles classiques. Plus précisément, nous appliquons le principe de retard stabilisant et nous montrons comment de l'information échantillonné convenablement peut être utilisée dans la design du contrôleur. Enfin, nous concevons et analysons un algorithme pour le déploiement d'agents compact. Dans cette approche, qui augmente le nombre de connexions du graphe, la configuration souhaitée de l'ensemble des robots est entièrement spécifiée par les angles inter-agents. La stratégie proposée est un algorithme complètement distribué, uniquement basée sur l'information locale qui permet l'auto-organisation du système. / This dissertation focuses on distributed agreement strategies for multi-robot systems. First of all, we deal with consensus algorithms for heterogeneous systems, representing, for example, different models or generations of robots. In the sequel, we propose two solutions to improve the connectivity properties of the system. Firstly, we show how to improve the consensus algorithm's convergence rate by modifying the classical control algorithms. More precisely, we apply the stabilizing delay principle and we show how appropriately sampled information can be used in the controller's design. Finally, we design and analyse an algorithm for the compact deployment of agents. In this approach, that increases the number of connections of the graph, the desired configuration of the swarm is entirely specified by the inter-agent angles. The proposed strategy is a completely distributed algorithm, only based on local information that allows swarm's self-organization.

Cette thèse considère principalement trois problèmes dans le domaine du contrôle distribué coopératif des systèmes multi-agents(SMA): le consensus, la navigation en formation et le maintien en formation d'un groupe d'agents lorsqu'un agent disparait. Nous proposons 3 algorithmes pour résoudre le problème du calcul distribué d'un consensus à partir de l'approche leadeur-suiveur dans le contexte SMA à dynamique non-linéaire. La référence est définie comme un leader virtuel dont on n'obtient, localement, que les données de position et de vitesse. Pour résoudre le problème du suivi par consensus pour les SMA à dynamique non-linéaire, nous considérons le suivi par consensus pour SMA de premier ordre. On propose des résultats permettant aux suiveurs de suivre le leadeur virtuel en temps fini en ne considérant que les positions des agents. Ensuite, nous considérons le suivi par consensus de SMA de second. Dans le cas de la planification de trajectoire et la commande du mouvement de la formation multi-agents. L'idée est d'amener la formation, dont la dynamique est supposée être en 3D, d'une configuration initiale vers une configuration finale (trouver un chemin faisable en position et orientation) en maintenant sa forme tout le long du chemin en évitant les obstacles. La stratégie proposée se décompose en 3 étapes. Le problème du Closing-Rank se traduit par la réparation d'une formation rigide multi-agents "endommagée" par la perte de l'un de ses agents. Nous proposons 2 algorithmes d'autoréparation systématique pour récupérer la rigidité en cas de perte d'un agent. Ces réparations s'effectuent de manière décentralisée et distribuée n'utilisant que des informations de voisinage.