| TU München | Informatik | Software & Systems Engineering | Theorem Proving Group | Lehre |
Praktikum Spezifikation und Verifikation
Prof. Tobias Nipkow
Gerwin Klein
|
Wollten Sie schon immer verstehen, was Ihr Programm eigentlich macht? Dann sind Sie hier richtig! |
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.
Die Korrektheit von sicherheitskritischen Hard- und Softwaresystemen zu gewährleisten, ist immer noch ein ernstes Problem. Die zentralen Ziele dieses Praktikums sind das Erlernen
Konkret werden einige Anwendungsbeispiele behandelt, wobei wir aus Zeitgründen von vielen Details abstrahieren. Vorgesehen sind u.a.
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:
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 1539 eine Beratung durch einen studentischen Mitarbeiter an:
| Montag | 12:30 Uhr - 14:00 Uhr | Michael Wahler |
| Freitag | 14:00 Uhr - 15:30 Uhr | Michael Wahler |
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 sunhalle-Rechner und die am Lehrstuhl üblichen Sparc/Solaris und x86/Linux Plattformen zur Verfügung.
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
Mit
/usr/proj/isabelle/bin/isatool install -p ~/bin
kann man sich das Isabelle binary auch im eigenen
~/bin Verzeichnis installieren.
Unter KDE lässt sich 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.
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.
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 17.Juli von 15:00 Uhr bis 17:30 Uhr statt, genaue Zuordnung der einzelnen Gruppen zu den Terminen siehe unten.
Achtung Raumänderung: Die Präsentationen finden im Raum 2547 statt.
| Sebastian Pohle, Christian Wied, Ivan Gergintchev | 17. Juli | 15:00 Uhr - 15:25 Uhr | Raum 2547 |
| Eric Tiabou, Guy Kouam | 17. Juli | 15:30 Uhr - 15:55 Uhr | Raum 2547 |
| Stephan Hintzen, Stephan Gradl | 17. Juli | 16:00 Uhr - 16:25 Uhr | Raum 2547 |
| Laure Danthony, Katharina Kraft, Markus Kräutner | 17. Juli | 16:30 Uhr - 16:55 Uhr | Raum 2547 |
| Andreas Hofhauser, Karsten Linz, Thomas Stammeier | 17. Juli | 17:00 Uhr - 17:25 Uhr | Raum 2547 |
| Gerwin Klein | Last modified: Tue Jul 16 19:14:11 MEST 2002 |