Formale Methoden der Softwaretechnik
Willkommen auf der Heimatseite der Lehrveranstaltung "Formale Methoden der Softwaretechnik " im Wintersemester 2009/2010!
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).
Generell können formale Methoden in drei Bereichen helfen: bei der Modellierung und Spezifikation, bei Entwurf und Implementation, und bei der Verifikation.
Diese Veranstaltung soll in die nötigen theoretischen Grundlagen einführen, einen Überblick über das Gebiet geben, und die Anwendung an kleineren Beispielen üben. Im übungsbetrieb werden wir auf den interaktiven Theorembeweiser Isabelle zurückgreifen.
Organisatorisches
Die VAK der Veranstaltung ist 03-05-H-604.03.
Termine
- Montags 12-14, MZH 7210
- Mittwochs 12-14, MZH 7220
Scheinkriterien
Vorlesungsfolien
Die Vorlesungsfolien sind jeweils verfügbar als ganzseitiges PDF zum Betrachten, oder als 8:1 Handzettel ohne Effekte zum Drucken:
- Alle Vorlesungen in einer Datei: [Folien] [Handzettel]
- Vorlesung vom 19.10.09: [Folien] [Handzettel]
- Vorlesung vom 26.10.09: [Folien] [Handzettel]
- Vorlesung vom 28.10.08:
- Das ganz einfache Beispiel (VerySimple.thy);
- Aussagenlogik (VSPL.thy) und eine kleine Erweiterung (VSPLTrue.thy).
- Vorlesung vom 02.11.09: [Folien] [Handzettel]
- Vorlesung vom 09.11.09:
- In Isabelle: Prädikatenlogik (VSPred.thy), Beispielbeweis (VSPredEx.thy)
- Vorlesung vom 11.11.09: [Folien] [Handzettel]
- Gleichungslogik (VSPredEq.thy),
- Presburger-Arithmetik (VSPresburger.thy),
- Peano-Arithmetik (VSPeano.thy) mit Beispiel (VSPeanoEx.thy).
- Vorlesung vom 16.11.09: [Folien] [Handzettel]
- Vorlesung vom 23.11.09: [Folien] [Handzettel]
- Vorlesung vom 25.11.09:
- HOL einfach (VSHOL.thy), axiomatische Listen (VSHOLList.thy)
- Vorlesung vom 30.11.09: [Folien] [Handzettel]
- Vorlesung vom 02.12.09: [Folien] [Handzettel]
- Beispiele: MyList.thy
- Vorlesung vom 09.12.09: Trees.thy
- Vorlesung vom 06.01.10: MoreSimplification.thy
- Vorlesung vom 13.01.10: FunEx.thy
Übungsblätter
Hier finden sich die Übungsblätter zur Veranstaltung.
- 1. Übungsblatt (1. Teil), ausgegeben am 28.10.09, abzugeben am 11.11.09.
- 1. Übungsblatt (2. Teil), ausgegeben am 11.11.09, abzugeben am 25.11.09.
- 1. Übungsblatt (3. Teil), ausgegeben am 25.11.09, abzugeben am 09.12.09.
- 2. Übungsblatt, ausgegeben am 09.12.09, abzugeben am 13.01.10.
- 3. Übungsblatt, ausgegeben am 13.01.10, abzugeben am 27.01.10.
Literatur und Links
- Buchempfehlung: Dirk van Dalen, Logic and Structure. Springer Verlag, vierte Auflage, 2004.
- Mehr über die Softwarefehler im Therac-25. Sehr lesenswerter Artikel!
Links zu Isabelle
- Die Isabelle Heimatseite.
- Die Heimatseite von Proof General, der Emacs-basierten Benutzerschnittstelle.
- Übersicht über die Theorien in Isabelle/HOL.
- Handbücher: das Tutorial, das HOL-Handbuch, das Systemhandbuch.