AktuellModellgetriebene Generierung eines formalen Modells zur Verifikation sicherheitskritischer Anwendungen
Ansprechpartner: Nina Moebius
Ausgangssituation:
Die Arbeit bettet sich ein in das Projekt SecureMDD, dessen Ziel die modellgetriebene Entwicklung sicherheitskritscher Anwendungen ist. Hier soll, aus einem gemeinsamen plattformunabhängigen UML-Modell der Anwendung, zum einen eine lauffähige Implementierung sowie ein formales Modell mittels Model-zu-Modell (M2M) sowie Modell-zu-Text (M2T) Transformationen erzeugt werden. Das generierte formale Modell soll anschließend in das Beweissystem KIV eingelesen werden und dort die Verifikation von Sicherheitseigenschaften ermöglichen.
Ziel der Arbeit:
In dieser Arbeit soll, basierend auf dem plattformunabhängigen UML Modell, ein plattformspezifisches UML-Modell für die formale Spezifikation entworfen werden. Im Anschluss sollen die für die Generierung des PSMs sowie des formalen Modells benötigten M2M und M2T Transformationen implementiert und validiert werden. Die verwendeten Sprachen sind QVT und XPand. Die Struktur und der Aufbau des formalen Modells sind bereits vorhanden und somit nicht Teil der Aufgabenstellung.
Voraussetzungen:
- Grundkenntnisse im Bereich modellgetriebene Softwareentwicklung
- Kenntnisse im Bereich formaler Methoden / Lehrveranstaltung Beweisbar korrekte Software
Zeitrahmen:
Beginn: ab Oktober