Home | deutsch  | Legals | Sitemap | KIT

Modellprüfung und modellbasiertes Testen (SS 09)

Modellprüfung und modellbasiertes Testen (SS 09)
Type: Seminar
Time:

Blockveranstaltung am Semesterende

Lecturer:

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

SWS: 2
Information:

Der Inhalt der Vorlesung Formale Systeme wird als bekannt vorausgesetzt.

Ausfallsichere Systeme spielen heutzutage eine wichtige Rolle. Ein großer Teil dieser Sicherheit ist auf moderne Modellprüfungsverfahren zurückzuführen, denn damit können frühzeitig Fehler entdeckt bzw. Fehlerfreiheit nachgeweisen werden. Z.B. wurde mit Modellprüfung die Korrektheit des IEEE 1394FireWire root contention Protokolls gewährleistet.

Häufig benötigt Modellprüfung jedoch zu viele Ressourcen wie Laufzeit, Speicher und Expertenwissen. In diesen Fällen wird auf Testverfahren zurückgegriffen, die sich einfacher anwenden lassen. Testen ist aber weniger aufschlussreich, und die Zahl der Testfälle, die für eine erwünschte Konfidenz notwendig wäre, lässt sich mittlerweile bei komplexen Systemen mit klassischen Testverfahren auch nicht mehr handhaben. Modellbasiertes Testen kann jedoch beide Gebiete kombinieren und die jeweiligen Vorteile ausnutzen, um  aufschlussreichere und effizientere automatische Testgenerierung mittels leichtgewichtiger Modellprüfung zu ermöglichen.  

Im Rahmen dieses Seminars sollen Grundlagen moderner Modellprüfverfahren und Ihre Anwendung für modellbasiertes Testen aufgearbeitet werden. Als Tools werden z.B. SPIN, CADP, PRISM, UPPAAL, UPPAAL Tron, Spec Explorer und TorX eingesetzt, deren theoretische Automatenkonzepte ebenalls behandelt werden. Teilweise werden Fallstudien aus dem Bereich von Sensornetzen betrachtet, z.B. das Wireless Local Area Network Protocol IEEE 802.11.

 

Organisatorisches

  • Anmeldung bei Frau Beckert in Raum 321
  • Vorbesprechung am Mi, 29.04.2009, 13:00-14:00 in SR 301
  • Vorbereitungstermin am Mi, 27.05.2009, 11:30-12:00
    • jeder Teilnehmer stellt in ca. 5 min die Gliederung seines Vortrags vor
    • dazu höchstens 5 Folien
  • Abgabe der Ausarbeitung und der Folien bis Mi, 24.06.2009. Für die Ausarbeitung gilt:
  • Vorträge am Mi, 08.07.2009, 9:45-13:45 in SR -109
    • jeweils ca. 45 min + 10 min Diskussion

Vorläufige Themenübersicht

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

 

Modellprüfung:

  • 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.

  • Specification and Analysis of Asynchronous Systems using CADP (FW, DF):
    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.

Modellbasiertes Testen (MBT):

  • Die ioco Theorie (DF):
    Die Artikel [1] und [2] von Jan Tretmans definieren wichtige theoretische Grundlagen für mehrere MBT Werkzeuge, z.B. für TorX und UPPAAL TRON (s.u.): Input/output transition systems (IOTS) und die input/output conformance (ioco) Theorie.
    Beschreibung: Ein IOTS ist ein Labeled Transition System (LTS), wobei die Labels Eingaben, Ausgaben, oder interne Aktionen beschreiben. Die ioco-Relation legt fest, welche Systeme korrekt sind in Bezug auf eine Spezifikation. Die Theorie kann für automatische Testgenerierung benutzt werden, um eine Testsuite aus der Spezifikation herzuleiten, die das System auf ioco-Korrektheit überprüft.

  • 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 (ATG) 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.


  • Das Werkzeug Spec Explorer (DF):
    Artikel zu Spec Explorer
    AsmL-Einführung und Spec#-Einführung
    Beschreibung: Spec Explorer von Microsoft Research ist eine der bekanntesten und mächtigsten ATG-Werkzeuge, welches bei Microsoft industriell eingesetzt wird. Die Spezifikation ist in Spec# oder AsmL beschreiben. Sie ist ausführbar, führt aber wesentlich weiger durch als die Implementierung. Se weist nur die relevanten Zustände des Systems und ihre Korrektheitsbedingungen auf. Testsuites können systematisch erzeugt werden, indem alle möglichen Durchführungspfade des Spezifikationsprogramms mit einem Explizit exploring the possible runs of the specification-program with the help of an explicit-state model checker.

  • Das Werkzeug TorX (DF):
    [26]
    TorX ist ein on-the-fly ATG-Werkzeug und kann auch mit nichtdeteministischen Systemen umgehen. Es basiert auf der ioco Theorie (s.o.) und bietet eine effiziente probabilistische Testgenerierung. Zur Testauswahl bietet Torx Testzwecke, probabilistische Selektion und Heuristiken basierend auf Überdeckungskriterien an. TorX ist durch seine modulare Architektur sehr flexibel: viele seiner Komponenten können ausgetauscht werden.
  • Das Wekzeug UPPAAL Tron (DF):
    [15,16]
    UPPAAL TRON ist ein modellbasiertes Werkzeug für Konformitätstests von Echtzeit-Systemen. Es überprüft on-the-fly, ob bestimmte zeitlich festgelegte Ausführungspfade des Systems spezifiziert sind im System-Modell,
    einem nichtdeterministischen Zeitautomaten-Netzwerk. UPPAAL TRON partitioniert dieses in ein Modell des eigentichen Systems und in ein Modell, welches die Umgebung des Systems beschreibt. Dem Werkzeug sind relativierte timed input/output conformance (rtioco) Relationen zugrunde gelegt.
  • The testing framework TTCN-3 (DF):

Fallstudien:

  • Probabilistic Model Checking of the IEEE 802.11 Wireless Local Area Network Protocol (FW)(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.

Hinweise für gute Seminarvorträge