Masterarbeit: Semantische Unterschiedsanalyse bei Dekomposition von MontiArc-Komponenten

Hintergrund

In der modellbasierten Entwicklung von Systemen stellen Modelle die primären Artefakte dar, die sich im Laufe der Entwicklung weiter verändern. Diese Weiterentwicklung muss verifiziert werden, um Fehler frühzeitig zu erkennen und zu beheben. Bei einer Verfeinerung des Modells soll z.B. die bisherige Verhaltensspezifikation erhalten bleiben, d.h. es darf kein Verhalten hinzukommen, das vorher nicht erlaubt war.

MontiArc ist eine Architektursprache bestehend aus Komponenten und Konnektoren, die die Komponenten über Ports verbinden und auf denen Nachrichtenströme fließen. Komponenten verarbeiten Eingabenachrichten und produzieren entsprechende Ausgabenachrichten. Sie können atomar sein oder aus Subarchitekturen bestehen. Das Eingabe- und Ausgabeverhalten einer atomaren MontiArc-Komponente wird durch einen endlichen Automaten spezifiziert. Die Eingaben erhält die Komponente über Eingabeports, Ausgaben werden über Ausgabeports weitergeleitet. Die Semantik einer MontiArc-Komponente ist damit genau ihr Ein- und Ausgabeverhalten.

Ziel der Masterarbeit

Ziel der Masterarbeit ist es, ein Tool zu entwickeln, das bei der Dekomposition von MontiArc-Komponenten semantische Unterschiede im Ein- und Ausgabeverhalten automatisch erkennt. MontiArc-Komponenten können durch Dekomposition verfeinert werden: Eine einzelne Komponente wird durch eine Subarchitektur ersetzt, die das Eingabe- und Ausgabeverhalten der ursprünglichen Komponente beibehält und ggf. weitere Spezifikationen hinzufügt.

Es soll überprüft werden, ob bei dieser Dekomposition die Verfeinerungsbeziehung verletzt wird, d.h. ob ein semantischer Unterschied zwischen dem ursprünglichen und dem dekomponierten Modell besteht. Zu diesem Zweck soll ein Tool zur Semantikanalyse entwickelt werden. Dieses Tool soll die Verhaltensspezifikation der MontiArc-Modelle automatisiert in SMT kodieren und mithilfe eines SMT-Solvers (z.B. Z3) semantische Unterschiede in Form von Ein-/Ausgabe-Traces berechnen.

Aufgaben

Konzipierung einer geeigneten SMT-Kodierung der MontiArc-Modelle für die Semantikanalyse
Implementierung einer automatisierten Übersetzung von MontiArc-Modelle in SMT-Kodierung
Entwicklung eines Tools zur semantischen Unterschiedsanalyse
Evaluation des Tools anhand von geeigneten Beispielmodellen

Wünschenswerte Vorkenntnisse

Erfolgreicher Abschluss der Vorlesungen “Model-Based Software/Systems Engineering” und “Software Language Engineering”
Kenntnisse der Architektursprache “MontiArc” oder weiterer MontiCore-basierter Sprachen
Erfahrung im Umgang mit SMT-Solvern

Ansprechpartner

Für mehr Informationen wenden Sie sich mit ihren Bewerbungsunterlagen bitte an Max Stachon.

Aufgabenstellung:

Prof. Dr. Bernhard Rumpe
Lehrstuhl Software Engineering
Ahornstr. 55
52074 Aachen