Wintersemester 2017/18

Vorlesung: donnerstags 9:30 Uhr in Hörsaal HS3 (erster Termin 19. Oktober 2017)

Übung: donnerstags 11:00 Uhr (nach Absprache)

Formale Spezifikation und Verifikation (Master Informatik)

Klassisches Software-Engineering setzt umgangssprachliche und informelle Notationsformen ein, um die Anforderungen an die zu erstellende Software und die während der Entwicklung getroffenen Entscheidungen zu beschreiben. Dies birgt die Gefahr von Mehrdeutigkeiten oder Widersprüchlichkeiten, die zu Softwarefehlern führen können. Je nach Art des jeweiligen Systems können dabei auch schwere Schäden (Verlust von Menschenleben oder hoher wirtschaftlicher Verlust) entstehen.

Diese Schwierigkeit kann durch Formale Spezifikation und Verifikation vermieden werden, indem man mathematisch präzise und damit unmissverständliche Beschreibungen - Formale Spezifikationen - anfertigt und Eigenschaften des damit beschriebenen Systems mathematisch beweist (Verifikation).

Formale Spezifikation und Verifikation versteht sich dabei als zusätzliche Technik zur Qualitätssicherung die neben den etablierten Qualitätssicherungsverfahren, etwa dem systematischen Test von Software, zum Einsatz kommen soll.

Die Vorlesung richtet sich an Studierende im Master-Studiengang Informatik. Sie widmet sich den typischen Techniken zur formalen Spezifikation und zur Verifikation.

Literatur

Vorlesungen über Informatik Band 1 - Grundlagen und funktionales Programmieren,
Gerhard Goos, Springer Verlag, Heidelberg, 2005

Logik für Informatiker,
Uwe Schöning, Spektrum Akademischer Verlag, Heidelberg, 2000

Software Engineering 1,
Dines Bjørner, Springer, Heidelberg, 2006

Algebraische Spezifikation abstrakter Datentypen,
Ehrich/Gogolla/Lipeck, Teubner, Stuttgart, 1989

Z - An Introduction to Formal Methods,
Antoni Diller Wiley & Sons, New York, 1994

Software Development with Z,
J.B. Wordsworth, Addison-Wesley, New York, 1992