Entwicklung objektorientierter Software mit formalen Methoden
Praktikum im Wintersemester 2004/2005
Dr. Bernhard Beckert
Vladimir Klebanov
 |
| 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.
Aktuelle Informationen
- Termin: jeweils Dienstag 14.00 Uhr, Raum N.N.
Allgemeine Informationen
Im Praktikum soll ein Projekt durchgeführt werden, dass alle Phasen
und Arbeitsgänge der Softwareentwicklung 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. Anwendungsbeispiel wird die Software für einen Geldautomaten sein.
Dabei setzen Sie professionelle Entwicklungswerkzeuge ein, wie z.B.
das UML-Werkzeug (CASE Tool) Borland
Together ControlCenter. Für die formalen Aspekte kommt eine im
Rahmen des KeY Projektes entwickelte
Erweiterung dieses Werkzeuges zum Einsatz.
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.
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.
Die notwendigen Kenntnisse werden am Anfang des Praktikums in einem
theoretischen Teil vermittelt. Zu den einzelnen Einheiten gibt es korrigierte
und besprochene Übungsaufgaben.
Voraussetzung zur Teilnahme sind Grundkenntnisse in Softwaretechnik (insebesondere UML) und Logik.
Kriterien für den Scheinerwerb
-
Anwesenheit und aktive Mitarbeit bei den offiziellen Terminen
-
Bearbeiten der Übungsblätter (die
Übungsblätter sind
zu bearbeiten und abzugeben; ein ernsthaftes Bemühen, die Aufgaben
zu lösen, muss erkennbar sein)
-
Erfolgreiche Bearbeitung des Abschlussprojekts (einschließlich einer schriftlichen Dokumentation und einer mündlichen Präsentation).
Anmeldung und Vorbesprechung
Die Teilnehmerzahl ist auf 12 begrenzt. Eine Anmeldung vor der
Vorbesprechung ist nicht unbedingt erforderlich. Sie können an der
Vorbesprechung unverbindlich teilnehmen, um sich zunächst genauer über
den Inhalt des Praktikums zu informieren. Sollten die Praktikumsplätze
allerdings nicht ausreichen, dann werden sie in der Reihenfolge der
Anmeldung vergeben.
Materialien
Folien, Übungsblätter, Lösungen
03.11.04: 1. Veranstaltung:
- 1. Übungsblatt (PDF)
- Folien zur 1. Veranstaltung: Einführung
in UML (gzipped PostScript)
16.11.04: 3. Veranstaltung:
30.11.04: 5. Veranstaltung:
7.12.04: 6. Veranstaltung:
4.1.05: 8. Veranstaltung:
27.01.05: 11. Veranstaltung:
Weitere Materialien
Bernhard Beckert