Entwicklung objektorientierter Software mit formalen Methoden
Praktikum im Wintersemester 2003/2004
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
- Regelmäßiger Praktikumstermin ist Dienstags, 18 Uhr, Raum B013.
- Liste: Rechnerausstattung im KI-Labor
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.
Regelmäßiger Praktikumstermin ist Dienstags, 18 Uhr, Raum B013.
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).
Materialien zum Praktikum
Folien, Übungsblätter, Lösungen
07.11.03: 1. Veranstaltung:
- 1. Übungsblatt (PostScript)
- Folien zur 1. Veranstaltung: Einführung
in UML (gzipped PostScript)
18.11.03: 2. Veranstaltung:
25.11.03: 3. Veranstaltung:
- 3. Übungsblatt (PostScript) Abgabe am 1.12.
- Folien zum Thema "Design Patterns" (Entwurfsmuster)
02.12.03: 4. Veranstaltung:
09.12.03: 5. Veranstaltung:
- Rahmenwerk Milliardenbank (Abgabe 15.12.)
- Kein Übungsblatt
13.1.04: 6. Veranstaltung:
20.1.04: 7. Veranstaltung:
27.1.04: 8. Veranstaltung:
- Kein Übungsblatt
- Bitte Code einchecken
3.2.04: 9. Veranstaltung:
10.2.04: 10. Veranstaltung:
Weitere Materialien
Das KeY Tool
Zum Download.
Bernhard Beckert