TY  - JOUR
A1  - Dyck, Johannes
A1  - Giese, Holger
A1  - Lambers, Leen
T1  - Automatic verification of behavior preservation at the transformation level for relational model transformation
T2  - Software and systems modeling
N2  - The correctness of model transformations is a crucial element for model-driven engineering of high-quality software. In particular, behavior preservation is an important correctness property avoiding the introduction of semantic errors during the model-driven engineering process. Behavior preservation verification techniques show some kind of behavioral equivalence or refinement between source and target model of the transformation. Automatic tool support is available for verifying behavior preservation at the instance level, i.e., for a given source and target model specified by the model transformation. However, until now there is no sound and automatic verification approach available at the transformation level, i.e., for all source and target models. In this article, we extend our results presented in earlier work (Giese and Lambers, in: Ehrig et al (eds) Graph transformations, Springer, Berlin, 2012) and outline a new transformation-level approach for the sound and automatic verification of behavior preservation captured by bisimulation resp.simulation for outplace model transformations specified by triple graph grammars and semantic definitions given by graph transformation rules. In particular, we first show how behavior preservation can be modeled in a symbolic manner at the transformation level and then describe that transformation-level verification of behavior preservation can be reduced to invariant checking of suitable conditions for graph transformations. We demonstrate that the resulting checking problem can be addressed by our own invariant checker for an example of a transformation between sequence charts and communicating automata.
KW  - Relational model transformation
KW  - Formal verification of behavior preservation
KW  - Behavioral equivalence and refinement
KW  - Bisimulation and simulation
KW  - Graph transformation
KW  - Triple graph grammars
KW  - Invariant checking
Y1  - 2018
UR  - https://publishup.uni-potsdam.de/frontdoor/index/index/docId/48122
SN  - 1619-1366
SN  - 1619-1374
VL  - 18
IS  - 5
SP  - 2937
EP  - 2972
PB  - Springer
CY  - Heidelberg
ER  -