Formale Verifikation

Sie befinden sich hier:

Kürzel

VorFer

Modulnummer

n.n.

Leistungspunkte (Credits)

5 CP

Workload

150 Stunden

Semesterwochenstunden

4 SWS

Turnus

jedes Wintersemester

Unterrichtssprache

Englisch

Aktuelle Informationen wie Vorlesungstermine, Räume oder aktuelle Dozent*innen und Übungsleiter*innen

 

Lehrveranstaltungen

  • Formale Verifikation – Vorlesung (2 SWS)
  • Formale Verifikation – Übung (2 SWS)

Modulbeauftragte/r, aktuelle Dozent*innen und Übungsleiter*innen
Inhaber*in der Professur „Logik und Formale Verifikation“ (in Besetzung)
Empfohlene Vorkenntnisse
Inhalte des Pflichtmoduls Software Engineering sowie solides Basiswissen aus den Grundlagenmodulen im Bereich Mathematik und Informatik
Teilnahmevoraussetzungen
keine
Lernziele (Lerning Outcomes)
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)

Lernformen
Hörsaalvorlesung mit Medienunterstützung, praktische Übungen am Rechner, zusätzlich Selbststudium durch praktische Projektaufgaben
Prüfungsformen
Schriftliche Modulabschlussprüfung über 120 Minuten
Vorraussetzung für die Vergabe von Kreditpunkten
Bestandene Modulabschlussprüfung
Empfohlene 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