Home | deutsch  | Legals | Sitemap | KIT

Theorie und Anwendung von Model Checking (SS 07)

Theorie und Anwendung von Model Checking (SS 07)
Type: Seminar
Place: SR -108
Time:

13.7.2007, 9:00 - 13:00

Lecturer:

Prof. P. H. Schmitt
Frank Werner

SWS: 2

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.