20-00-0901-iv Formale Methoden im Softwareentwurf

Lehrende: Prof. Ph.D. Sebastian Faust

Veranstaltungsart: Integrierte Veranstaltung

Orga-Einheit: FB20 Informatik

Anzeige im Stundenplan: FormMeth SWentwurf

Fach:

Anrechenbar für:

Semesterwochenstunden: 3

Unterrichtssprache: Deutsch

Min. | Max. Teilnehmerzahl: - | -

Digitale Lehre:
https://moodle.informatik.tu-darmstadt.de/course/view.php?id=1054

Lehrinhalte:
- Modellierung nebenläufiger Software mit der Sprache ProMeLa
- Formalisierung von Sicherheits- und Lebendigkeitseigenschaften mit temporaler Aussagenlogik
- Theoretische Grundlagen von Modellprüfungsverfahren
- Verifikation von ProMeLa Programmen mittels des Modellprüfers SPIN
- Syntax, Semantik und Sequenzenkalkül für typisierte Logik erster Stufe
- Grundlagen der kontraktbasierten Softwarespezifikationssprache JML
- Dynamische Logik als eine Programmlogik erster Stufe
- Formale Programmverifikation durch symbolische Ausführung und Invariantenschließen
- Werkzeugunterstützte Verifikation von Java-Programen mit der KeY System

Literatur:
Für den ersten Teil des Kurses:
- Ben-Ari: Principles of the SPIN Model Checker, Springer
- Holzmann: The SPIN Model Checker, Addison-Wesley

Für den zweiten Teil des Kurses:
- Beckert et al.: Verification of Object-Oriented Software, Springer

Die Literaturempfehlungen werden kontinuierlich aktualisiert.

Voraussetzungen:
Empfohlen:
Programmierkenntnisse in Java und Vertrautheit mit Aussagenlogik wird erwartet.
Empfohlen ist der Besuch der Vorlesung “Aussagen- und Prädikatenlogik”.
Ansonsten genügt grundlegende mathematische Reife.