Formale Techniken der Software-Entwicklung
Aktuelles
Inhalte
Die Entwicklung zuverlässiger Soft- und Hardware stellt immer noch ein großes Problem dar. Aufgrund der Komplexität moderner Systeme gibt es viele Fehler, die nur in wenigen Systemzuständen oder in bestimmten Interaktionen mit der Umgebung auftreten. Durch Tests sind diese Fehler nur schwer zu finden. Für kritische Systeme bietet sich daher der Einsatz von Techniken an, die es Entwicklern ermöglichen, Eigenschaften systematisch zu spezifizieren und das fertige System aus der Spezifikation zu generieren oder die Eigenschaften des Systems gegenüber der Spezifikation zu verifizieren.
In dieser Vorlesung werden logische Grundlagen und formale Techniken der Software-Entwicklung behandelt. Neben dem grundlegenden Verständnis für formale Methoden liegt ein Schwerpunkt auf praktisch anwendbaren Techniken und Werkzeuge zur formalen Spezifikation und Verifikation. Geplant sind die folgenden Themen:
- Einführung in die Computational Logic ACL2 und automatisches Theorembeweisen
- Boole'sche Logik und Erfüllbarkeit, SAT Solving
- Rekursion und induktive Beweise
- Einführung in die Prädikatenlogik und Logiken höherer Ordnung
- Spezifikation von Systemen
- Ausblick in die Behandlung von zeitbasiertem Verhalten, Model Checking
Termine
Vorlesung (3-stündig)
- Mo 12ct-15 Uhr, Richard-Wagner-Str. 10, Raum 101
Übung (2-stündig)
- Fr 12ct-14 Uhr, Richard-Wagner-Str. 10, Raum 101
Mündliche Prüfungen
- Die Termine für die mündlichen Prüfungen stehen noch nicht fest.
Personen
Dozent
Übungsbleitung
Materialien
Vorlesung
- Folien der ersten Vorlesung
- Folien der zweiten Vorlesung
- Folien der dritten Vorlesung
- Folien der vierten Vorlesung
- Folien der fünften Vorlesung
- Folien der sechsten Vorlesung
- Folien der siebten Vorlesung
- Folien der achten Vorlesung
- Folien der neunten Vorlesung, "Logikprogrammierung" in Snark
- Folien der zehnten Vorlesung
- Folien der elften Vorlesung
- Folien der zwölften Vorlesung
- Folien der dreizehnten Vorlesung
Übungsblätter
Übung
- 22. Mai 2015
- Präsentation
- Java-Code zu SAT (Eclipse-Projekte graphdyer, simplesat und sat4jtest)
- 05. Juni 2015
Hörerkreis
Benötigte Vorkenntnisse
Literatur
Insbesondere gibt es als Begleitmaterial für das Buch ein Reihe von Übungsaufgaben samt Lösungen im Internet: