Techniken zur Entwicklung Korrekter Software 1
Willkommen auf der Heimatseite der Lehrveranstaltung "Techniken zur Entwicklung Korrekter Software 1" im Wintersemester 2007/2008!
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 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). Formale Methoden sind allerdings immer eng mit Techniken des formalen Beweisens verbunden, denn nur durch rechnergestützte Beweise läßt sich die für diesen Bereich nötige durchgängige Korrektheit sicherstellen.
Diese Veranstaltung soll in die nötigen theoretischen Grundlagen einführen, einen Überblick über das Gebiet geben, so dass Teilnehmer formale Methoden in zukünftigen Projekten selber einsetzen können. Schwerpunkte der Veranstaltung sind Anforderungsspezifikationen, Entwurfsspezifikationen und formale Entwicklung, die Spezifikationssprache CASL und Techniken des rechnergestützten, formalen Beweisens.
Themen
In der Vorlesung werden folgende Themen behandelt:- Theoretische Grundlagen
- Spezifikation in CASL
- Grundlagen des formalen Beweisens
- Techniken des rechnergestützten Beweisens
- Entwicklung durch Verfeinerung
Im Übungsbetrieb werden wir die Spezifikationssprache CASL, den Theorembeweiser Isabelle und das Hets-Werkzeug benutzen.
Organisatorisches
Die Veranstalter sind Lutz Schröder und Christoph Lüth.
VAK: 03-05-H-706.05.
K 4 SWS (6 ECTS) Praxis (A), Handelsklasse: I
Termine:
- Mon 10:00 - 12:00 MZH 7230 Tue 13:00 - 15:00 MZH 7230
- Veranstaltungsbeginn (erste Vorlesung): Di 23.10 13:00 ct
Wegen starker inhaltlicher Überschneidungen kann dieses Modul nicht gleichzeitig mit dem Modul "Formale Methoden der Softwaretechnik I" angerechnet werden.
Vorlesungsfolien
- Vorlesung vom 23.10.2007: Einführung [PDF]
- Vorlesung vom 29.10.2007: Überblick über CASL [PDF]
- Vorlesung vom 30.10.2007: Wiederholungsfolien zur CASL-Syntax [PDF]
- CASL-Einführung (Bidoit/Mosses) [PDF]
- Vorlesung vom 03/04.12.2007: Aussagenlogik
und natürliches Schließen [PDF]
Dazu auch: Example1.thy und VSPL.thy - Vorlesung vom 10/11.12.2007: Quantoren [PDF]
Dazu auch: VSPred.thy und VSPredEx.thy - Vorlesung vom 18/19.12.2007: Isabelle
[PDF]
Dazu auch: VSPredEq.thy, VSNat.thy und VSNatEx.thy. - Vorlesung vom 08.01.2008: Logik höherer
Stufe [PDF]
Dazu auch: VSPLRes.thy (Verschiedene Arten der Resolution: rule, erule, drule). - Vorlesung vom 14.01.2008: VSHOL.thy und VSHOLEx.thy.
- Vorlesung vom 15.01.2008: Isabelle/HOL
[PDF]
Dazu auch: Datatypes.thy und Auto.thy. - Vorlesung vom 21.01.2008: Rekursion &
Induktion [PDF]
Dazu auch: MyList.thy und MyListExample.thy - Vorlesung vom 04.02.2008: AdvancedExamples.thy
Weiteres Material:
- Überblick über alle Ableitungsregeln des natürlichen Schließens (aus der VL)
- Mehr über die Softwarefehler im Therac-25.
- Absturz der Ariane-5: Untersuchungsbericht.
- Verlust des Mars Climate Orbiters .
Übungsblätter
- Übungsblatt 1 [PDF] (keine Abgabe)
- Übungsblatt 2 [PDF] (Abgabe 10.12.2007)
- Übungsblatt 3 [PDF], Teil 1 (Abgabe 15.01.2008)
- Übungsblatt 3 [PDF], Teil 2 (Abgabe 04.02.2008)
- Übungsblatt 4 [PDF] (Abgabe 20.02.2008) mit zugehöriger CASL-Spezifikation von Queues und dem Beweis der ersten implizierten Formel
Links
In diesem Abschnitt finden sich Links und Verweise zu weiterführender Literatur.
CASL
- Die Heimatseite von CASL
- Die Heimatseite der Common Framework Initiative
Isabelle
- Die Isabelle Heimatseite.
- Die Proof General Heimatseite.
- Übersicht über die Theorien in Isabelle/HOL.
- Handbücher: das Referenzhandbuch, das HOL-Handbuch, das Systemhandbuch.