Mitarbeiter
Wintersemester 2015/16
Vorlesung: donnerstags 15:30 Uhr in Hörsaal HS3 (erster Termin 15. Oktober 2015)
Übung: donnerstags 17:00 Uhr in Hörsaal HS3 (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.
Vorlesungsfolien
- FSV_01_Einleitung.pdf
- FSV_02_Math_Grundlagen_1.pdf
- FSV_03_Math_Grundlagen_2.pdf
- FSV_04_Math_Grundlagen_3.pdf
- FSV_05_Algebraische_Spezifikationen_1.pdf
- FSV_06_Algebraische_Spezifikationen_2.pdf
- FSV_07_Modellbasierte_Spezifikationen_1.pdf
- FSV_08_Modellbasierte_Spezifikationen_2.pdf
- FSV_09_Modellbasierte_Spezifikationen_3.pdf
- FSV_10_Modelchecking.pdf
- FSV_11_Modellbasierte_Spezifikationen_4.pdf
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