2015/11/03 by Frank Hermann, Hermann, Frank, Mathias Hülsbusch +3 · 1 citation
Computer Science · #Advanced Software Engineering Methodologies #Model-Driven Software Engineering Techniques #Software Testing and Debugging Techniques
paper · doi:10.14279/tuj.eceasst.30.424
openalex publication_date 2024/03/25 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/15
Model transformations are a key concept within model driven development and there is an enormous need for suitable formal analysis techniques for model transformations, in particular with respect to behavioural equivalence of source models and their corresponding target models. For this reason, we discuss the general challenges that arise for the specification and verification of model transformations and present suitable formal techniques that are based on graph transformation. In this context, triple graph grammars show many benefits for the specification process, e.g. modelers can work on an intuitive level of abstraction and there are formal results for syntactical correctness, completeness and efficient execution. In order to verify model transformations with respect to behavioural equivalence we apply well-studied techniques based on the double pushout approach with borrowed context, for which the model transformations specified by triple graph transformation rules are flattened to plain (in-situ) graph transformation rules. The potential and adequateness of the presented techniques are demonstrated by an intuitive example, for which we show the correctness of the model transformation with respect to bisimilarity of source and target models.