Home | deutsch  | Legals | Sitemap | KIT

Formale Modellierung in Sensornetzen (SS 08)

Formale Modellierung in Sensornetzen (SS 08)
Type: Seminar
Lecturer:

Prof. P. H. Schmitt
Frank Werner
David Faragó

SWS: 2

Ausfallsichere Systeme spielen heutzutage in vielen technischen Bereichen eine wichtige Rolle. Einen großen Teil dieser Sicherheit ist auf moderne Modellprüfungsverfahren urü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 Modellprüfverfahren und Ihre Anwendungsmöglichkeiten im Bereich von Sensornetzen aufgearbeitet werden. Als Tools werden SPIN, CADP, 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 zu analysieren.

 

Bemerkung: Der Inhalt der Vorlesung Formale Systeme wird als bekannt vorausgesetzt.

Seminarvorträge am 8./9. Juli 2008

Uhrzeit   Vortrag Ort
Dienstag, 08. Juli 2008
09:45   [Sem:FSE] Philipp Glaser: Daikon   SR 131
10:45   [Sem:FSE] Saoussen Arfaoui: Non-null Types in an Object-Oriented Language   SR 131
11:45-12:45   [Sem:FSE] Sebastian Maisch: Perc Pico   SR 131
14:00   [Sem:FSE] Michael Ziller: Pex (Program EXploration)   SR 131
15:00   [Sem:FSE] Simon Roth: Compilerverifikation   SR 131
16:00   [Sem:FSE] Martin Küster: Towards Verified Model Transformations   SR 131
Mittwoch, 09. Juli 2008
09:45   [Sem:FSE] Daniel Bruns: Interactive Verification of Statecharts   SR -109
10:45   [Sem:FSE] Rolf Haynberg: Model Checking Dynamic and Hierarchical UML State Machines   SR -109
11:45-12:45   [Sem:FMSens] J.P. Tsague: Automated Test Generation using the Simbolic Analysis Laboratory (SAL)   SR -109
14:00   [Sem:SAT] Markus Iser: Visualisierung der Struktur von SAT-Instanzen mittels Graph-Layout   SR -109
14:50   [Sem:SAT] Simon Roth: Software Verifikation: Abstraction Refinement   SR -109
15:40       [Sem:SAT] Jan Rochel: Tree Decomposition für SAT   SR -109

Organisatorisches

  • Vorbereitungstermin am Di, 20.05.2008, 11:30-13:00 in SR 131
    • jeder Teilnehmer stellt in ca. 5 min die Gliederung seines Vortrags vor
    • dazu höchstens 5 Folien
  • Abgabe der Ausarbeitung bis Di, 24.06.2008
    • 5-10 Seiten
    • mit LaTeX erstellt
  • Vorträge am Di, 08.07.2008 (ganztags) und Mi, 09.07.2008 (vormittags)
    • jeweils ca. 45 min + 15 min Diskussion

Hinweise für gute Seminarvorträge

Vorläufige Themenübersicht

