DoubleCheck: Semantikerhaltende Modelltransformationen

Ziel des Projektes ist es, UML Aktivitäten semantikerhaltend in die Programmiersprache TAAL zu transformieren. Semantikerhaltend heißt in diesem Zusammenhang, dass Aktionen der Aktivität im TAAL-Programm dem Aufruf von Methoden entsprechen; diese sollen in der gleichen Reihenfolge aufgerufen werden wie die Aktionen der Aktivität.

Teilnehmer: Gregor Engels, Arend Rensink, Maria Semenyak, Christian Soltenborn, Heike Wehrheim

Kontaktperson: 

Maria Semenyak

Beschreibung:

Modelltransformationen sind ein wichtiger Teil des von der OMG proklamierten Model Driven Development (MDD). Die wichtigste Charakteristik einer Modelltransformation ist die Überführung eines Ausgangsmodells in ein Zielmodell (welches nicht über das gleiche Metamodell wie das Ausgangsmodell verfügen muss). Die Transformation wird dabei auf der Metamodell-Ebene definiert.

Ziel des DoubleCheck-Projektes ist die Entwicklung einer Modelltransformation, die beweisbar bestimmten Anforderungen genügt. Dabei dient eine Aktivität als Ausgangsmodell, das Zielmodell ist ein TAAL-Programm. TAAL ist eine an der Universität Twente entwickelte Programmiersprache, deren Semantik auf Graphtransformationsregeln basiert. In unserer Arbeitsgruppe wurde eine ebenfalls auf Graphtransformationen basierende Semantik für Aktivitäten entwickelt (siehe DMM). 

Die zu entwickelnde Transformation übersetzt die Aktionen einer Aktivität in Methodenaufrufe von TAAL. Wir wollen nun beweisen, dass im resultierenden TAAL-Programm die Methoden in der gleichen Reihenfolge ausgeführt werden wie die Aktionen in der Aktivität. Voraussetzung für den Beweis ist natürlich eine formale Spezifikation der Transformation, die deshalb als Menge von Graphtransformationsregeln definiert wird.


Werkzeuge: GROOVE


Verwandte Forschungsthemen: Dynamic Meta Modeling (DMM)