Universität München
Institut für Informatik
Lehr- und Forschungseinheit für Programmierung und Softwaretechnik
Grundlagen der Systementwicklung (PG)
Aktuell
03.02.03
Pr�fungstermine sind jetzt online.
17.01.02 Die n�chste �bung wurde verschoben und findet nicht am Freitag, sondern am Montag danach, den 27. Januar, statt und zwar um 16:15 nach der Vorlesung (Treffpunkt: PST-Besprechungsraum).
15.11.02 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 ist
hier abrufbar. Diese Datei sollte als
uebung/List1.1
abgespeichert werden. Falls in diesem Verzeichnis noch keine (versteckte) Datei
.last
existiert, sollte diese angelegt werden, z.B. mit
echo List1 > .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
Die Vorlesung wird im Wintersemester 2002/03 gehalten von
Prof. Dr. Martin Wirsing
Die Übungen werden betreut von
Dr. Piotr Kosiuczenko
und von
Hr. Axel Rauschmayer
Adresse: |
Raum E5, Oettingenstr. 67 |
Telephon: |
2180 9126 |
Email-Adresse: |
rauschma AT informatik.uni-muenchen.de |
Sprechstunde: nach Vereinbarung |
Termine
Vorlesung: montags, 14-16 Uhr Raum 1.05
mittwochs, 10-12 Uhr Raum 0.05
Übungen: freitags, 10-12 Uhr Raum 1.27
Tutorien: freitags, 14-16 Uhr Raum E9 (Piotr Kosiuczenko)
donnerstags, 11-13 Uhr Raum E5 (Axel Rauschmayer)
Beginn der Vorlesung 1. Woche, Beginn der Übungen 2. Woche
Materialien
Es wird umfangreiches Begleitmaterial zur Vorlesung zur Verfügung gestellt.
Folien zur Vorlesung
- Kapitel 1: System Development and Formal Specification
- Kapitel 2: Data-Oriented System Development, Signatures for Interface Descriptions
- Kapitel 3: Data-Oriented System Development, Functional Models: Interpretation of Interfaces through Structures
- Kapitel 4: Data-Oriented System Development, Algebraic Specification with CASL
- Kapitel 5: Data-Oriented System Development, Refinement Technics
- Kapitel 6: Specification of state-based Systems, States and Transition Systems
- Kapitel 7: Specification of state-based Systems, Model-oriented Specification with Z
- Kapitel 8: Specification of state-based Systems, Specification Development with Z
- Kapitel 9: Reaktive Systeme, Transitionssysteme
- Kapitel 10: Reaktive Systeme, Spezifikation von Transitionssystemen mit TLA
Im vorletzten Jahr entstand ein Skript zur Vorlesung, das hier als
PDF-Datei oder als
Druckvorlage (gzip'te Postscript-Datei, zweispaltig) zur Verfügung steht.
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 ]
-
Z
-
Siehe
extra Seite zur Z-Notation.
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-Notation (lokal)
-
Seite mit Information zur Z-Notation, die lokal auf dem Server vorliegt.
-
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.
-
Zusammenfassung von TLA, von der TLA-Homepage entliehen, gibt einen Kurz�berblick �ber die Sprache.
-
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
kosiucze@informatik.uni-muenchen.de.
Lehrstuhl
Institut
Universität
Piotr Kosiuczenko