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

Grundlagen der Systementwicklung (PG)

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)
Validierung 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

Die Vorlesung wird im Wintersemester 2000/01 gehalten von

Prof. Dr. Martin Wirsing

Adresse: Raum 058, Oettingenstr. 67
Telephon: 2178 2154
Email-Adresse: wirsing@informatik.uni-muenchen.de
Sprechstunde: Di, 11-12 Uhr

Adresse:	Raum 058, Oettingenstr. 67
Telephon:	2178 2154
Email-Adresse:	wirsing@informatik.uni-muenchen.de
Sprechstunde:	Di, 11-12 Uhr

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

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

Stephan Merz betreut auch die Übungen.

Termine

Vorlesung:      montags, 14-16 Uhr       Raum 0.43
            donnerstags, 11-13 Uhr       Raum 1.27
Übungen:      dienstags, 11-13 Uhr       Raum 1.05

Beginn der Vorlesung am 16.10.2000, Beginn der Übungen am 24.10.2000.

Materialien

Skript

Frau Johanna Martin hat dankenswerterweise ein Skript zur Vorlesung erstellt.

PDF-Version

zweispaltige Druckvorlage (.ps.gz)

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 | DVI | Postscript]

HOL-CASL: [lokale Installation | Kurzanleitung | Homepage]

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

Das Papier 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.
The Z notation
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

Zur Teilnahme an den Übungen ist keine separate Einschreibung erforderlich. Die Übungsblätter werden montags in der Vorlesung ausgeteilt. Sie enthalten Präsenzaufgaben und Hausaufgaben. Die Hausaufgaben sind bis zum Dienstag der Folgewoche zu bearbeiten und in der Übungsstunde abzugeben. Für die Zulassung zur Semestralprüfung sind etwa 50% der in den Hausaufgaben erreichbaren Punkte erforderlich.

Anregungen, Kommentare? Bitte schicken Sie eine email an merz@informatik.uni-muenchen.de.