Formale Spezifikation und Verifikation von Software (KITE und ST)

Vorlesung im Wintersemester 2002/2003 (drei SWS)

Dr. Bernhard Beckert

ACHTUNG RAUMÄNDERUNG:
Die Vorlesung findet ab sofort Donnerstags im Raum MB013 statt.

Die Vorlesung beginnt
Mittwochs um 14:15 Uhr s.t. (bis 15:45 Uhr), 14-tg., und
Donnerstags um 12:30 Uhr (bis 14:00 Uhr).

 In Zukunft wird die Vorlesung auch Mittwochs zweistündig (ab 14:15) und dafür nur 14-tägig gehalten.
 
 

Vorläufiger Zeitplan (Vorlesungstermine)

Mittwoch Donnerstag
06.11., 15:00 07.11., 12:30
13.11., 15:00 14.11., 12:30
20.11., 14:15 21.11., 12:30
28.11., 12:30
04.12., 14:15 05.12., 12:30
12.12., 12:30
18.12., 14:15 19.12., 12:30
Mittwoch Donnerstag
09.01., 12:30
15.01., 14:15 16.01., 12:30
23.01., 12:30
29.01., 14:15 30.01., 12:30
06.02., 12:30
12.02., 14:15 13.02., 12:30
20.02., 12:30


Allgemeine Informationen zur Vorlesung

Die Modellierung von Software in einer geeigneten Modellierungssprache (z.B. UML) gehört schon seit langem zu einer grundlegenden Technik des Software-Engineerings. Jedoch nimmt auch die praktische Bedeutung formaler Methoden in der Softwareentwicklung ständig zu, da mehr und mehr sicherheitskritische Anwendungen entstehen und die Qualitätsansprüche an Software wachsen.

In der Vorlesungen werden zunächst Techniken der formalen Beschreibung (Spezifikation) von Software vorgestellt (wobei die Spezifikation objektorientierter Software den Schwerpunkt bildet). Themen in diesem Bereich sind:

Im zweiten Teil der Vorlesung wird in Methoden zur deduktiven Verifikation von Software eingeführt. Sie dienen dazu, formal nachzuweisen, dass eine Implementierung ihre Spezifikation erfüllt. Themen sind hier: Die Vorlesung wendet sich an Studenten im Hauptstudium, und zwar gleichermaßen in den beiden Vertiefungsrichtungen "Künstliche Intelligenz" und "Softwaretechnik".

Voraussetzungen: Grundkenntnisse in Softwaretechnik und Prädikatenlogik.

Zeit und Ort:
Mittwochs, 14:15 Uhr s.t. bis 15:45 Uhr, 14-tg., MK101 und
Donnerstags, 12:30 bis 14:00 Uhr, MB013

Weitere Informationen:Bernhard Beckert


Materialien zur Vorlesung

Skriptum

Die Vorlesung Formale Spezifikation und Verifikation von Software deckt sich inhaltlich zum großen Teil mit der von Prof. Peter Schmitt an der Universität Karlsruhe gehaltenen Vorlesung UML and its Meaning. Darum ist das von Prof. Schmitt erstellte Skriptum als weiterführende Literatur sehr nützlich und dient auch als vorläufiges Skriptum zur Vorlesung Formale Spezifikation und Verifikation von Software. Zum Ende des Semesters werde ich hier eine überarbeitete und erweiterte Version des Skriptums zur Verfügung stellen, das dann auch die weiteren Inhalte der Vorlesung Formale Spezifikation und Verifikation von Software abdeckt.

Folien

Jeweils nach der Vorlesung werden die Folien hier zur Verfügung gestellt.

Übungsblätter

Von Zeit zu Zeit werde ich hier Übungsblätter mit Aufgaben zum Stoff der Vorlesung bereit stellen. Nachdem genügend Zeit zur Bearbeitung vertrsichen ist, wird es hier auch Musterlösungen geben.

Weitere Materialien


Bernhard Beckert