Up to now, except for our own preliminary work, there is not much work available presenting methods for the formal verification of correctness of a transformation described by model transformations based on graph transformation. Using Story Diagrams and Triple Graph Grammars as representatives for operational and relational model transformation approaches based upon graph transformation systems, we want to take advantage of the fact that graph transformation systems are also suitable to specify the semantics of models such that we can tackle the verification problem for model transformations with a single formal model. On this basis an approach will be developed and validated for the methodological development of correct model transformations, containing adequate concepts and algorithms for the formal analysis and verification of model synchronisations, model transformations, and model transformation results; corresponding tooling for the formal verification (automatic and semi-automatic) will be added to the existing tool support for Story Diagrams and Triple Graph Grammars, and a verification routine resp. process for the developer and user perspective will be elaborated. The practicability of the developed methods will be demonstrated on two different case studies (in the automative domain and in mechanical engineering).
During the continuation phase of the CorMorant project, we want to advance the project work in two directions: First, we aim at continuing our research on open theoretical problems. Furthermore, we want to investigate the transfer of project results into practice. Open theoretical problems regard, in particular, the definition of adequate refinement relations for structural models. Important practical issues are the development of an overall approach to ensure the correctness for model transformations, the mapping and creation of relationships with other model transformation, modeling, and programming languages that are of practical importance, as well as the development of a process that can be applied in practice. Furthermore we plan to again evaluate the theoretical as well as practical project results based on case studies.
