Spezifikation und Analyse von Modelltransformationen mit Hilfe von Modelltransformationseinheiten

• Antragsteller: Professor Dr. Hans-Jörg Kreowski
• Fachliche Zuordnung: Theoretische Informatik
• Förderung: Förderung von 2013 bis 2016
• Projektkennung: Deutsche Forschungsgemeinschaft (DFG) - Projektnummer 233031177

In dem Projekt "Spezifikation und Analyse von Modelltransformationen mit Hilfe von Modelltransformationseinheiten" soll das Konzept der Modelltransformationseinheiten theoretisch fundiert weiterentwickelt, systematisch untersucht und prototypisch implementiert werden. Ausgangspunkt ist das in den letzten 15 Jahren in der Forschungsgruppe des Antragstellers entwickelte Konzept der Graphtransformationseinheiten, mit denen sich Berechnungsprozesse auf Graphen regelbasiert modellieren und analysieren lassen. Graphtransformationseinheiten sind kürzlich zu Modelltransformationseinheiten verallgemeinert worden, indem zu den visuellen und diagrammatischen Komponenten von Modellen, die adäquat durch Graphen dargestellt werden, nichtgraphische Komponenten wie Wörter, Zahlen, Vektoren, Matrizen, Formeln, Terme und Mengen hinzugenommen werden können. Modelle sind deshalb Tupel aus Graphen und Objekten anderer Datentypen, bei deren Transformation Graphkomponenten mit Hilfe von Graphtransformationsregeln und andere Komponenten mit entsprechenden Datentypoperationen bearbeitet werden. Dieser neue Zugang zur Modelltransformation deckt sowohl alle Ansätze ab, die direkt auf Graphen und Diagrammen aufbauen, einschließlich der in der Softwaretechnik propagierten modellgetriebenen Architektur auf der Basis von UML-Diagrammen als auch viele Beispiele von Modelltransformationen in der Theoretischen Informatik wie die Übersetzung von Automaten in Grammatiken oder den Reduktionsbegriff in der Berechenbarkeits- und Komplexitätstheorie.Untersucht werden sollen Schlüsseleigenschaften von Modelltransformationen wie Termination, Konfluenz, Funktionalität, Effizienz, Sackgassenfreiheit und Korrektheit. Da solche Eigenschaften im Allgemeinen unentscheidbar sind, geht es darum, brauchbare hinreichende Bedingungen zu finden bzw. die in der Literatur bekannten auf Modelltransformationseinheiten zu übertragen. Insbesondere wird beabsichtigt, die vielen guten Einzelerfahrungen mit Korrektheitsbeweisen für Modelltransformationen in der Theoretischen Informatik aufzugreifen und allgemeine Beweisprinzipien daraus abzuleiten.Für die prototypische Implementierung ist geplant, das Graphtransformationssystem GrGen.NET, das sich durch hohe Flexibilität und gutes Laufzeitverhalten auszeichnet, so zu erweitern, dass auch die Komponenten, die keine Graphen sind, geeignet transformiert werden. Darüber hinaus soll erprobt werden, wie Beweissysteme für die Verifikation von Modelltransformationseinheiten genutzt werden können. Dabei ist insbesondere an den Einsatz eines Modelchecker wie GROOVE und eines SAT-Solver wie MiniSAT gedacht.

• DFG-Verfahren: Sachbeihilfen