Universität München
Institut für Informatik
Lehr- und Forschungseinheit für Programmierung und Softwaretechnik
www.pst.informatik.uni-muenchen.de/Lehre/WS0102/gse/

Grundlagen der Systementwicklung (PG)

Aktuell

12.11.01: Informationen über die von HOL-CASL ausgeführten Beweisschritte erhält man, indem man unter [Options | Isabelle Options] die Isabelle-Konsole öffnet und "Trace simplification" aktiviert. Eine Beispiel-Sitzungsdatei für die in der Vorlesung vorgeführten Beweise ist hier abrufbar. Diese Datei sollte als HOL-CASL/git/sessions/casl_win/ListNat.1 abgespeichert werden. Falls in diesem Verzeichnis noch keine (versteckte) Datei .last existiert, sollte diese angelegt werden, z.B. mit

echo ListNat > .last

Inhalt

Ein bedeutsames und derzeit noch unbefriedigend beherrschtes Problem im Entwicklungsprozess technischer Systeme ist die Zuverlässigkeit der produzierten Software. Diese ist gegeben, wenn ein Softwaresystem im Sinne der Aufgabenstellung funktioniert und auch auf Fehler angemessen reagiert. Besonders in sicherheitskritischen Anwendungsgebieten, wie etwa bei medizinischen Anwendungen, bei Zahlungssystemen, elektronischer Kommunikation, Zugangskontrollsystemen, aber auch Gasbrennersteuerungen im Haushalt, ist es entscheidend, dass die verwendeten Programmsysteme zuverlässig und sicher arbeiten. Die Vorlesung gibt eine Einführung in Methoden und Techniken zum Entwurf sicherer Systeme. Besonderes Gewicht wird dabei auf Techniken der Spezifikation und der Verfeinerung von Spezifikationen gelegt, die die Grundlage f�r moderne Validierungs- und Verifikationswerkzeuge bilden. Insbesondere werden folgende Themen behandelt:

• daten-orientierte Spezifikationsentwicklung (Abstrakte Datentypen, Wechsel der Datenstruktur, CASL)
• Spezifikation dynamischer Systeme (Transitionssysteme, modell-basierte Spezifikationen, Invarianten, Vor- und Nachbedingungen, Z)
• Verifikation und Verfeinerung nebenläufiger Systeme (Eigenschaften von Abläufen, Temporale Logik, Model Checking, TLA)

Die Vorlesung wendet sich an Studierende im Haupt- und Nebenfach Informatik. Der Schein gilt für die Diplom-Hauptprüfung im Haupt- und Nebenfach Informatik. Der Schein gilt auch für die Hauptprüfung für das Lehramt an Gymnasien im Erweiterungsfach Informatik.

Personen

Prof. Dr. Martin Wirsing

Adresse:	Raum 058, Oettingenstr. 67
Telephon:	2178 2154
Email-Adresse:	wirsing@informatik.uni-muenchen.de

Dr. Stephan Merz

Adresse:	Raum E0.9, Oettingenstr. 67
Telephon:	2178 2182
Email-Adresse:	merz@informatik.uni-muenchen.de
Sprechstunde:	Mo, 10-11 Uhr und nach Vereinbarung

Dr. Piotr Kosiuczenko

Adresse:	Raum E9, Oettingenstr. 67
Telephon:	2178 2133
Email-Adresse:	kosiucze@informatik.uni-muenchen.de
Sprechstunde:	Do, 14-15 Uhr und nach Vereinbarung

Termine

Vorlesung:      montags, 14-16 Uhr             Raum 1.27
              mittwochs, 10:40-12:10 Uhr       Raum 1.27
Übungen:      dienstags, 12-14 Uhr             Raum 1.27

Materialien

Warnung: Das Skript ist noch nicht korrigiert. Für Hinweise auf Fehler und Verbesserungsvorschläge wären wir dankbar.

Weiterführende Unterlagen

CASL

Syntax: [ HTML | PDF | gzip'tes Postscript ]

Einführung: [ Guided Tour | Beispiele ]

Werkzeuge: [ Überblick ]

HOL-CASL: [ lokale Installation | Kurzanleitung | Homepage | Beispiel LISTNAT.casl | Sitzungsdatei ListNat.1 ]

CASL-Spezifikationen müssen für HOL-CASL im Verzeichnis HOL-CASL/examples/ liegen, Sitzungsdateien im Verzeichnis HOL-CASL/git/sessions/casl-win/. Der Name von Spezifikation und .casl-Datei muss übereinstimmen, der Name der Sitzungsdatei ist beliebig.

Warnung: Die offizielle Kommentarsyntax für CASL hat sich gegenüber der Syntax der Vorlesung geändert. CASL-Parser ab Version 0.7 liefern Fehlermeldungen. HOL-CASL basiert aber noch auf der in der Vorlesung verwendeten Syntax.

Z

Merkblatt Z-Notation

z-eves.sty zur Formatierung von Z-Spezifikationen mit LaTeX.

Jaza: [ Manual (Postscript) | Homepage ]

Z/Eves: [ User's Guide | Mathematical Toolkit | Reference Manual | Homepage ]

Emacs-Mode für Z/Eves: z-eves.el z.B. in ~/lib/xemacs/z-eves.el abspeichern und folgende Zeilen in die Datei .emacs aufnehmen:

    (setq auto-mode-alist
       (append auto-mode-alist
          '(("\\.z$" . z-latex-mode)
            ("\\.zed$" . z-latex-mode))))
    (autoload 'z-latex-mode "~/lib/xemacs/z-eves" "Z-EVES LaTeX mode." t)
    (autoload 'run-z-eves "~/lib/xemacs/z-eves" "Run Z-EVES." t)
    (setq z-eves-program "z-eves")

TLA

• S. Merz: A User's Guide to TLA entstand als Beitrag zu einer Sommerschule und gibt einen einführenden Überblick zu TLA.
• M. Abadi, S. Merz: On TLA as a Logic gibt eine präzisere Definition der Logik TLA und behandelt weiterführende Themen.

Literatur

J. Loeckx, H. Ehrich, M. Wolf

Specification of Abstract Data Types. Wiley & Teubner, 1996.

M. Wirsing

Algebraic specification. In J. van Leeuwen (ed.): Handbook of Theoretical Computer Science. Elsevier, Amsterdam, 1990.

CASL

Common language for formal specification of functional requirements and modular software design, 2000.

J. Jacky

The Way of Z: Practical Programming with Formal Methods. Cambridge University Press, 1997.

Z homepage

C. Morgan

Programming from Specifications. Prentice Hall, 3. Auflage, 1998.

Z. Manna, A. Pnueli

The temporal logic of reactive and concurrent systems - specification. Springer-Verlag, New York, 1992 (vergriffen, in der Bibliothek vorhanden).

L. Lamport

TLA - The Temporal Logic of Actions.

SML

Empfehlenswert ist vor allem Larry Paulsons Buch ML for the working programmer (Cambridge Univ. Press, 2. Auflage, 1996). Weitere Informationen, insbesondere zu dem am CIP-Pool installierten SML-Interpreter, enthält die Homepage von SML/NJ.

Übungsbetrieb