A) Schwerpunkt dieser Vorlesung sind sogenannte modellbasierte
Spezifikationstechniken. Diese Techniken ermöglichen die
Beschreibung und Konstruktion eines konkreten Modells des zu
entwerfenden Systems.
Der Einsatz formaler Beschreibungstechniken wird innerhalb der
Software-Entwicklung immer häufiger verlangt. Dies gilt insbesondere
für den Bereich der sicherheitskritischen Systeme. Dabei werden in
der Praxis modellbasierte Spezifikationstechniken wie etwa Z,
B-Methode und VDM in den frühen Entwicklungsphasen am häufigsten
eingesetzt. Grundlage dieser Spezifikationstechniken ist die
einfache Mengenlehre und Prädikatenlogik erster Stufe, die es auf
eine natürliche Art und Weise erlauben, Mengen mit ihren Operationen
zur Definition von Datenträgern bzw. Vor- und Nachbedingungen zur
Definition der Methoden auf den Datenträgern zu verwenden.
Vorgestellt werden hauptsächliche Z, B-Methode und ASM (Abstract
State Machines). Hierbei werden nicht nur Syntax und Semantik
behandelt, sondern auch die wichtige Methode der Verfeinerung
vorgestellt und anhand einzelner Fallstudien verdeutlicht. Die in
diesem Zusammenhang entstehenden Beweisaufgaben werden
charakterisiert und in den Beispielen ermittelt und überprüft.
B) Nimal Nissanke: Formal Specification: Techniques and
Applications. Springer, 1999.
Ben Potter, Jane Sinclair, David Till: An Introduction to Formal
Specification and Z. Prentice Hall, 1996.
Jim Woodcock, Jim Davies: Using Z: Specification, Refinement, and
Proof, Prentice Hall, 1996.
C) Vordiplom Informatik.
D) --
E) Vertiefungsveranstaltung des Lehrgebiets 'Grundlagen der Programmierung'.
