Specification and Analysis of Model Transformations by Model Transformation Units

• Applicant: Professor Dr. Hans-Jörg Kreowski
• Subject Area: Theoretical Computer Science
• Term: from 2013 to 2016
• Project identifier: Deutsche Forschungsgemeinschaft (DFG) - Project number 233031177

The project "Specification and Analysis of Model Transformations by Model Transformation Units" aims to develop, systematically investigate and prototypically implement the recently introduced concept of model transformation units. To that end, the notion of graph transformation units serves as a starting point. Graph transformation units have been developed over the last 15 years in the research group of the applicant for the rule-based modeling and analysis of computation processes on graphs. Graph transformation units were recently generalized to model transformation units by allowing the inclusion of not only the visual and diagrammatic components of models which may be suitably represented by graphs, but also non-visual components such as strings, numbers, vectors, matrices, formulas, terms and sets. Models are defined as tuples over graphs and objects of various other data types. While the transformation of graph components is done via graph transformation rules, non-graph components are transformed via suitable operations on their data types. This new approach to model transformation covers both the approaches that build directly on graphs and diagrams, including the concept of Model Driven Architecture on the basis of UML diagrams which is prevalent in software engineering, and also many examples of model transformations from theoretical computer science, such as the translation of automata into grammars or the notion of reduction in computability and complexity theory. Key concepts in model transformation such as termination, confluence, functionality, efficiency, deadlock-freeness and correctness are to be explored. Since such properties are undecidable in general, the goal is to find sufficient conditions or to carry over respective conditions known from the literature to model transformation units. One particular aim is to use the many positive experiences gained from correctness proofs for model transformations in the area of theoretical computer science to derive general proof principles.For the prototypical implementation we plan to expand the graph transformation system GrGen.NET, which has proven to be highly flexible and runs very fast, in such a way that non-graph components of a model may be suitably transformed alongside its graph components. Moreover, it shall be examined how the verification of the correctness of model transformation units can be supported by the use of a model checker such as GROOVE or a SAT solver like MiniSAT.

• DFG Programme: Research Grants