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