Formale Verifikation

NUMMER:	n.n.
KÜRZEL:	ForVer
MODULBEAUFTRAGTE:R:	Prof. Dr. Thomas Zeume
DOZENT:IN:	Prof. Dr. Thomas Zeume
FAKULTÄT:	Fakultät für Informatik
SPRACHE:	Englisch
SWS:	4 SWS
CREDITS:	5 CP
ANGEBOTEN IM:	jedes Wintersemester

PRÜFUNGEN

FORM:	schriftlich
TERMIN:	Siehe Prüfungsamt.

LERNFORM

Hörsaalvorlesung mit Medienunterstützung, praktische Übungen am Rechner, zusätzlich Selbststudium durch praktische Projektaufgaben

LERNZIELE

Nach dem erfolgreichen Abschluss des Moduls

- beherrschen die Studierenden die Grundlagen der formalen Verifikation
- verstehen die Studierenden das Konzept der Abstraktion von Daten und Transitionen
- verfügen die Studierenden über Werkzeuge zur Verifikation von Software
- kennen die Studierenden die Model-Checking Verfahren und können sie in praktische Algorithmen umsetzen
- sind die Studierenden in der Lage, die verschiedenen Techniken der formalen Spezifikation und Verifikation von Software zu verstehen und praktisch anzuwenden
- sind sich der Studierenden über die praktischen Relevanz der formalen Verifikation von Software bewusst

INHALT

Es ist eine große Herausforderung an die Informatik, automatische Methoden zur Analyse und Verifikation von Verhaltenseigenschaften für Software-Systeme zu entwickeln. Diese Methoden für die formale Verifikation und Spezifikation von Software ergänzen die traditionelle Softwareentwicklungsmethoden und ersetzen sie sogar teilweise. Die Verfahren, dessen Grundlagen auf Logik und Deduktion basieren, müssen in der Praxis auf die jeweiligen Anwendungen und deren Eigenschaften abgestimmt sein, und zwar sowohl die zur Spezifikation verwendeten Sprachen als auch zur Verifikation verwendeten Kalküle.
Die Vorlesung gibt einen Einblick in das Thema Formale Verifikation und gliedert sich wie folgt:

- Einführung in das Thema Formale Verifikation
- Logik (Aussagelogik, temporale Logik)
- Spezifikationsformalismen
- Systemmodellierung und Algorithmen zur Modellprüfung
- Techniken der Automatisierung der Verifikation

Anwendungen (Verifikation funktionaler Eigenschaften imperative und objekt-orientierter Programme, Verifikation nebenläufiger Programme, Verifikation von Echtzeiteigenschaften, Verifikation der Eigenschaften der Datenstrukturen, Programm- und Protokollverifikation)

VORAUSSETZUNGEN CREDITS

Bestandene Modulabschlussprüfung

EMPFOHLENE VORKENNTNISSE

Inhalte des Pflichtmoduls Software Engineering sowie solides Basiswissen aus den Grundlagenmodulen im Bereich Mathematik und Informatik

LITERATUR

1. F. Nielson, H. Nielson, C. Hankin: „Principles of Program Analysis”, Springer Verlag
2. E. M. Clarke, O. Grumberg, D. Peled: “Model Checking”, MIT Press
3. C. Baier and J.-P. Katoen: ”Principles of Model Checking”, MIT Press

SONSTIGE INFORMATIONEN

Aktuelle Informationen wie Vorlesungstermine, Räume oder aktuelle Dozent*innen und Übungsleiter*innen sind im Vorlesungsverzeichnis der Ruhr-Universität https://vvz.rub.de/ und im eCampus https://www.rub.de/ecampus/ecampus-webclient/ zu finden.