//img.uscri.be/pth/652458b0c85c4a3197aaa362464f38316d703583
Cet ouvrage fait partie de la bibliothèque YouScribe
Obtenez un accès à la bibliothèque pour le lire en ligne
En savoir plus

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

De
178 pages
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
Voir plus Voir moins

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 - 3 Mar 2011TABLE OF CONTENTS
6.1.1 Components, interaction models and systems . . . . . . . . . . . . . . . . . 104
6.1.2 Controllers defined by properties . . . . . . . . . . . . . . . . . . . . . . . . 107
6.2 Synthesis of priorities for avoiding deadlocks . . . . . . . . . . . . . . . . . . . . . 111
7 Distributed Controllers for Systems with Priorities 119
7.1 Distributing systems and controllers . . . . . . . . . . . . . . . . . . . . . . . . . . 119
7.1.1 Concurrency and confusion . . . . . . . . . . . . . . . . . . . . . . . . . . 121
7.2 Implementation of a distributed controller as a protocol . . . . . . . . . . . . . . . . 124
7.2.1 Description of the protocol . . . . . . . . . . . . . . . . . . . . . . . . . . . 125
7.2.2 Avoiding deadlocks due to potential decision cycles . . . . . . . . . . . . . . 131
7.3 Correctness of the protocol . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 134
8 Implementation and Experimental Results 141
8.1 Sensitivity of the prototype . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 141
8.1.1 Sensitivity to prioritized conflicts . . . . . . . . . . . . . . . . . . . . . . . 142
8.1.2vity to structural . . . . . . . . . . . . . . . . . . . . . . . . 145
8.2 The dining philosophers example . . . . . . . . . . . . . . . . . . . . . . . . . . . . 147
IV Conclusions and Perspectives 149
9 Conclusion and Perspectives 151
9.1 Conclusions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 151
9.2 Perspectives . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 152
Bibliography 155
5
tel-00573291, version 1 - 3 Mar 2011TABLE OF CONTENTS
6
tel-00573291, version 1 - 3 Mar 2011List of Figures
1.1 Approach to the Design of Contract Frameworks. . . . . . . . . . . . . . . . . . . . 17
1.2 Distributed Controllers. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 20
2.1 BIP Layers. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 25
2.2 Component Composition. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 26
2.3 Hierarchical Components. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 26
2.4 Structuring. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 26
2.5 Flattening. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 27
2.6 Atomic Component. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
2.7 Example of Connectors. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
2.8 Structured Connector. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
2.9 Semantics of a composition. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
2.10 Composition of Components. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
2.11 Semantics of Composite Component with Priorities. . . . . . . . . . . . . . . . . . . 35
2.12 Example: Priorities to enforce Mutual Exclusion. . . . . . . . . . . . . . . . . . . . 36
2.13 A hierarchical component and its equivalent flattened form. . . . . . . . . . . . . . . 38
4
2.14 Kv G for conformance defined as simulation. . . . . . . . . . . . . . . . . . . 40A;gl
3.1 Step 2: Conformance. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47
n3.2 Step 3:K defined as a composition offKg usinggl . . . . . . . . . . . . . . . . 48i Ii=1
3.3 Step 3: Dominance (fC ;C ;Cg dominatesC w.r.t. gl ). . . . . . . . . . . . . . . . 491 2 3 I
3.4 Step 4: Satisfaction. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49
3.5 Methodology steps ensuring thatglfA;gl fI ;I ;Igg4’. . . . . . . . . . . . . . 501 2 3I
3.6 gl allows relating the gluegl provided inC to the actual environment forK . . . 531 1E 11
3.7 A counterexample to circular reasoning due to non-determinism. . . . . . . . . . . . 55
3.8 A to due to strong synchronization. . . . . . . . . 55
4.1 Example: Component with data. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 62
4.2 Consistent version of a component with data. . . . . . . . . . . . . . . . . . . . . . 63
4.3 Composition of components. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 68
4.4 Composite component. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 68
4.5 Merge of Connectors. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 69
0 0 04.6 II =f ; g . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 701 2
7
tel-00573291, version 1 - 3 Mar 2011LIST OF FIGURES
0 0 04.7 II =f( )g . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 701 2
4.8 Inferring Progress Conditions. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 73
c a4.9 Refinement:K v K . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 80EK ;I
5.1 The overall structure of the application. . . . . . . . . . . . . . . . . . . . . . . . . 88
5.2 (a) Node Structure. (b) Node Behavior. . . . . . . . . . . . . . 89
5.3 Top-level requirement’ . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 90
5.4 Assumption of the network and the node contract. . . . . . . . . . . . . . . . . . . . 92
5.5 Guarantee of the Node Contract. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 92
5.6 of the Network Contract . . . . . . . . . . . . . . . . . . . . . . . . . . . 93
5.7 I for contractC . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 94Net Net
5.8 Inner structure of a network component. . . . . . . . . . . . . . . . . . . . . . . . . 95
5.9 Refinement Checker Structure. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 97
5.10 Composition Module . . . . . . . . . . . . . . . . . . . . . . . . . . . . 98
6.1 An example where reducing non-determinism eliminates a deadlock. . . . . . . . . . 112
6.2 A simple system not controllable with priorities. . . . . . . . . . . . . . . . . . . . . 113
6.3 A solution to the dining philosophers problem. . . . . . . . . . . . . . . . . . . . . . 114
7.1 Symmetric and asymmetric confusion. . . . . . . . . . . . . . . . . . . . . . . . . . 123
7.2 Prioritized confusion. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 123
7.3 Structure of the protocol forC . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 126i
7.4 An example with global prioritiesc<b. . . . . . . . . . . . . . . . . . . . . . . . 131
7.5 Scenario of possible executions of interactionsa,b andc. . . . . . . . . . . . . . . 132
7.6 An example with cycle and independence. . . . . . . . . . . . . . . . . . . . . . . 134
7.7 State diagram of the algorithm. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 136
8.1 Implementation layers . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 142
8.2 System pattern for experiments . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 143
8.3 Sensitivity to the degree of prioritized conflict . . . . . . . . . . . . . . . . . . . . . 144
8.4 System pattern for experiments (T ) . . . . . . . . . . . . . . . . . . . . . . . . . . 145k
8.5 Sensitivity to the degree of structural conflict . . . . . . . . . . . . . . . . . . . . . 146
8.6 The dining philosophers problem with priorities. . . . . . . . . . . . . . . . . . . . . 147
8
tel-00573291, version 1 - 3 Mar 2011Part I
Context
9
tel-00573291, version 1 - 3 Mar 2011