Design, vérification et implémentation de systèmes à composants

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.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