Praktikum Spezifikation und Verifikation

Zeit:

Mittwochs 16:00 - 18:00

Ort:

1546

Beginn:

25.4.

Anmeldung:

Bei der zentralen Praktikumsanmeldung.

Zuordnung:

Das Praktikum zählt zum Bereich Theoretische Informatik.

• Voraussetzungen
• Motivation und Inhalt
• Durchführung
• Arbeitsunterlagen und Aufgaben
• Aktuelle Hinweise
• Literatur

Voraussetzungen

• funktionaler Programmierung (z.B. in Gofer oder ML)

• formaler Programmentwicklung,
• logisch präzisen Beweisen.

So sollten Sie z.B. ein rekursives funktionales Programm schreiben können, das die natürlichen Zahlen 1, ..., n aufsummiert. Der Begriff der vollständigen Induktion sollte kein Fremdwort sein, und der Beweis, daß der von obigem Algorithmus berechnete Wert gleich n(n+1)/2 ist, keine fundamentalen Schwierigkeiten bereiten.

Motivation und Inhalt

Die Korrektheit von sicherheitskritischen Hard- und Softwaresystemen zu gewährleisten, ist immer noch ein ernstes Problem. Die zentralen Ziele dieses Praktikums sind das Erlernen

• der Modellierung von funktionalem Systemverhalten
• und des maschinengestützten Nachweisens der Korrektheit von Systemen.

Konkret werden einige Anwendungsbeispiele behandelt, wobei wir aus Zeitgründen von vielen Details abstrahieren. Vorgesehen sind u.a.

• Listen und Bäume
• Arithmetik
• Effiziente Datenstrukturen
• Hoare-Logik imperativer Programme
• Sicherheit im Unix-Filesystem

An jedem dieser Beispiele werden spezifische Modellierungs- und Beweistechniken geübt. Die Spezifikation und Verifikation erfolgt in Isabelle/HOL.

In einer das Praktikum speziell 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 Beschreibung funktionaler Programme.

Isabelle

ist ein generischer Theorembeweiser. Eine Ausprägung, Isabelle/HOL, unterstützt Spezifikation und Verifikation in HOL. Im Praktikum werden verschiedene 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. Die Aufgaben sind jeweils innerhalb von 1-3 Wochen zu bearbeiten und bei der Praktikumsleitung zu präsentieren (Termin nach Vereinbarung).

Ferner bieten wir zu den folgenden Zeiten im Raum 1545 eine Beratung durch einen studentischen Mitarbeiter an:

Alle Praktikumsteilnehmer und Betreuer sind unter psv@mailbroy.in.tum.de erreichbar. Hier können auch allgemeine Fragen zu Isabelle gestellt und beantwortet (!) werden.

Als Arbeitsumgebung stehen die am Lehrstuhl üblichen Sparc/Solaris und x86/Linux Plattformen zur Verfügung.

Arbeitsunterlagen und Aufgaben

Tutorium

Vorlesungsunterlagen

• Vorlesung 1: Demo.thy ToyList.thy
  
• Vorlesung 2: Demo.thy
  
• Vorlesung 3: Demo.thy ToyList.thy
  
• Vorlesung 4: Demo.thy Natürliches Schließen
  
• Vorlesung 5: Demo.thy
• Vorlesung 6: Demo.thy

Aufgaben

• Aufgabe 1: pdf thy
  Abgabe bis 2.5.2001
  Musterlösung: pdf thy
  
• Aufgabe 2: pdf thy
  Abgabe bis 9.5.2001
  Musterlösung: pdf thy
  
• Aufgabe 3: pdf Trie1.thy Trie2.thy Trie3.thy
  Abgabe bis 16.5.2001
  Musterlösung: pdf Trie1.thy Trie2.thy Trie3.thy
  
• Aufgabe 4: pdf thy
  Abgabe bis 23.5.2001
  Musterlösung: pdf thy
  
• Aufgabe 5: pdf thy PL.thy
  Abgabe bis 30.5.2001, 6.6.2001, 13.6.2001
  Musterlösung: pdf thy
  
• Aufgabe 6: pdf thy Hoare.thy
  Abgabe bis 20.6.2001, 27.6.2001
  
• Aufgabe 7: pdf
  Unix Formalisierung: pdf thy
  Unix Dokumentation
  Abgabe bis 3.7.2001, 11.7.2001, 18.7.2001

Aktuelle Hinweise

(1) Rechnerbenutzung

(2) Starten von Isabelle

Auf den sunbroy und sunhalle Rechnern läßt sich Isabelle (zusammen mit der Proof General Benutzeroberfläche) wie folgt starten:

        /usr/proj/isabelle/psv/bin/Isabelle
      

Mit

        /usr/proj/isabelle/psv/bin/isatool install -p ~/bin
      

Unter KDE lässt sich ein Application Desktop-Objekt zum Anklicken erzeugen:

        /usr/proj/isabelle/psv/bin/isatool install -k
      

Für zügiges Arbeiten mit Isabelle sollte man eine relativ robuste Maschine verwenden, am Lehrstuhl etwa die sunbroy60, sunbroy61, sunbroy1, oder einen sunhalle Rechner.

(3) Isabelle zuhause installieren

Sie können Isabelle recht einfach auf dem eigenen PC zuhause installieren. Isabelle sollte gut mit allen gängigen Linux-Distributionen zusammenarbeiten. Angenehmes Arbeiten ist ab ca. 128M Arbeitsspeicher und einer 500Mhz CPU möglich.

Weitere Hinweise zur Installation und eine vorkompilierte Isabelle-Version finden sie auf unserer download Seite.

(4) Hinweise für die abschließende Präsentation

Zum Abschluß des Praktikums findet eine Präsentation der letzten Aufgabe in Form eines 20- bis 25-minütigen Vortrags statt, an dem alle Teilnehmer einer Gruppe beteiligt sein sollten.

Für den Vortrag steht Ihnen ein Beamer und Notebook zur Verfügung, Sie können aber auch einen Tageslichtprojektor verwenden.

Die Präsentationen finden am 18.Juli von 14:30 Uhr bis 17:30 Uhr statt. Hier ist die genaue Zuordnung der einzelnen Gruppen zu den Terminen.

Achtung Raumänderung: Die Präsentationen finden im Raum 2547 und nicht, wie angekündigt im Raum 1546 statt.

Literatur

1. Tobias Nipkow and Lawrence Paulson Isabelle/HOL - The Tutorial, TU München, 2001.
2. Markus Wenzel. The Isabelle/Isar Reference Manual, TU München, 2001.
3. Lawrence C. Paulson. ML for the working programmer, Cambridge University Press, 1996.
4. Daniel J. Velleman. How to Prove it: A Structural Approach, Cambridge University Press, 1996.