Praxis der Softwareentwicklung (PSE)

Aufgabenbeschreibung

Ziel des Projektes ist die Entwicklung eines graphischen Editors für Contract Automata. Contract Automata sind ein an unserer Forschungsgruppe entwickelter Formalismus zur Spezifikation sogennanter Reaktiver Systeme, wie etwa Steuergeräten in Autos oder wobei die Zustandsübergänge von formalen Verträgen abgesichert werden. Interesse für die formalen Hintergründe ist willkommen, aber nicht notwendig. Entwickelt werden soll eine Desktopanwendung zum Visualisieren und Bearbeiten der Contract Automata. Die folgenden Features stehen dabei im Mittelpunkt:

Anforderungen

• Erstellen und Bearbeiten der Automaten, Platzierung von Zuständen, Übergängen (Kanten), Verträgen an den Kanten. Manuelle Platzierung muss möglich sein, ein automatisches Graph-Layouting ist aber auch denkbar.
• Übersichtliche Darstellung und gute Performance auch bei sehr großen Contract Automata mit vielen Zuständen und Übergängen und langen Verträgen.
• Für die Contract Automata haben wir schon ein textbasiertes Dateiformat. Die Anwendung muss in der Lage sein, diese Dateien zu laden und zu speichern.
• Mit Contract Automata spezifizieren wir große und modulare Systeme aus mehreren Teilsystemen, die miteinander verbunden sind. Die Anwendung soll daher in der Lage sein, auch ein System aus mehreren Contract Automata und wie diese miteinander Interagieren zu verwalten.

Technischer Rahmen

• Als Programmiersprache und Framework soll Java mit JavaFX verwendet werden. Anderen Technologien stehen wir aber prinzipiell offen gegenüber.
• Das Projekt wird angeboten vom FZI Forschungszentrum Informatik zusammen mit der Forschungsgruppe für Anwendungsorientierte formale Verifikation am KIT.