Praktikum Spezifikation und Verifikation



!!! Beginn: 3. Mai um 16:00 im S1128 !!!



Zielgruppe und Voraussetzungen

Dieses Praktikum wendet sich in erster Linie an diejenigen Studierenden nach dem Vordiplom, die sich im Bereich Programmentwicklung (Praktische Informatik) vertiefen wollen. Es ist aber ebenso für Leute mit Vertiefung im Bereich Semantik und Logik (Theoretische Informatik) interessant.

Das Praktikum erfordert als Voraussetzung Grundkenntnisse einer typisierten funktionalen Programmiersprache (etwa ML, Haskell 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 Konkret werden folgende Anwendungsbeispiele behandelt, wobei wir aus Zeitgründen von vielen Details abstrahieren:
  1. Codegenerierung für arithmetische Ausdrücke
  2. Arithmetik-Hardware (nicht die des Pentium!)
  3. Ein Cache-Coherence Protokoll
  4. Ein Datenkommunikationsprotokoll
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 jeden Mittwoch von 16:00-17:30 im S1128 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 eine Beratung durch studentische Hilfskräfte 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.