Praktikum Spezifikation und Verifikation

Zeit:

Mittwochs 16-18 Uhr

Ort:

1546 ("McKinsey-Raum")

Beginn:

10. Mai 2000

Anmeldung:

Bei der zentralen Praktikumsanmeldung am Semesteranfang.

Zuordnung:

Das Praktikum zählt sowohl zum Bereich Theoretische als auch Praktische Informatik.

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

Voraussetzungen

• klassischer Logik,
• 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
• Grundlagen zu Model Checking
• 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 1533 eine Beratung durch studentische 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 am Lehrstuhl üblichen Sparc/Solaris und x86/Linux Plattformen zur Verfügung. Die Isabelle Distribution wird außerdem als Source und Binär-Pakete zum Download angeboten. Achtung: Verwenden Sie nur Isabelle_09-May-2000, oder eine neuere Version!

Aktuelle Hinweise

(5) Termine für die abschließende Präsentation

Im Anschluß daran (26. Juli, ca. 17 Uhr) sind alle Praktikumsteilnehmer herzlich ins Park Cafe eingeladen!

(4) Arithmetische Vereinfachung in Isabelle

Wie wir jetzt festgestellt haben, kann das neue Verhalten leicht zu Komplikationen führen, insbesondere können verschiedene Zahl-Darstellungen plötzlich gemischt auftauchen: z.B. eine 'gewöhnliche' 1 = Suc 0 vs. eine #1 in Binärdarstellung.

Folgender ML-code deaktiviert die neuen Prozeduren in der aktuellen Theorie:

ML_setup {*
  Delsimprocs Nat_Numeral_Simprocs.cancel_numerals;
  Delsimprocs [Nat_Numeral_Simprocs.combine_numerals];
*};

(3) Isabelle und Proof General

Weitere Hinweise zur Installation der einzelnen Komponenten befinden sich am Anfang des Isabelle/Isar Reference Manual.

(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/bin/Isabelle
      

Unter KDE kann man sich auch ein Application Desktop-Objekt zum Anklicken erzeugen:

        /usr/proj/isabelle/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.

(1) Rechnerbenutzung

Literatur

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