Reachability analysis of fault tolerant protocols [Elektronische Ressource] / vorgelegt von Sabine Böhm

Sujets

• Informatik

Informations

• Publié par: universitat_duisburg-essen
• Publié le: 01 janvier 2007
• Nombre de lectures: 41
• Langue: Deutsch

Extrait

Reachability Analysis of Fault-Tolerant
Protocols
Dissertation
zur Erlangung des akademischen Grades eines
Doktors der Naturwissenschaften
(Dr. rer. nat.)
durch den Fachbereich Wirtschaftswissenschaften der
Universitat Duisburg-Essen
Campus Essen
Vorgelegt von
Dipl.-Inform. Sabine Bohm
aus Bochum
Essen 2007Tag der mundlichen Prufung: 27.04.2007
Erstgutachter: Prof. Dr. Klaus Echtle
Zweitgutachter: Prof. Dr. Bruno Muller-Clostermann
iiDanksagung
Die vorliegende Arbeit entstand wahrend meiner Tatigkeit als wissenschaftliche Mitarbeiterin
der Forschungsgruppe Verlasslichkeit von Rechensystemen der Universitat Duisburg-Essen am
Campus Essen. Mein Dank gilt allen ohne die diese Arbeit nicht denkbar gewesen ware fur ihre
ganz personlic he Art und Weise der Unterstutzung:
Alex, Andre, Andre, Andreas, Anna, Anne, Arzu, Barbel, Bruno, Carsten, Cathrin, Charlotte,
Christian, Christina, Christoph, Christoph, Claudia, Conny, Daniela, Dominik, Dominik, Elisa-
beth, Eva, Frank, Frank, Frau Becker, Frau Beckmann, Frau Dusenberg, Frau Gotze, Freimut,
Gottfried, Gregor, Gudrun, Huly a, Hans, Heike, Heike, Helmut, Henrik, Herr Griebsch, Ingo,
Irene, Jan, Jana, Jens, Johannes, Johannes, Jutta, Katja, Klaus, Kribbel, Leoni, Lili, Magdalena,
Manuela, Manuela, Marc, Mario, Markus, Markus, Mohamed, Rainer, Ralf, Rose, Sascha, Se-
bastian, Silke, Simone, Sonja, Stefan, Stefan, Ste , Sven, Tanja, Tanja, Tanja, Tanja, Tara,
Thorsten, Tobias, Uli, Ulrike, Ulrike, Veronika, Werner, Wolfgang, Wolfgang.
Explizit bedanken moc hte ich mich bei Prof. Dr. Echtle fur spannende Diskussionen und seine
Unterstutzung in allen Phasen dieser Arbeit. Weiterhin danke ich Prof. Dr. Muller-Clostermann
fur seine konstruktiven Beitrage und seine Bereitschaft das Zweitgutachten zu erstellen.
vviKurzfassung
Durch die zunehmenden Anforderungen an fehlertolerante Protokolle steigt auch deren Komplexitat zuse-
hends. Dadurch ist es deutlich schwieriger die Funktionalitat der Fehlertoleranzmechanismen zu ub er-
prufen. In dieser Arbeit wird ein modellbasierter Ansatz vorgestellt, dessen Ziel es ist \Luc ken" in den
Fehlertoleranzeigenschaften e zien t zu nden. Dazu wird ein Algorithmus entwickelt, der eine partiellen
Ordnung erzeugt und es somit erlaubt den Zustandsraum zu verkleinern ohne Verhalten bezuglic h der
zu prufenden Eigenschaften zu verlieren. Weiterhin werden zwei Algorithmen zur (partiellen) Analyse
entworfen, implementiert und bewertet: Der H-RAFT Algorithmus basiert auf den SDL-Elementen der
jeweiligen Transitionen und erfordert keinerlei weiteres Domanen-Wissen des Benutzers. Der Close-to-
Failure Algorithmus hingegen ist nur von Benutzerinformationen abhangig. Kombinationen der beiden
Ansatze werden ebenfalls untersucht. Fur alle vorgestellten Methoden und Algorithmen wird ausgenutzt,
dass es sich um fehlertolerante Protokolle handelt. Um die neuen Ansatze mit weitverbreiteten Al-
gorithmen vergleichen zu konnen wird ein Werkzeug entwickelt, welches eine einfache Integration von
Algorithmen ermoglicht. Die vorgestellten Techniken werden ausfuhrlich in Experimenten mit einem
Gesamtaufwand von etlichen CPU-Monaten untersucht. Die Ergebnisse dieser Exptreihen zeigen
eindeutig die Vorteile der entwickelten Algorithmen und Methoden.
Abstract
Due to the increasing requirements imposed on fault-tolerant protocols, their complexity is steadily
growing. Thus veri cation of the functionality of the fault-tolerance mechanisms is also more di cult
to accomplish. In this thesis a model-based approach towards e cien tly nding \loopholes" in the fault-
tolerance properties of large protocols is provided. The contributions comprise thinning out the state
space without missing behavior with respect to the validation goal through a partial ordering strategy
based on single fault regions. Two algorithms for (partial) analysis are designed, implemented and
evaluated: the H-RAFT algorithm is based on SDL elements constituting each transition and requires
no user-knowledge. The Close-to-Failure algorithm on the other hand is purely based on user-provided
information. Combination of the two algorithms is also investigated. All contributions exploit the fault-
tolerant nature of the protocols. In order to compare the performances of the novel techniques to well-
known algorithms, a tool has been developed to allow for easy integration of di eren t algorithms. All
contributions are thoroughly investigated through experiments summing up to several CPU-month. The
results show unambiguously the advantages of the developed methods and algorithms.
viiContents
I. Introduction 1
1. Introduction 3
1.1. Motivation and Goal of the Thesis . . . . . . . . . . . . . . . . . . . . . . . . . . 3
1.2. Scienti c Background and Related Work . . . . . . . . . . . . . . . . . . . . . . . 6
1.2.1. Related Tools . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 7
1.2.2. Scienti c Work . . . . . . . . . . . . . . . . . . . . . . . . . . . . 8
1.3. Organization of the Thesis . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 9
2. SDL 11
2.1. Introduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 11
2.2. Hierarchy . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 11
2.3. SDL Processes . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 15
2.3.1. Process Overview . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 15
2.3.2. Input Elements . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 17
2.3.3. Actionts . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 19
2.4. Concept of Time in SDL . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 21
3. Reachability Analysis 23
3.1. Introduction to Reachability Analysis . . . . . . . . . . . . . . . . . . . . . . . . 23
3.1.1. Application Areas . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 27
3.2. General Reachability Analysis Algorithms . . . . . . . . . . . . . . . . . . . . . . 28
3.2.1. Exhaustive Exploration . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
3.2.2. Random Walk . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
3.2.3. Bitstate Exploration . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
II. Algorithms 31
4. Motivation and Introduction 33
5. State Space Reduction Techniques 37
5.1. Single Fault Region Partial Ordering . . . . . . . . . . . . . . . . . . . . . . . . . 37
5.1.1. State Space Reduction Based on Single Fault Regions . . . . . . . . . . . 37
5.1.2. Solutions for SDL . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41
5.1.3. Time Progress in State Space Analysis of SDL Models . . . . . . . . . . . 47
5.2. Start Transitions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52
ixContents
5.3. Speci cation of Special Processes . . . . . . . . . . . . . . . . . . . . . . . . . . . 53
5.4. Summary . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 54
6. H-RAFT 55
6.1. Introduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 55
6.2. Global State Selection . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 57
6.3. Transition . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 63
6.3.1. Input Weights . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 64
6.3.2. Action Weights . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 68
6.3.3. Transition Weight Composition . . . . . . . . . . . . . . . . . . . . . . . . 70
6.4. Summary . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 73
7. Close-to-Failure 75
7.1. Criteria De nition . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 75
7.2. Variants . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 78
7.2.1. C2F . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 78PART F
7.2.2. C2F . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 78PRED
7.3. Combination with H-RAFT . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 79
7.4. Summary . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 80
III. Tool 81
8. RAFT 83
8.1. Introduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 83
8.2. Features of RAFT . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 84
8.2.1. Implemented Algorithms . . . . . . . . . . . . . . . . . . . . . . . . . . . . 85
8.2.2. Partial Order Reduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . 86
8.2.3. Global State De nition and Timing . . . . . . . . . . . . . . . . . . . . . 86
8.2.4. Special Transitions and Processes . . . . . . . . . . . . . . . . . . . . . . . 86
8.2.5. Rule and Criteria De nition . . . . . . . . . . . . . . . . . . . . . . . . . . 87
8.3. Usage of RAFT . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 88
8.3.1. RAFT-Parser . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 88
8.3.2. RAFT Parameter Class . . . . . . . . . . . . . . . . . . . . . . . . . . . . 91
IV. Analysis 93
9. Introduction and Goal of the Analysis 95
10.Modeled Protocols 97
10.1. Pendulum Protocol . . . . . . . .