Vorlesung im WS02/03 (KITE und ST): Formale Spezifikation und Verifikation von Software
Bernhard Beckert
ich möchte noch einmal auf die folgende Vorlesung hinweisen, die sich
gleichermaßen an Studenten der beiden Vertiefungsrichtungen "Künstliche
Intelligenz" und "Softwaretechnik" richtet.
Formale Spezifikation und Verifikation von Software
Vorlesung im Wintersemester 2002/2003 (drei SWS)
Dr. Bernhard Beckert
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, 15-16 Uhr, MK101 und
Donnerstags, 12-14 Uhr, MK114
Erstmals am Mittwoch, dem 06.11.02
Weitere Informationen: Bernhard Beckert (bec...@uni-koblenz.de)
http://i12www.ira.uka.de/~beckert/Lehre/Spezifikation-Verifikation/
--
+-------------------------------------------------------------+
| Bernhard Beckert, WWW: http://www.uni-koblenz.de/~beckert/ |
+-------------------------------------------------------------+