Es stehen folgende Themen zur Auswahl. Für weitere Fragen richten Sie sich bitte an den entsprechenden Seminarbetreuer.

 

  • Fallstudie (FW):
    Probabilistic Model Checking of the IEEE 802.11 Wireless Local Area Network Protocol (PDF, HTML)
    Beschreibung: Diese Fallstudie untersucht probabilistische Modellprüfverfahren und Modellierungen von eigenschaften des IEEE802.11 Wireless LAN Standarts. Es wird ein 2-Wege Handshake Machanismus des 802.11 MAC (Medium Access Control) Entwurfs für eine fest vorgegebene Topologie modelliert.
  • Model Checking of Randomized Leader Election Algorithms (DF):
    Simplifying Itai-Rodeh leader election for anonymous rings, Fokkink and Pang
    (weitere Papiere: Symmetry breaking in distributed networks, Itai and Rodeh;
    Model Checking of Randomized Leader Election Algorithms, David Farago)
    Beschreibung: Untersucht wird der probabilistische Modellprüfer PRISM, der randomisierte Algorithmen modellieren, verifizieren und Statistiken über sie berechnen kann. Dies wird mit randomisierten Leader Election Algorithmen als Fallstudie gemacht. Solche Algorithmen lösen das Problem, verteilt einen eindeutigen Knoten in einem anonymen Ring auszuwählen.
  • Specification and Analysis of Asynchronous Systems using CADP (FW):
    Modeling and Verification of Real-Time Systems ,
    Stephan Metz and Nicolad Navet, page 141-166
    Beschreibung: Der Beitrag beschäftigt sich mit der CADP Toolbox zur Analyse asynchroner Systeme und bietet hier divere Untersuchungsmöglichkeiten. Hierzu zählen Spezifikation, Simulation, Rapid Prototyping, Verifikation und Test Generierung.
  • Verification of Probabilistic Systems, Methods and Tools (FW):
    Modeling and Verification of Real-Time Systems ,
    Stephan Metz and Nicolad Navet, page 289-315
    Beschreibung: Im Fokus dieser Arbeit liegt in der Verifikation probabilistischer Systeme und Modelle. Die Bevorzugten Modellierungen sind Markov Ketten (MC), Markov Decision Prozesse (MDP), und stochatstische Modelle, die durch Werkzeuge wie z.B. ETMCC (Erlangen-Twente Markov Chain Model Checker) und Prism.

  • Symmetry Reduction for PRISM (FW oder DF):
    Symmetry Reduction for Probabilistic Model Checking, Kwiatkowska et al.
    (freiwilliges Papier mit anderem Reduktionsalgorithmus: Symmetry Reduction for Probabilistic Model Checking using Generic Representatives, Donaldson and Miller)
    Beschreibung: Durch Ausnutzung von Symmetrie kann die Größe eines Modelles reduziert werden. Da Netzwerke häufig Symmetrien aufweisen, lohnt sich diese herausfordernde Aufgabe. Untersucht werden Reduktionen von Transitionssystemen für den Modellprüfer PRISM.

  • Testing within the Model-Based Design Process (DF):
    Requirements-Based Testing in Aircraft Control Design, Jason Ghidella and Pieter J. Mosterman
    (User's guides: Simulink Stateflow, Simulink Verification and Validation)
    Beschreibung: Modellbasierter Entwurf wird immer mehr verschränkt mit dem Erfassen von Anforderungen und den Phasen des Testens. Die angegebene Fallstudie modelliert ein Flugzeugkontrollsystem als einen endlichen Automaten mit Simulink Stateflow und handhabt die Anforderungen und Tests mit Simulink Verification & Validation und mit Abdeckungskriterien.

  • Automated Test Generation using the Symbolic Analysis Laboratory (SAL) (DF):
    Automated Test Generation with SAL, Grégoire Hamon, Leonardo de Moura and John Rushby
    (Handbücher: The SAL Language Manual, basic SAL tutorial)
    Beschreibung: Es werden Spezifikationen in Simulink Stateflow angegeben, die in SAL Spezifikationen übersetzt werden, welche angereichert sind mit strukturellen Abdeckungskriterien. Das Werkzeug SAL-atg generiert dann daraus automatisch Tests indem es Modellprüfer der SAL nutzt.

  • The UML Testing Profile (UTP) (DF):
    UTP-Spezifikation vom 05.05.07
    (freiwillige Fallstudie: From Design to Test with UML - Applied to a Roaming Algorithm for Bluetooth Devices;
      Model Driven Testing Using the UML Testing Profile (nur Amazon-Link))
    Beschreibung: UTP ist eine Testmodellierungssprache der OMG um Testsysteme zu entwerfen, visualisieren, spezifizieren, analysieren, konstruieren und zu dokumentieren - kurz: zum UML-basierten modellgetriebenen Testen.
    Die freiwillige Fallstudie modifiziert und erweitert ein gegebenes UML-Modell eines Roaming-Algorithmus für Bluetooth-Geräte, so dass auch die Aspekte des Testens in das Modell integriert werden.

  • Coverage criteria for model-based testing (DF):
    Evaluating Coverage Based Testing, Christophe Gaston and Dirk Seifert
    (freiwillige Fallstudie: Abdeckungskriterien in der modellbasierten Testfallgenerierung, Mario Friske und Bernd-Holger Schlingloff)
    Beschreibung: Die Anwendung von Abdeckungskriterien auf der Modellebene sowie ihre Komplementierung durch probabilistisches Testen werden mit Hilfe von Übereinstimmungsrelationen untersucht.
    Das freiwilliges Fallbeispiel einer in UML modellierten Sitzsteuerung zeigt, dass MC/DC für modellbasiertes Blackbox-Testing in manchen Situationen keinen zufriedenstellenden Abdeckungsgrad bietet, und risiko- und szenariogesteuerte Direktiven als Metastrategie die automatische Testfallgenerierung verbessert.