Logik und Formale Methoden

Formale Entwicklung objektorientierter Software (WS 09/10)

Ist fehlerfreie Software möglich?

Wenn Sie die Antwort auf diese Frage interessiert und Sie schon immer einmal Software 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). Für die Implementierung verwenden wir Java, zum Spezifizieren EventB und die Java Modeling Language (JML). Als Verifikationswerkzeuge werden z. B. Rodin, ESC/Java2, JMLUnit, der JML Runtime Assertion Checker (RAC) und KeY eingesetzt

Der in der Vorlesung “Formale Systeme” behandelte Stoff sowie Programmierkenntnisse werden vorausgesetzt. Kenntnisse aus der Vorlesung “Softwaretechnik” sind von Vorteil. In der parallel laufenden Vorlesung “Spezifikation und Verifikation von Software” werden die notwendigen theoretischen Grundlagen zum Praktikum vermittelt. Zu den einzelnen Einheiten gibt es korrigierte und besprochene Übungsaufgaben.

Die Vorbesprechung findet am Mittwoch, dem 28.10.2009 um 17:30 in SR301 statt. Das Praktikum findet im Wintersemester 2009/10 erstmalig in einer gründlich überarbeiteten und neu konzipierten Form statt.

Aufgaben