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. Der Besuch der ebenfalls im Wintersemester 2002/2003 angebotenen Vorlesung "Formale Spezifikation und Verifikation von Software" ist den Praktikumsteilnehmern empfohlen aber nicht notwendig.Voraussetzungen: Grundkenntnisse in Softwaretechnik und Prädikatenlogik.
Zeit und Ort:
Mittwochs, 16 Uhr s.t., MA 203 (weitere Termine nach Vereinbarung)
Anmeldung und weitere Informationen: Bernhard Beckert
Bevor KeY mit der Datei key.jar installiert werden kann, müssen - wie bisher - TogetherCC und die KeY-Libraries vorhanden sein, und Java muß installiert sein. Die Datei key.jar laesst sich unter Windows/Linux mit "java -jar key.jar" ausführen (bzw. unter Windows auch mit einem Doppelklick auf die Datei).