Formale Methoden der Softwaretechnik
Willkommen auf der Heimatseite der Lehrveranstaltung „Formale Methoden der Softwaretechnik“ im Sommersemester 2011. Auf dieser Seite finden sich:
Inhaltliches
Inhalt der Veranstaltung sind sogennannte Formale Methoden. Hierunter versteht man ganz allgemein Methoden, die Korrektheit von Software mit mathemathischen Mitteln (meist formaler Logik) sicherstellt. Formale Methoden werden immer wichtiger, weil immer mehr sicherheitskritische Funktionen in Software implementiert werden, und in immer mehr Situationen Softwarefehler inakzeptabel sind; hier besteht ein großer Bedarf. Gleichzeitig erfordert der Einsatz formaler Methoden auch eine gewisse Kenntniss der mathematischen Hintergründe, die weit über übliche Programmierkenntnisse hinausgeht, und die in dieser Veranstaltung vermittelt werden.
In der Veranstaltung werden wir verschiedene Logiken (Aussagenlogik, Prädikatenlogik erster und höhere Stufe) kennenlernen. Wir werden sehen, wie wir in diesen Logiken Korrektheitsaussagen (und welche) ausdrücken können, und werden Werkzeuge kennenlernen, die mit diesen Logiken arbeiten (SAT-Solver, automatische und interaktive Beweiser, SMT-Solver), und lernen, diese Werkzeuge sinnvoll einzusetzen, um korrekte Software zu entwickeln.
Die Ziele dieser Veranstaltung sind
- vertiefte Kenntnisse in der Methodik formaler (d.h. logikbasierter) Spezifikation und Verifikation von Systemen,
- Verständnis der dafür verwendeten Beweis- und Analyseverfahren, insbesondere formaler Kalküle und ihrer Algorithmen,
- die Verwendung formaler Modellierungs- und Verifikationswerkzeuge,
- und die Fähigkeit zur Auswahl geeigneter Werkzeuge und Verfahren für praktische Fragestellungen.
Organisatorisches
Kenndaten: VAK 03-MB-706.05, Kategorie: V, ECTS: 6.
Die Veranstaltung ist als Kurs konzipiert, mit Vorlesungen und interaktivem Übungsbetrieb. Die Termine sind
- Montags 14-16 im MZH 1460
- Donnerstags 16-18 im MZH 1380
Achtung, die Vorlesung am 30.06.11 muss leider wegen Abwesenheit der Veranstalter ausfallen.
Die Veranstalter sind Till Mossakowski und Christoph Lüth (siehe verlinkte Heimatseiten für die Kontaktdetails).
Vorlesungsunterlagen
Hier finden sich die Vorlesungsfolien:
- Vorlesung 1 vom 04.04.11
- Vorlesung 2 vom 07.04.11
- Vorlesung 3 vom 11.04.11
- Vorlesung 4 vom 14.04.11
- Vorlesung 5 vom 18.04.11
- Vorlesung 6 vom 21.04.11
- Übung am 02.05.11
- Vorlesung 7 vom 05.05.11
- Vorlesung 8 vom 09.05.11
- Vorlesung vom 12.05.11: [Folien] [Handzettel]
- Vorlesung vom 16.05.11: [Folien] [Handzettel]
- Beispiele aus der Vorlesung vom 19.05.11: VSPL.thy, VSPLTrue.thy
- Vorlesung vom 23.05.11: [Folien] [Handzettel]
- Beispiele aus der Vorlesung vom 26.05.11: VSPred.thy, VSPredEx.thy, VSPredEq.thy, VSPresburger.thy, VSPeano.thy, VSPeanoEx.thy
- Vorlesung vom 30.05.11: [Folien] [Handzettel]
- Beispiele aus der Vorlesung vom 06.06.11: VSHOL.thy, VSHOLList.thy
- Vorlesung vom 09.06.11: [Folien] [Handzettel]
- Vorlesung vom 16.06.11: [Folien] [Handzettel]
- Beispiele aus der Vorlesung vom 20.06.11, 23.06.11 und 27.06.11 als
ZIP-Datei. Enthält:
- Problemstellung (Ueb03.txt) und Spezifikation (Ueb03Spec.thy)
- Zusätzlich Funktionen zur Modellierung von Worten (Ueb03Model.thy)
- Implementierung und Beweis in Isabelle (Ueb03Impl.thy), Prototyp in Haskell (Ueb03.hs).
Übungsblätter
- Übungsblatt 1 vom 07.04.11
- Übungsblatt 2, Teil 1 vom 19.05.11
- Übungsblatt 2, Teil 2 vom 26.05.11
- Übungsblatt 2, Teil 3 vom 06.06.11
- Übungsblatt 3 vom 20.06.11
Software für den Übungsbetrieb
Nachdem Sie diese Dateien heruntergeladen haben [1] [2], können sie in die die VirtualBox (siehe auch das Handbuch dazu), oder VMWare oder andere Virtualisierungssoftware geladen werden; Sie erhalten dann eine virtuelle Machine mit einer Ubuntu-Installation, auf der alle Software für die Veranstaltung vorinstalliert ist.