Praktikum im WS02/03: Entwicklung objektorientierter Software mit formalen Methoden

[Bernhard Beckert]

Auch noch einmal ein Hinweis auf das zur Vorlesung passende Praktikum:

Entwicklung objektorientierter Software mit formalen Methoden
Praktikum im Wintersemester 2002/2003
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.

Unter formalen Methoden verstehen wir hier

* die Anreicherung von UML-Modellierungen um formale Spezifikationen,
wie Klassen-Invarianten und Vor- und Nachbedingungen für Methoden
(formuliert in Object Constraint Language, OCL) und
* den anschließenden formalen Nachweis, dass die entwickelte Software
die Spezifikation erfüllt.

Im Praktikum soll ein Projekt durchgeführt werden, dass alle Phasen und
Arbeitsgänge der Software-Entwicklung mit formalen Methoden umfasst:
Analyse, Modellierung, Spezifikation, Implementierung, Verifikation
(aber auch Dokumentation etc.). Dies geschieht in Gruppenarbeit, so dass
auch die Softwareentwicklung im Team eingeübt wird.

Das Anwendungsbeispiel wird die Software für einen Geldautomaten sein.
Die Modellierung in UML und die Implementierung in Java erfolgt unter
Nutzung des kommerziellen UML-Werkzeugs Together Control Center. Zudem
kommt eine im Rahmen des KeY-Projektes entwickelte Erweiterung dieses
Werkzeugs zum Einsatz, dass die deduktive Behandlung von OCL-Constraints
und also die Verifikation der Java-Implementierung ermöglicht.

Die notwendigen Kenntnisse - vor allem im formalen Bereich - werden am
Anfang des Praktikums in einem theoretischen Teil vermittelt. Der Besuch
der ebenfalls im Wintersemester 2002/2003 angebotenen Vorlesung "Formale
Spezifikation und Verifikation von Software" ist den
Praktikumsteilnehmern empfohlen aber nicht notwendig.

Voraussetzungen: Grundkenntnisse in Softwaretechnik und Prädikatenlogik.

Zeit und Ort:
Mittwochs, 16 Uhr, MA 203 (weitere Termine nach Vereinbarung)
Erstmals am: Mittwoch, 06.11.02
Die erste Veranstaltung ist eine unverbindliche Vorbesprechung.
Allerdings werden die Praktikumsplätze in der Reihenfolge der
Anmeldungen vergeben.

Anmeldung und weitere Informationen: Bernhard Beckert
(bec...@uni-koblenz.de)
http://i12www.ira.uka.de/~beckert/Lehre/Praktikum-Formale-Entwicklung/

--

+-------------------------------------------------------------+
| Bernhard Beckert, WWW: http://www.uni-koblenz.de/~beckert/ |
+-------------------------------------------------------------+