Verifikation reaktiver Systeme

Nächste Vorlesung: 07. April 2009
Nächste Übung: 09. April 2009
Vorlesungsmaterial vom 31.3. eingestellt

Vorlesung: Di. 13:15 - 14:45 Uhr
Übung: Do. 09.45 - 11.15 Uhr
Raum: IZ 358
Erster Termin: 31.03.2009

Dozentin: Dr. Michaela Huhn

LV-Nr Vorlesung: INF-PRS-018
LV-Nr Übung: INF-PRS-011

Art der Veranstaltung: Vorlesung
Stundenzahl: 2+2
Leistungspunkte: 5

Hörerkreis: Studenten und Studentinnen der Informatik, Wirtschaftsinformatik und Informationssystemtechnik im Master, oder fortgeschrittenen Bachelorstudium
Voraussetzungen: Grundlegende Kenntnisse in Informatik
Scheinerwerb: nach Absprache

Inhalt: Eingebettete Hardware-Controller und Telekommunikationsprotokolle sind Beispiele für Systeme, die kontinuierlich mit der Umgebung interagieren und daher als reaktive Systeme bezeichnet werden. Um die steigende Komplexität in den Griff zu bekommen, wird heute zunehmend formale Verifikation beim Entwurf reaktiver Systeme und Komponenten eingesetzt: Durch Bilden eines mathematischen Modells und mathematischen Beweisen über seine Eigenschaften wird versucht, Fehler systematisch schon in frühen Entwurfsphasen zu finden. Die Vorlesung vermittelt einen Überblick über Methoden und Werkzeuge zur automatischen Verifikation: Zur Modellierung des Systemverhaltens werden Transitionssysteme und Automatenmodelle eingeführt. Dann betrachten wir anhand der Verifikation von Invarianten grundlegende Algortihmen und Heuristiken zur Effizienzverbesserung. Mit Temporallogiken und Omega-Automaten werden komplexere Spezifikationen ermöglicht. Die Verifikationsalgorithmen werden zum sogenannten Modelchecking erweitert. Gegen Ende werden wir hoffentlich noch neuere Ansätze wie Abstraktionstechniken zur Verifikation großer Systeme behandeln. In den Übungen sollen die Teilnehmer kleine Beispiele mit Werkzeugen ( SPIN, SMV) verifizieren.

Formales: Für diese Vorlesung wird eine Übung angeboten.

Terminplanung (vorläufig):

Dienstag 13:15 - 14:45 vermutl. Donnerstag 9:45 - 11:15

Di, 31.03.09

Di, 07.04.09 Do, 09.04.09

Do, 16.04.09

Di, 21.04.09

Di, 28.04.09 Do, 30.04.09

Di, 05.05.08 Do, 07.05.08

Di, 12.05.09 Do, 14.05.09

Di, 19.05.09 (Übung)

Di, 26.05.09 Do, 28.05.09

Di, 09.06.09 Do, 11.06.09

Mi, 16.06.09 Do, 18.06.09

Di, 23.06.09 Do, 25.06.09

Di, 30.06.09 Do, 02.07.09

Di, 07.07.09 Do, 09.07.09

(Stand: 31.03.09)

Folien (Sie müssen sich einloggen.):

Einführung:

Folien der Vorlesung

Folienskript

Literatur: Die Vorlesung orientiert sich an verschiedenen Lehrbüchern. Weitere Literaturempfehlungen werden in der Vorlesung angegeben.
< Grundlegende Literatur:

Gerard Holzmann: The SPIN Model Checker, Addison Wesley, 2003
Doron Peled: Software Reliability Methods

Literatur: Die Vorlesung orientiert sich an verschiedenen Lehrbüchern. Weitere Literaturempfehlungen werden in der Vorlesung angegeben.
< Grundlegende Literatur:

Gerard Holzmann: The SPIN Model Checker, Addison Wesley, 2003
Doron Peled: Software Reliability Methods

Lassen Sie sich von uns regelmäßig über neue Lehrveranstaltungen undStudien-/Diplomarbeiten informieren: