Angewandte Softwareverifikation mit einem interaktiven Theorembeweiser

Seitennavigation: Inhalt Ort und Zeit Systemdemo Skript PVS Voraussetzungen Ziele Anwendung Aufgaben Hilfe & Kontakt Dokumentation

Inhalt

In dieser Vorlesung werden Sie lernen, mit dem interaktive Theorembeweiser PVS zu arbeiten. Nach einer kurzen Einführung werden Sie eine Verifikationsaufgabe selbstständig in PVS lösen. (Die Vorlesung gleicht also eher einem Praktikum mit Einführung.)

In der Prüfung werden PVS und Details Ihrer Aufgabe besprochen.

Ort und Zeit (SS 2012)

Umfang in SWS:

1V + 1Ü + 0P

Systemdemo in der ersten Woche

Mi 4.4.2012, 2. DS, INF E069

Einführung 2.-4. Woche

nach Vereinbarung

Systemdemo

In der ersten Einführungsveranstaltung werde ich Ihnen die wichtigsten Aspekte von PVS anhand eines kleinen Beispiels im Rechnerlabor demonstrieren. Um dabei mitarbeiten zu können, bereiten Sie sich bitte wie folgt vor:

• Stellen Sie sicher, dass Sie sich im Rechnerlabor der Fakultät unter Linux anmelden und PVS starten können (entweder auf den Fakultätsrechnern oder auf Ihrem eigenen Rechner). Hinweise dazu gibt es in der PVS Überlebenshilfe.
• Erstellen Sie ein neues Verzeichnis und kopieren Sie die Beispieldatei sum.pvs dort hinein.

Skript

Was ist PVS?

• Die Pvs-Spezifikationssprache kann man sich in erster Näherung vorstellen als funktionale Programmiersprache ohne Seiteneffekte (so wie Haskell), erweitert um Existenz- und Allquantoren sowie die Möglichkeit, Axiome und Theoreme zu formulieren.
• Der Beweiser implementiert einen Beweiskalkül für die Pvs-Spezifikationssprache. Damit lassen sich die in den Quelldateien formulierten Theoreme beweisen. Der Beweiser ist interaktiv, das heißt, der Nutzer steuert die Aktionen des Beweisers durch seine Kommandos.

Pvs kann einen hohen Suchtfaktor entfalten! Seien Sie gewarnt! ;-)

Was Sie lernen werden

• mit Pvs umzugehen
• Spezifikationen in Logik höherer Ordnung zu erstellen
• Beweise mit Hilfe von Pvs durchzuführen

Wo Sie das Gelernte verwenden können

Die Benutzung eines interaktiven Theorembeweisers (wie Pvs) ist der radikalste Ansatz zur Spezifikation und Verifikation von Hard- oder Software. Dieses Praktikum wird Ihnen von Nutzen sein, wann immer Sie sich der formalen Behandlung von Hard- oder Software nähern.

PVS spielt auch in der Vorlesung Interactive Theorem Proving von Dr. Michael Posegga eine Rolle. Beide Vorlesungen sind aber unabhängig von einander.

Welche Voraussetzungen Sie mitbringen sollten

Pvs läuft nur auf Linux, Solaris und dem Mac mit einem Emacs-Frontend. Emacs-Erfahrung ist deshalb auch vorteilhaft. Man kann Pvs aber auch in der vi-Emulation in Emacs betreiben, sodass wenige Emacs-Kenntnisse ausreichen.

Aufgaben

1. Korrektheit von Quicksort [dvi.gz] [ps.gz] [dvi] [ps] [pdf]
2. Korrektheit von Heapsort [dvi.gz] [ps.gz] [dvi] [ps] [pdf]
3. Korrektheit von Bitonic Sort [dvi.gz] [ps.gz] [dvi] [ps] [pdf]
4. ausbalancierte binäre Bäume [dvi.gz] [ps.gz] [dvi] [ps] [pdf]
5. rot-schwarze Bäume (red-black trees) [dvi.gz] [ps.gz] [dvi] [ps] [pdf]
6. das Lampen-Frosch Problem [dvi.gz] [ps.gz] [dvi] [ps] [pdf]
7. Charakterisierung des reflexiven, symmetrischen und transitiven Abschlusses einer Relation mittels Zickzacks [dvi.gz] [ps.gz] [dvi] [ps] [pdf]
8. Knaster-Tarski-Fixpunkttheorem [dvi.gz] [ps.gz] [dvi] [ps] [pdf]
9. finale Sequenzen-Coalgebra [dvi.gz] [ps.gz] [dvi] [ps] [pdf]
10. Endliche Mengen: Externe Charakterisierung [dvi.gz] [ps.gz] [dvi] [ps] [pdf]
11. Endliche Mengen: Interne Charakterisierung [dvi.gz] [ps.gz] [dvi] [ps] [pdf]

Hilfe, Kontakt

Sie können natürlich auch auf den Pvs Emaillisten posten.

Private oder anonyme Hinweise, Anregungen oder Vorschläge senden Sie bitte an tews@os.inf.tu-dresden.de.

Dokumentation

• PVS Überlebenshilfe (mit vi-Modus Hinweisen): [ps.gz] [ps] [dvi.gz] [dvi] [pdf]
• PVS Kurzanleitung und Ergänzung von Prof. F. v. Henke und H. Pfeifer
• PVS Tutorien:
  • Standard Tutorium
  • Less Elementary Tutorial

Seitennavigation: Inhalt Ort und Zeit Skript PVS Voraussetzungen Ziele Anwendung Aufgaben Hilfe & Kontakt Dokumentation