Mitarbeiter
Wintersemester 2016/17
Vorlesung: mittwochs 9:30 Uhr in Hörsaal HS1 (erster Termin 12. Oktober 2016)
Übung: mittwochs 11: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_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