Universität Karlsruhe
Institut für Theoretische Informatik
Prof. P. H. Schmitt, Dr. T. Käufl, C. Engel, B. Weiß

Formale Entwicklung objektorientierter Software

Praktikum im Wintersemester 2006/2007


(Die Ariane 5 bei ihrem durch einen Software-Bug jäh beendeten Jungfernflug)

Ist fehlerfreie Software unmöglich?

Wenn Sie die Antwort auf diese Frage interessiert und Sie schon immer einmal Software realitätsnah in einer Gruppe entwickeln wollten, dann ist dieses Praktikum genau das, wonach Sie suchen.

Anhand eines selbst realisierten Software-Projektes lernen Sie in einer Gruppe Aspekte der formalen Software-Entwicklung kennen und anzuwenden, d.h. Analyse, Modellierung, Spezifikation, Implementierung und Verifikation (aber z.B. auch Dokumentation).

Die Implementierung erfolgt in Java, als Spezifikationssprache kommt die Java Modeling Language (JML) zum Einsatz. Mit Hilfe der State-of-the-Art-Verifikationssysteme ESC/Java2 und KeY wird sichergestellt, dass die Implementierung der Spezifikation entspricht.

Die notwendigen Kenntnisse werden am Anfang des Praktikums in einem theoretischen Teil vermittelt. Zu den einzelnen Einheiten gibt es korrigierte und besprochene Übungsaufgaben.

Der in der Vorlesung "Formale Systeme" behandelte Stoff sowie Programmierkenntnisse werden vorausgesetzt. Kenntnisse aus der Vorlesung "Softwaretechnik" sind von Vorteil.

Anmeldung bei Frau Beckert, Geb. 50.34, Raum 321, lbeckert@mail.informatik.kit.edu