Masterarbeit "Verifikation von Eclipse EMF-Transformationen"

PETE-Framework

18.02.2010, Abschlussarbeiten, Bachelor- und Masterarbeiten

Im Rahmen der Master-/Diplomarbeit soll mittels des Theorem-Beweisers Isabelle eine Verifikationsunterstütztung für das Eclipse-Plugin PETE (http://www4.in.tum.de/~schaetz/PETE/PETEFrame.html) für Modelltransformationen realisiert werden.

Zur Unterstützung der modellbasierten Entwicklung erlaubt das Eclipse-Plugin PETE (http://www4.in.tum.de/~schaetz/PETE/PETEFrame.html), EMF-Modelle mittels deklarativ-relationaler Regeln zu transformieren. Wegen der umfangreichen stereotypen Veränderung von Modellen mittels Modelltransformation ist hier die Korrektheit von Transformationen von besonderem Interesse.

Im Rahmen der Master-/Diplomarbeit soll daher mittels des Theorem-Beweisers Isabelle eine Verifikationsunterstütztung für Modelltransformationen realisiert werden. Dies umfasst im Einzelnen:
• Implementierung einer Übersetzung von EMF-Modellen und Transformationen in entsprechende Isabelle-Theorien
• Entwicklung von geeigneten Lemmata für Basisoperatoren (z.B. für union etc)
• Übersetzung von OCL-Properties in Isabelle-HOL
Darüber hinaus soll die realisierte Unterstützung anhand eines Beispiels – unter Verwendung möglichst generischer Proof-Templates in Isar – demonstriert werden.
Die Arbeit wird gemeinsam durch den Lehrstuhl für Software & Systems Engineering sowie durch die fortiss GmbH betreut. fortiss ist ein An-Institut der TU München mit enger Anbindung an den Lehrstuhl.

Kontakt: schaetz@fortiss.org

Mehr Information

http://dav.informatik.tu-muenchen.de/search/arbeit.php?arbeitID=709&id=32&PHPSESSID=