TU Wien:Formale Verifikation von Software VU (Futschek)
Daten[Bearbeiten | Quelltext bearbeiten]
| Vortragende | Gerald Futschek, Gernot Salzer (Übungsteil) |
|---|---|
| ECTS | 6 |
| Links | tiss:185292 , Homepage |
| Masterstudium Logic and Computation | |
| Masterstudium Software Engineering & Internet Computing | |
| Masterstudium Technische Informatik |
Inhalt[Bearbeiten | Quelltext bearbeiten]
- Grundlagen der formalen Verifikation (Hoare-Logik)
- Entwicklung korrekter Programme mit Hilfe von Zusicherungen, Pre- und Postconditions, Schleifeninvarianten
- Verifikation sequentieller, paralleler und verteilter Programme
- praktische Übungen mit ausgewählten Systemen zur Programmverifikation.
Ablauf[Bearbeiten | Quelltext bearbeiten]
Die Lehrveranstaltung gliedert sich in Vorlesungs- und Übungsteil (siehe unten).
Benötigte/Empfehlenswerte Vorkenntnisse[Bearbeiten | Quelltext bearbeiten]
Kaum. Elementare Programmierkenntnisse sowie einigermaßen gutes Verständnis für (einfache) mathematische Beweise helfen wohl.
Vortrag[Bearbeiten | Quelltext bearbeiten]
Fast jede Woche wird eine ca. zweistündige Vorlesung gehalten. Der Inhalt ist grundsätzlich interessant, der Vortragsstil mitunter (spätestens dann, wenn der Vortragende in englischer Sprache vorträgt) zum Einschlafen langweilig.
Andere Meinung: Ich finde den Vortragsstil sehr angenehm. Es wird alles so erklärt, dass es wirklich gut verständlich ist.
Übungen[Bearbeiten | Quelltext bearbeiten]
Es gibt zwei Übungsbeispiele; Inhalt ist die Verwendung von Perfect Developer zur formalen Verifikation, wie in der Vorlesung gebracht.
- Im ersten Übungsbeispiel geht es darum, das Tutorial zu Perfect Developer durchzuarbeiten und darin Fehler zu finden.
- Im zweiten Beispiel ist aus einer Liste in textueller Form gegebener Problemen eine Auswahl vorgegebener Größe zu treffen. Zu den ausgewählten Problemen sind jeweils eine formale Spezifikation anzugeben und weiters eine Implementierung, die durch Perfect Developer automatisch gegen die formale Spezifikation verifiziert werden soll. In diesem Beispiel hat man mit einigen der Probleme zu kämpfen, die ein automatischer Beweiser mit sich bringt; so können manchmal triviale Beweise nicht erbracht werden, obwohl für den menschlichen Betrachter offensichtlich ist, dass die zu beweisende Behauptung wahr ist. Auch die Dokumentation von Perfect Developer ist in dieser Hinsicht mangelhaft, da nicht dokumentiert ist, was genau automatisch bewiesen werden kann und was nicht.
Am Ende des Semesters gibt es ein Abgabegespräch, das nicht das geringste Problem darstellt, sofern man die Übungsbeispiele selbst gemacht hat. Es wird in erster Linie über Probleme diskutiert, die bei der Verwendung von Perfect Developer aufgetreten sind. Leider wurde man erst am Ende des Semesters (im Sommersemester 2008 am 30. Juni, ebenso im SS11) darauf aufmerksam gemacht, dass es ein Abgabegespräch gibt.
Prüfung, Benotung[Bearbeiten | Quelltext bearbeiten]
Die Prüfung ist nicht besonders schwer. Sie umfasst ausschließlich Beispiele, wie sie bereits in der Vorlesung gebracht wurden. Da alle schriftlichen Unterlagen verwendet werden dürfen, hält sich der Lernaufwand in Grenzen, zumindest, wenn man in (fast) allen Vorlesungseinheiten (geistig) anwesend war.
SS 2011: Das Niveau der Prüfung dürfte angehoben worden sein, ohne durcharbeiten des Teils 3 des Buches von D. Griess oder dem Studium der Unterlagen, sofern sie vollständig sind, und alle vorgerechneten Beispiele umfassen, sehe ich wenig Chance ein akzeptables Ergebnis bei der Prüfung zu erlangen.
Anmerkung: Ohne zu lernen geht es natürlich nicht :) Wer mit den Unterlagen zur Prüfung marschiert und meint ohne diese vorher durchzuarbeiten eine gute Note zu schaffen ist sicher fehl am Platz. Wer in die Vorlesung geht, aufpasst, die Beispiele mitschreibt und vor der Prüfung alles noch mal durchgeht dürfte aber kaum Probleme haben.
Dauer der Zeugnisausstellung[Bearbeiten | Quelltext bearbeiten]
Prüfung war am 23.06.2008; Prüfungsergebnisse gibt es seit 01.09.2008, Zeugnis am 03.09.2008. Bis dato jedoch keine Antwort auf ein diesbezüglich am 27.08.2008 an Salzer und Futschek versandtes Mail.
Zeitaufwand[Bearbeiten | Quelltext bearbeiten]
Was man nicht unterschätzen darf, ist der Aufwand für das zweite Übungsbeispiel. Die zu bearbeitenden Probleme sind grundsätzlich leicht; daraus eine formale Spezifikation zu extrahieren sowie eine Implementierung zu schreiben, sodass Perfect Developer in der Lage ist, die Korrektheit zu beweisen, kann einiges an Zeit in Anspruch nehmen.
Eher als gering einzuschätzen ist bei regelmäßigem Besuch der Vorlesung der Lernaufwand für die Prüfung über den Vorlesungsstoff.
Unterm Strich ist der Aufwand für sechs ECTS-Punkte gering, vor allem im Vergleich zu anderen Lehrveranstaltungen mit gleicher Anzahl an ECTS-Punkten, zum Beispiel Software Engineering und Projektmanagement LU.
Tipps[Bearbeiten | Quelltext bearbeiten]
- In die Vorlesung gehen und (zumindest das Wichtigste) mitschreiben. Es gibt keine Unterlagen, die speziell auf den Inhalt dieser Vorlesung eingehen, lediglich mehrere Bücher, die jeweils einen Teil abdecken. Die Mitschriften dürfen bei der Prüfung verwendet werden und machen das Lösen der Prüfungsbeispiele fast zu einer Abschreibübung.
- Den Aufwand für das dritte Übungsbeispiel darf man nicht unterschätzen.
- Perfect Developer ist ein proprietärer Batzen Software, den es unter Linux nur für x86 und nicht für x86_64 gibt (Windows-Version gibt's auch, für Mac-User schaut's aber schlecht aus). Zwar läuft die x86-Version auch auf x86_64-Systemen, allerdings hat man in diesem Fall immer wieder mit Krämpfen zu tun. So muss man zum Beispiel unter Ubuntu einige x86-Bibliotheken manuell nachinstallieren. Verwendet man die C++-Codeausgabe von Perfect Developer, muss man die Runtime-Library von Perfect aus dem glücklicherweise mitgelieferten Source für x86_64 neu kompilieren (mit gcc 3.3; weder gcc 3.4 noch gcc 4.2 funktionieren), damit man das von Perfect Developer generierte Programm mit dem x86_64-gcc kompilieren und linken kann. Meine Empfehlung daher: Wenn möglich, Windows oder ein x86-Linux verwenden.
- Perfect Developer kann für Teilnehmer der Lehrveranstaltung von der Webseite des Instituts heruntergeladen werden. Es empfiehlt sich, ab und zu auf der Downloadseite vorbeizuschauen, ob es vielleicht eine neue Version gibt, in der "etwas mehr" als in der alten Version bewiesen werden kann.
Verbesserungsvorschläge / Kritik[Bearbeiten | Quelltext bearbeiten]
noch offen
_-_Pr_27-06-11.jpg){kind=link}