Systèmes à base de composants : du design à l'implémentation, Component-based systems : from design to implementation

Imane Ben Hafaiedh

Description

Sous la direction de Susanne Graf
Thèse soutenue le 03 février 2011: UNIVERSITE DE GRENOBLE, Grenoble
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.
-Design à base de composants
-Contracts
-Vérification compositionelle
-Contrôle distribué
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.
-Contracts
-Composional verfication
-Component-based design
Source: http://www.theses.fr/2011GRENM005/document

Informations

• Publié par: Thesee
• Nombre de lectures: 33
• Langue: English
• Poids de l'ouvrage: 1 Mo

Extrait

THÈSE
Pour obtenir le grade de
DOCTEUR DE L’UNIVERSITÉ DE GRENOBLE
Spécialité : Informatique
Arrêté ministériel : 7 août 2006
Présentée par
« Imene BEN HAFAIEDH »
Thèse dirigée par« Susanne GRAF »
préparée au sein dLu aboratoire VERIMAG
dans l'École Doctorale MSTII
Systèmes à base de
Composants: du Design à
l'Implémentation
Thèse soutenue publiquement l«e 03/02/2011 »,
devant le jury composé d e:
Mr. Jean-Claude FERNANDEZ
Professeur , Université de Grenoble I (Président)
Mr. Elie NAJM
Professeur,Te lecom ParisTech (Rapporteur)
Mr. Iulian OBER
Maître de conférence HDR, Université de Toulouse (Rapporteur)
Mr. Gerardo SCHNEIDER
Professeur, Université de Gothenburg (Membre)
Mme. Susanne GRAF
Directeur de recherche au CNRS (Membre)
tel-00573291, version 1 - 3 Mar 2011Abstract
The goal of the thesis is to provide theory, methods and tools for the design and imple-
mentation 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 sys-
tems 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.
Key words: Component-based design, contract, compositional verification, dis-
tributed control, synchronization, priority.
1
tel-00573291, version 1 - 3 Mar 2011Résumé
Dans cette thèse, nous nous sommes intéressés aux design, vérification et implémen-
tation des systèmes à base de composants.
Nous proposons d’abord une méthodologie de design et de vérification composi-
tionelle et incrémentale à base de contrats pour les systèmes de composants. Nous pro-
posons ensuite une implémentation distribuée qui permet de préserver certaines proper-
iétés globales de ces systèmes.
La méthodologie de design proposée utilise les contrats comme un moyen de con-
traindre, 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.
Mots clés: Design à base de composants, contrat, vérification compositionelle, con-
trôle distribué, synchronisation, priorité.
2
tel-00573291, version 1 - 3 Mar 2011Table of contents
Table of contents 3
List of Figures 7
I Context 9
1 Introduction 11
1.1 Problems and needs . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 11
1.2 Design and verification of complex systems . . . . . . . . . . . . . . . . . . . . . . 13
1.2.1 Compositional reasoning . . . . . . . . . . . . . . . . . . . . . . . . . . . . 13
1.2.2 Using contracts . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 14
1.2.3 Property verification . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 15
1.2.4 Our contribution . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 16
1.3 Distributed systems with rich interaction models . . . . . . . . . . . . . . . . . . . . 18
1.3.1 Distributed control . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 18
1.3.2 Our contribution . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 19
1.4 Organization of the thesis . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 21
2 Preliminaries 23
2.1 The BIP modeling framework . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 23
2.1.1 Labeled Transition Systems . . . . . . . . . . . . . . . . . . . . . . . . . . 23
2.1.2 Component-based design with BIP . . . . . . . . . . . . . . . . . . . . . . . 25
2.1.3 Basic concepts of BIP . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 27
2.1.4 Glues in BIP: Interaction models . . . . . . . . . . . . . . . . . . . . . . . . 29
2.1.5 Composition of components in BIP . . . . . . . . . . . . . . . . . . . . . . 32
2.1.6 Priorities in BIP . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
2.2 Contract framework concepts . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
2.2.1 Contract frameworks . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
2.2.2 Dominance . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
3
tel-00573291, version 1 - 3 Mar 2011TABLE OF CONTENTS
II A Contract Framework for Reasoning about Safety and Progress 43
3 Contract-Based Verification Approach 45
3.1 Design and v methodology . . . . . . . . . . . . . . . . . . . . . . . . . . 46
3.1.1 Methodology . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46
3.1.2 Extension to recursively defined systems . . . . . . . . . . . . . . . . . . . 50
3.2 Soundness of the methodology . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51
3.2.1 Soundness . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52
3.2.2 Compatibility of glues . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52
3.3 Proving dominance . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53
3.3.1 Circular reasoning . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53
4 A Contract Framework for Components with Data 59
4.1 Components with data . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 59
4.1.1 Semantics . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 61
4.2 Glues: Rich interaction model . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 64
4.2.1 Connectors . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 64
4.2.2 Composition . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 66
4.2.3 of interaction models . . . . . . . . . . . . . . . . . . . . . . . 69
4.3 Progress description . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 71
4.3.1 Progress in components . . . . . . . . . . . . . . . . . . . . . . . . . . . . 71
4.3.2 of a composition . . . . . . . . . . . . . . . . . . . . . . . . . . . 74
4.4 Relations of the contract framework . . . . . . . . . . . . . . . . . . . . . . . . . . 76
4.4.1 Refinement . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 76
4.4.2 Conformance . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 80
4.5 Proofs . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 81
4.5.1 Well-definedness of the contract framework . . . . . . . . . . . . . . . . . . 81
5 An Application: Resource Sharing in a Networked System 87
5.1 Sharing resource system . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 87
5.1.1 The top-level requirement’. . . . . . . . . . . . . . . . . . . . . . . . . . . 90
5.1.2 Methodology . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 90
5.1.3 Interaction models and contracts . . . . . . . . . . . . . . . . . . . . . . . . 91
5.2 Implementation and experimental results . . . . . . . . . . . . . . . . . . . . . . . . 96
5.2.1 Refinement checker module. . . . . . . . . . . . . . . . . . . . . . . . . . . 96
5.2.2 Composition module. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 98
5.2.3 Results. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 99
III Building Distributed Controllers for Systems with Priorities 101
6 Controllers for Systems with Priorities 103
6.1 Systems and controlled systems . . . . . . . . . . . . . . . . . . . . . . . . . . . . 104
4
tel-00573291, version 1 -