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:
-
Mathematische Grundlagen (insbes. Mengentheorie, Logik)
-
Formale Semantik von UML-Klassendiagrammen
-
Object Constraint Language (OCL)
-
Abstract State Machines (ASMs)
-
State Charts
-
Die Spezifikationssprache Z
-
Abstrakte Datentypen
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:
-
Hoare-Logik
-
Grundlagen der Dynamischen Logik
-
Erweiterungen der Dynamischen Logik zur Behandlung objektorientierter Programmiersprachen
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.
-
folien01.ps.gz
- Vorlesung am 06.11.02 (Introduction and Motivation)
-
folien02.ps.gz
- Vorlesung am 07.11.02 (Reviewing Basic Set Theory)
-
folien03.ps.gz
- Vorlesung am 07.11.02 (Propositional and Predicate Logic)
-
folien04.ps.gz
- Vorlesung am 13.11.02 (Modal Logic)
-
folien05.ps.gz
- Vorlesung am 14.11.02 (The Unified Modeling Language)
-
folien06.ps.gz
- Vorlesung am 14.11.02 (UML Class Diagrams by Example)
-
folien07.ps.gz
- Vorlesung am 14.11.02 (The Object Constraint Language by Example)
-
folien08.ps.gz
- Vorlesung am 20.11.02 (Example: Role Based Access Control, Teil 1)
-
folien09.ps.gz
- Vorlesung am 21.11.02 (Example: Role Based Access Control, Teil 2)
-
folien10.ps.gz
- Vorlesung am 21.11.02 (OCL: Syntax and Semantics, Teil 1)
-
folien11.ps.gz
- Vorlesung am 28.11.02 (OCL: Syntax and Semantics, Teil 2)
-
folien12.ps.gz
- Vorlesung am 28.11.02 (The UML Metamodel)
-
folien13.ps.gz
- Vorlesung am 04.12.02 (Abstract State Machines, Teil 1)
-
folien14.ps.gz
- Vorlesung am 05.12.02 (Abstract State Machines, Teil 2)
-
folien15.ps.gz
- Vorlesung am 12.12.02 (ASM Example: Steam Boiler Control)
-
folien16.ps.gz
- Vorlesung am 12.12.02 (The Z Specification Language, Teil 1)
-
folien17.ps.gz
- Vorlesung am 18.12.02 (The Z Specification Language, Teil 2)
-
folien18.ps.gz
- Vorlesung am 19.12.02 (The Z Specification Language, Teil 3)
-
folien19.ps.gz
- Vorlesung am 19.12.02 (Z Example: Steam Boiler Control)
-
folien20.ps.gz
- Vorlesung am 09.01.03 (UML State Machines, Teil 1)
-
folien21.ps.gz
- Vorlesung am 15.01.03 (UML State Machines, Teil 2)
folien22.ps.gz
- |
Vorlesung am 15.01.03 (CASL: Algebraic Specification, Teil 1, Folien
1-16) |
|
Vorlesung am 16.01.03 (CASL: Algebraic Specification, Teil 2, Folien
17-49) |
|
Vorlesung am 23.01.03 (CASL: Algebraic Specification, Teil 3, ab Folie 50) |
-
folien23.ps.gz
- Vorlesung am 29.01.03 (Induction on Free Types: Arbitrarily Branching Trees)
- keine Folien - Vorlesung am 30.01.03 (Demo of the
KeY System)
-
folien24.ps.gz
- Vorlesung am 12.02.03 (Dynamic Logic, Teil 1)
-
folien25.ps.gz
- Vorlesung am 13.02.03 (Dynamic Logic, Teil 2)
-
folien26.ps.gz
- Vorlesung am 20.02.03 (Dynamic Logic, Teil 3)
Ü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.
-
1.
Übungsblatt - Formalisierung in Aussagenlogik, Prädikatenlogik
und Modallogik
Weitere Materialien
Bernhard Beckert