Formale Entwicklung objektorientierter Software

Praktikum im SS 2001

Die Modellierung von Software in einer geeigneten Modellierungssprache (z.B. UML) gehört schon seit langem zu einer grundlegenden Technik des Software-Engineerings. Eine abstraktere Sichtweise auf die zu entwickelnde Software erlaubt eine elegante Strukturierung, die zu übersichtlichem Implementationscode führt. Die Kunst bei der Anwendung dieser Technik besteht im Finden des geeigneten Abstraktionsniveaus in der Modellierung.

Unter formalen Methoden verstehen wir die Anreicherung von UML-Modellierungen um weitere Informationen (Constraints) in einem dafür vorgesehenen Formalismus (Object Constraint Language, OCL). Der systematische Einsatz dieser Technik erlaubt die Entwicklung von "korrektem" Implementationscode, d.h. die Entwicklung eines solchen Programms, für das gewünschte Eigenschaften (mit vertretbarem Aufwand) verifizierbar sind.

Im Praktikum wird eine Bank-Anwendung ausgehend von einer informellen Beschreibung zunächst modelliert und darauf aufbauend anschliessend in Java implementiert.Um letztendlich den Implementationscode auch verifizieren zu können, besteht die Kunst darin, die Constraints sehr sorgfältig und detailreich zu entwickeln.

Die Modellierung und Implementierung erfolgt unter Nutzung des kommerziellen UML-Werkzeugs TOGETHER. Ebenfalls kommt eine im Rahmen des KeY-Projektes entwickelte Erweiterung dieses Werkzeugs zum Einsatz, womit die deduktive Behandlung von OCL-Constraints ermöglicht wird.

Anmeldung: bei Frau Heck (Sekretariat), Geb. 50.34, Raum 321

Teilnehmerzahl: max. 12

Vorbesprechung: Mittwoch, 25. April 2001, Raum 301, 13:00 Uhr

Informationen: Th. Baar (Raum 306)