Masterarbeit: Automatisierte Konformitätsprüfung von MontiArc-Modellen zu Referenzmodellen

Hintergrund

Ein Referenzmodell ist ein abstraktes, normatives Modell, in einer gegebenen Modellierungssprache, welches Domänenkonzepte und deren Relationen kodiert und festlegt, welche Eigenschaften ein konformes konkretes Modell haben muss, insbesondere welche Elemente notwendig sind und in welcher Relation sie zueinander stehen müssen [KMR24,KRS+24]. In der modellbasierten Entwicklung können Referenzmodelle als Vorlage zur Modellierung und Entwicklung von Systemen für eine Klasse konkreter Szenarien dienen.

Konformität zu einem Referenzmodell ist über eine Konformitätsrelation spezifiziert, welche für eine gegebene Modellierungssprache definiert wird. Allerdings soll als notwendige Bedingung der Konformität das konkrete Modell das Referenzmodell unter “Inkarnation” semantisch verfeinern. Inkarnationen sind dabei Elemente des konkreten Modells, welche Elemente des Referenzmodells im konkreten Modell repräsentieren, dabei aber ggf. anders benannt und (de-)komponiert sind. Die Inkarnationen werden dabei entweder mit Hilfe ein explizites Inkarnationsmapping oder über Konvention identifiziert.

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. Semantische Verfeinerung ist dann gegeben, wenn dieses Verhalten präzisiert wird, d.h. durch Reduktion von Unterspezifizierung und Nicht-Determinismus die Menge der erlaubten Ein- uns Ausgabepaare weiter eingeschränkt wird.

Ziel der Masterarbeit

Ziel der Masterarbeit ist es, eine geeignete Konformitätsrelation für MontiArc-Modelle zu definieren, welche semantische Verfeinerung unter Inkarnation garantiert und ggf. notwendige strukturelle Aspekte des Referenzmodells erhält, sowie einen entsprechenden Algorithmus zu entwickeln welcher diese Relation implementiert und automatisierte Konformitätsprüfung ermöglicht. Hierfür soll auch der existierende SMT-basierte Konformitätsansatz für MontiArc-Automaten ausgebaut werden [KRS+24].

Aufgaben

Konzipierung einer umfassenden Konformitätsrelation für MontiArc
Ausbau des existierenden SMT-basierte Konformitätsansatz für MontiArc-Automaten
Entwicklung eines Konzepts zur Konformitätsprüfung bei Automatendekomposition
Entwicklung eines Tools zu automatisierten Konformitätsprüfung für MontiArc-Modelle

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-Solver

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