Praktikum Spezifikation und Verifikation
!!! Beginn: Mi., 8. Mai um 16:00 im S1128 !!!
Zielgruppe und Voraussetzungen
Dieses Praktikum wendet sich in erster Linie an Studierende nach
dem Vordiplom, die sich im Bereich Programmentwicklung (Praktische
Informatik) vertiefen wollen. Es ist aber ebenso für Vertiefung
im Bereich Semantik und Logik (Theoretische Informatik) interessant.
Das Praktikum erfordert als Voraussetzung Grundkenntnisse einer typisierten
funktionalen
Programmiersprache (etwa ML,
oder Gofer) und ein
Interesse am Umgang mit formalen Begriffen und Methoden.
Inhalt
Die Korrektheit von zunehmend komplexeren Hard- und Softwaresystemen zu
gewährleisten, ist zu einem ernsten Problem geworden, vor allem in
sicherheitskritischen Bereichen [1]. Die
zentralen Ziele dieses Praktikums sind das praktische Erlernen
- von formalen Techniken zur Modellierung des funktionalen Verhaltens
von Systemen aus verschiedenen Bereichen der Informatik,
- des Umgangs mit Werkzeugen zum computergestützten Nachweis der
Korrektheit von Systemen.
Konkret werden einige Anwendungsbeispiele behandelt, wobei wir aus
Zeitgründen von vielen Details abstrahieren. Vorgesehen sind u.a.:
- Codegenerierung für arithmetische Ausdrücke
- Arithmetik-Hardware (nicht die des Pentium!)
- Ein Cache-Coherence Protokoll
An jedem dieser Beispiele werden spezifische Modellierungs- und auch
Beweistechniken geübt. Die Spezifikation erfolgt jeweils in HOL, die
Verifikation in Isabelle [2]. In einer das Praktikum begleitenden
Vorlesungsreihe werden die Grundlagen zu Isabelle/HOL vermittelt:
- HOL
- ist, in erster Näherung, die Anreicherung einer polymorphen
funktionalen Programmiersprache um logische Konzepte wie Quantoren und
Mengen. HOL ist damit eine ideale Sprache zur Entwicklung funktionaler
Programme.
- Isabelle
- ist ein generischer Theorembeweiser. Eine Ausprägung,
Isabelle/HOL, unterstützt Spezifikation und Verifikation in HOL. Es
werden verschiedenen Beweisverfahren (Termersetzung, Induktion, etc)
vorgestellt und ihre Funktion innerhalb des Beweisprozesses erläutert.
Durchführung
In der ersten Hälfte des Semesters findet
eine Vorlesung statt, in der die nötigen
Isabelle/HOL Kenntnisse vermittelt werden. Außerdem findet eine
wöchentliche Besprechung mit der Praktikumsleitung statt.
Die obigen Anwendungsbeispiele werden in der Vorlesung und der
wöchentlichen Besprechung vorgestellt und sind dann innerhalb von 3
Wochen in Gruppen zu bearbeiten und anschließend zu präsentieren.
Zur Durchführung stehen am Lehrstuhl eigene Suns und HPs zur
Verfügung. Zusätzlich bieten wir zu festen Zeiten Beratung an.
Literatur
- 1
-
W. Wayt Gibbs.
Software: chronisch mangelhaft.
Spectrum der Wissenschaft, Dezember 1994, 56-63.
- 2
-
Lawrence C. Paulson.
Isabelle: A Generic Theorem Prover,
Springer LNCS 828, 1994.