Dieses Praktikum wird im Rahmen des KeY Projektes durchgeführt.
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.
Unter formalen Methoden verstehen wir hier
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.
Das Anwendungsbeispiel wird die Software für einen Geldautomaten sein. Die Modellierung in UML und die Implementierung in Java erfolgt unter Nutzung des kommerziellen UML-Werkzeugs Together Control Center. Zudem kommt eine im Rahmen des KeY-Projektes entwickelte Erweiterung dieses Werkzeugs zum Einsatz, dass die deduktive Behandlung von OCL-Constraints und also die Verifikation der Java-Implementierung ermöglicht.
Die notwendigen Kenntnisse - vor allem im formalen Bereich - werden am Anfang des Praktikums in einem theoretischen Teil vermittelt.Anmeldung: Frau Heck (Sekretariat), Geb. 50.34, Raum 321
Teilnehmerzahl: max. 12
Vorbesprechung: Mittwoch, 16. Oktober 2002, 13:15 Uhr, SR301
Informationen: B. Beckert (Raum 309), M. Giese (Raum 307)