Ausfallsichere Systeme spielen heutzutage in vielen technischen Bereichen eine wichtige Rolle. Einen großen Teil dieser Sicherheit ist auf moderne Modellprüfungsverfahren zurückzuführen. Durch die Anwendung von Model Checking konnten insbesondere in der Vergangenheit viele Fehler frühzeitig - wie z.B. im IEEE 1394 FireWire root contention Protokolls - entdeckt werden um so die Korrektheit zu gewährleisten.
Im Rahmen dieses Seminars sollen Grundlagen moderner Model Checking Tools aufgearbeitet werden. Als Tools werden SPIN, PRISM und UPPAAL eingesetzt, deren theoretische Automatenkonzepte behandelt werden und in Fallstudien dazu benutzt werden z.B. das Wireless Local Area Network Protocol IEEE 802.11 auf probabilistischem Weg zu analysieren.
Voraussichtlich werden Themen zu den folgenden Werkzeugen oder Forschungsgebieten angeboten:
- (PHS) Grundlagen: Model Checking
Daniel Bruns
A Logic for Reasoning about Time and Reliability - (FW) SPIN Fallstudie: Model Checking of the non-deterministic Leader Election algorithm
An O(n log n) Unidirectional Distributed Algorithm for Extrema Finding in a Circle
- (PHS) UPPAAL Theorie:
Markus Kuderer
Timed Automata - Semantics, Algorithms, and Tools - (FW) UPPAAL Einführung: Das Uppaal Tool
Christoph Scheben
- (PHS) PRISM: Theorie probabilistischer Modellprüfung
Jonida Saqe
CRM Monograph Series, Mathematical Techniques for Analyzing Concurrent and Probabilistic Systems, J. J. M. M. Rutten, M. Kwiatkowska, G. Norman, D. Parker, Chapter 2, page 101 - 115 - (FW) UPPAAL Fallstudie:
Probabilistic Model Checking of the IEEE 802.11 Wireless Local Area Network Protocol - (FW) PRISM Fallstudie:
Probabilistic Model Checking of the IEEE 802.11 Wireless Local Area Network Protocol
Termine und Organisatorisches
Die Vorträge finden am 12./13. Juli statt.
Bemerkung: Der Inhalt der Vorlesung Formale Systeme wird als bekannt vorausgesetzt.
