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.
Project Team
- Prof. Dr. Holger Giese (contact person)
- Prof. Dr. Jürgen Dingel (Mercator Fellow)
- Dr. Leen Lambers
- Sven Schneider
Former Team Members:
- Basil Becker
- Thomas Beyhl
- Johannes Dyck
- Stephan Hildebrandt
- Stefan Neumann
- Andreas Seibel
- Thomas Vogel
Former Students:
- Stefanie Birth
- Dominic Petrick
- Ingo Richter
- Johann Schmidt (summer term 2010)
Project Partner
- System Analysis and Modeling
Hasso Plattner Institut for Software Systems Engineering
Prof. Dr. Holger Giese - Software Engineering for Embedded Systems
Technical University Berlin
Prof. Dr. Sabine Glesner
Project Funding
This project is financed by the DFG.
Duration of funding:
- Begin: 01.01.2010
- End: 31.12.2012
Duration of funding of continuation phase:
- Begin: 01.08.2013
- End: 31.07.2015
Duration of funding of second continuation phase:
- Begin: 01.11.2017
- End: 31.10.2018
Publications:
see research page
Used mdelab.de Software:
- TGG Interpreter
- Invariant Checker
Used external Software:
- Eclipse (http://www.eclipse.org/)
- AGG (http://www.tfs.cs.tu-berlin.de/AGG)
- JaMoPP (http://www.jamopp.org/index.php/JaMoPP)
- EclEmma (http://www.eclemma.org/)
Software usage scenarios:
- The TGG Interpreter is used to perform model transformations specified in the corresponding TGG editor.
- The Invariant Checker is used to analyze syntactical and semantical correctness of model transformations on the transformation level.
- AGG is used to analyze uniqueness of model transformation results on the transformation level.