[03-604.04] Formale Methoden der Softwaretechnik

Willkommen auf der Heimatseite der Lehrveranstaltung "Formale Methoden der Softwaretechnik " im Wintersemester 2005/2006!

Inhaltliches

Inhalt der Veranstaltung sind sogenannte Formale Methoden. Hierunter versteht man ganz allgemein Methoden, die Korrektheit von Software mit mathemathischen Mitteln (meist formaler Logik) sicherstellt. Als formale Methoden im engeren Sinne (und im Sinne dieser Veranstaltung) zählen alle Methoden, die auch eine wohldefinierte mathematische Fundierung haben, also zählt zum Beispiel die UML nicht dazu.

Formale Methoden werden je wichtiger, je mehr sicherheitskritische Funktionen in Software (anstatt in Hardware) implementiert werden. In immer mehr Situationen sind Softwarefehler inakzeptabel, und wir müssen die Sicherheit der Software mit anderen Mitteln sicherstellen als code review ("scharf hingucken") oder testen (durch Tests alleine läßt sich nie die Fehlerfreiheit sicherstellen).

Diese Veranstaltung soll in die nötigen theoretischen Grundlagen einführen, einen Überblick über das Gebiet geben, und die Anwendung an kleineren Beispielen (aus dem Bereich der Robotik und des Automobilbaus) üben, so dass Teilnehmer formale Methoden in zukünftigen Projekten selber einsetzen können.

Themen

In der Vorlesung werden folgende Themen behandelt:

Theoretische Grundlagen
Modellbasierte Spezfikation in Z
Axiomatische Spezifikation in CASL
Grundlagen der Programmverifikation
Entwicklung durch Verfeinerung

Im übungsbetrieb werden wir auf Z und den interaktiven Theorembeweiser Isabelle zurückgreifen.

Organisatorisches

VAK: 03-604.04.
Kategorie: A (ECTS: 6)
Modulbereich: Theorie

Termine:

Vorlesung: Mo 15:00 -- 17:00, MZH 7260
Übungen: Do 09:00 -- 10:00 MZH 8090 oder Do 10:00 -- 11:00, MZH 8090
Achtung, Raumänderung: ab dem 03.11.05 jetzt im MZ 8090!
Veranstaltungsbeginn (erste Vorlesung): Mo 24.10 15:00

Achtung: Wegen starker inhaltlicher Überschneidungen kann dieses Modul nicht gleichzeitig mit dem Modul "Techniken zur Entwicklung korrekter Software I" angerechnet werden.

Vorlesungsfolien

Alle Folien im Überblick: [PDF] (Fassung vom 30.01.06; wird ständig aktualisiert).
Handouts pro Vorlesung (PostScript schwarz-weiß, 8 Folien auf einer Seite, zum Ausdrucken):
- [1] vom 24.10.05.
- [2] vom 31.10.05.
- [3] vom 07.11.05.
- [4] vom 14.11.05.
- [5] vom 21.11.05.
- [6] vom 24.11.05.
- [7] vom 05.12.05.
- [8] und [Anhang] vom 12.12.05.
- [9] vom 09.01.06
- [10] vom 16.01.06
- [11] vom 23.01.06
- [12] vom 30.01.06
- [13] vom 06.02.06
Weiteres Material:
- Mehr über die Softwarefehler im Therac-25. Sehr lesenswerter Artikel!
- Buchempfehlung: Dirk van Dalen, Logic and Structure. Springer Verlag, vierte Auflage, 2004.
- Die Beispielbeweise aus der Übung vom 10.11.05.
- Die Induktionsbeweise aus der Übung vom 17.11.05.
- Das Mergesort-Beispiel aus der Übung vom 08.12.05 ist Teil der Isabelle-Distribution und findet sich hier oder in $ISABELLE_HOME/src/HOL/ex/MergeSort.thy.
Zu der Spezifikationssprache Z:
- Buchempfehlung: Jonathan Jacky, The Way of Z. Cambridge University Press, 1997.
- Zweite Buchempfehlung: Jim Woodcock, Jim Davies, Using Z. Prentice-Hall, 1996. Online-Version hier.
- Die Referenz: J.M. Spivey, The Z notation. A reference manual. Prentice-Hall, 1992. Online-Version hier.
- Mehr Infos und Links im Eintrag über Z in der Virtuellen Bücherei für Formale Methoden.
- Für Z in LaTeX: oz.sty mit Anleitung.

Übungsblätter

[1] vom 03.11.05 (Version 1.3). Dazu: die Theory MyList.thy
[2] vom 17.11.05 (Version 1.0).
[3] vom 01.12.05 (Version 1.2). Dazu: die Theory OrderedList.thy
[4] vom 12.01.06 (Version 1.1). Dazu:
- Das Auto in Haskell hsRacer.tgz (Version 0.4 vom 06.02.06).
- Die Theorie Vec2.thy.
[5] (Zusatzübungsblatt) vom 03.03.06 (Version 1.0).