Establishing properties of interaction systems [Elektronische Ressource] / vorgelegt von Moritz Martens

Sujets

• Informatik

Informations

• Publié par: universitat_mannheim
• Publié le: 01 janvier 2009
• Nombre de lectures: 4
• Langue: English
• Poids de l'ouvrage: 1 Mo

Extrait

Establishing Properties of
Interaction Systems
Inauguraldissertation
zur Erlangung des akademischen Grades
eines Doktors der Naturwissenschaften
der Universit¨at Mannheim
vorgelegt von
Moritz Martens
aus K¨oln
Mannheim, November 2009Dekan: Professor Dr. Felix Freiling, Universit¨at Mannheim
Referentin: Professor Dr. Mila Majster-Cederbaum, Universit¨at Mannheim
Korreferent: Professor Dr. Felix Freiling, Universit¨at Mannheim
Tag der mu¨ndlichen Pru¨fung: 18. Dezember 2009Abstract
We exhibit sufficient conditions for generic properties of component based
systems. The model we use to describe component based systems is the
formalismofinteractionsystems. Becausethestatespaceexplosionproblem
is encountered in interaction systems (i.e., an exploration of the state space
gets unfeasible for a large number of components), we follow the guideline
thattheseconditionshavetobecheckableefficiently(i.e., intimepolynomial
in the number of components). Further, the conditions are designed in such
awaythattheinformationgatheredisreusableifaconditionisnotsatisfied.
Concretely, we consider deadlock-freedom and progress in interaction
systems. We state a sufficient condition for deadlock-freedom that is based
on an architectural constraint: We define what it means for an interaction
system to be tree-like, and we derive a sufficient condition for deadlock-
freedom of such systems. Considering progress, we first present a charac-
terization of this property. Then we state a sufficient condition for progress
whichisbasedonadirectedgraph. Wecombinethisconditionwiththechar-
acterizationtopointoutonepossibilitytoproceedifthegraph-criteriondoes
not yield progress. Both sufficient conditions can be checked efficiently be-
cause they only require the investigation of certain subsystems. Finally, we
consider the effect that failure of some parts of the system has on deadlock-
freedom and progress. We define robustness of deadlock-freedom respec-
tively progress under failure, and we explain how the sufficient conditions
abovehavetobeadaptedinordertobealsoapplicableinthisnewsituation.Zusammenfassung
Wir pra¨sentieren hinreichende Bedingungen fu¨r allgemeine Eigenschaften
von komponentenbasierten Systemen. Als Formalismus zur Modellierung
komponentenbasierter Systeme nutzen wir Interaktionssysteme (interaction
systems). Da fu¨rInteraktionssysteme das Problem der Zustandsraumexplo-
sion auftritt (d.h. fu¨r eine große Anzahl von Komponenten ist eine Analyse
des gesamten Zustandsraums nicht durchfu¨hrbar), sollen die Bedingungen
effizient u¨berpru¨fbar sein (d.h. mit polynomiellem Aufwand in der Anzahl
der Komponenten). Des Weiteren sind die Bedingungen so geartet, dass
die gesammelte Information wiederbenutzbar ist, falls eine Bedingung nicht
erfu¨llt sein sollte.
Im Einzelnen betrachten wir Deadlockfreiheit und Fortschritt in Inter-
aktionssystemen. Wir formulieren eine hinreichende Bedingung fu¨r Dead-
lockfreiheit, welche auf einer Einschra¨nkung an die Kommunikationsarchi-
tektur basiert: Wir definieren baumartige Interaktionssysteme und leiten
dann eine hinreichende Bedingung fu¨r die Deadlockfreiheit solcher Systeme
her. Im Hinblick auf Fortschritt geben wir zuna¨chst eine Charakterisierung
dieserEigenschaftan. Dannformulierenwirbasierendaufeinemgerichteten
Graphen eine hinreichende Bedingung fu¨r Fortschritt. Wir kombinieren
diese Bedingung mit der Charakterisierung, um einen Ausweg aufzuzeigen,
falls das Graphkriterium nicht erfu¨llt ist. Beide hinreichenden Bedingungen
k¨onnen effizient u¨berpru¨ftwerden, weil nur die Analyse bestimmter Teilsys-
teme erforderlich ist. Schließlich untersuchen wir noch die Auswirkungen,
welche der Ausfall bestimmter Teile eines Systems auf Deadlockfreiheit und
Fortschritt hat. Wir definieren zuna¨chst Robustheit von Deadlockfreiheit
beziehungsweise Fortschritt unter Ausfall. Dann erkl¨aren wir, wie die obi-
gen hinreichenden Bedingungen angepasst werden mu¨ssen, damit sie auf
diese neue Situation angewendet werden k¨onnen.Ruhe in Frieden, Unglu¨cksbock!
To
VII
HennesContents
1 Introduction 1
1.1 Component Based Systems . . . . . . . . . . . . . . . . . . . 1
1.2 Establishing Properties — Goal of this Thesis . . . . . . . . . 4
1.2.1 Methodologies . . . . . . . . . . . . . . . . . . . . . . 4
1.2.2 Goal of this Thesis . . . . . . . . . . . . . . . . . . . . 9
1.3 Other Approaches Towards Component Systems . . . . . . . 10
1.4 Thesis Outline . . . . . . . . . . . . . . . . . . . . . . . . . . 15
2 Interaction Systems 19
2.1 Components, Interactions, and Interaction Systems . . . . . . 19
2.2 Properties of Interaction Systems . . . . . . . . . . . . . . . . 28
2.3 Conclusion and Discussion . . . . . . . . . . . . . . . . . . . . 34
3 Deadlock-Freedom for Component Systems with Architec-
tural Constraints 37
3.1 Motivation . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
3.2 Reachability in Interaction Systems . . . . . . . . . . . . . . . 39
3.3 Architectural Patterns . . . . . . . . . . . . . . . . . . . . . . 50
3.4 Deadlock-Freedom for Tree-Like Component Architectures . . 54
3.4.1 Interaction Systems with Multiway Cooperation . . . 54
3.4.2 Strongly Tree-Like Interaction Systems . . . . . . . . 64
3.5 Freedom of Local Deadlocks for Tree-Like Component Archi-
tectures . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 69
3.5.1 Strongly Tree-Like Interaction Systems . . . . . . . . 69
3.5.2 Interaction Systems with Multiway Cooperation . . . 70
3.6 Examples . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 71
3.6.1 A Banking System . . . . . . . . . . . . . . . . . . . . 71
iii CONTENTS
3.6.2 The River Delta . . . . . . . . . . . . . . . . . . . . . 77
3.6.3 The Railway Track . . . . . . . . . . . . . . . . . . . . 80
3.7 Conclusion and Related Work . . . . . . . . . . . . . . . . . . 86
3.7.1 Conclusion and Discussion . . . . . . . . . . . . . . . . 86
3.7.2 Related Work . . . . . . . . . . . . . . . . . . . . . . . 91
3.8 Proofs . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 96
3.8.1 Proofs for Section 3.2 . . . . . . . . . . . . . . . . . . 96
3.8.2 Proofs for Section 3.3 . . . . . . . . . . . . . . . . . . 97
3.8.3 Proofs for Section 3.4.1 . . . . . . . . . . . . . . . . . 100
3.8.4 Proofs for Section 3.4.2 . . . . . . . . . . . . . . . . . 113
3.8.5 Proofs for Section 3.5.1 . . . . . . . . . . . . . . . . . 124
3.8.6 Proofs for Section 3.5.2 . . . . . . . . . . . . . . . . . 126
4 Progress in Interaction Systems 131
4.1 Introduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . 131
4.2 Characterizing Progress . . . . . . . . . . . . . . . . . . . . . 131
4.3 Testing Progress . . . . . . . . . . . . . . . . . . . . . . . . . 134
4.3.1 A Graph Criterion . . . . . . . . . . . . . . . . . . . . 135
4.3.2 Enhancing the Graph . . . . . . . . . . . . . . . . . . 144
4.3.3 Failure of the Criterion . . . . . . . . . . . . . . . . . 147
4.4 Example — The Dining Philosophers . . . . . . . . . . . . . . 150
4.5 Conclusion and Related Work . . . . . . . . . . . . . . . . . . 153
4.5.1 Conclusion and Discussion . . . . . . . . . . . . . . . . 153
4.5.2 Related Work . . . . . . . . . . . . . . . . . . . . . . . 154
4.6 Proofs . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 155
4.6.1 Proofs for Section 4.2 . . . . . . . . . . . . . . . . . . 155
4.6.2 Proofs for Section 4.3.2 . . . . . . . . . . . . . . . . . 156
4.6.3 Proofs for Section 4.3.1 . . . . . . . . . . . . . . . . . 166
4.6.4 Proofs for Section 4.3.3 . . . . . . . . . . . . . . . . . 167
5 Robustness of Properties of Interaction Systems 171
5.1 Motivation . . . . . . . . . . . . . . . . . . . . . . . . . . . . 171
5.2 Defining Robustness of a Property . . . . . . . . . . . . . . . 172
5.3 Testing Robustness of Properties . . . . . . . . . . . . . . . . 176