@article{DyckGieseLambers2019,
  author    = {Dyck, Johannes and Giese, Holger and Lambers, Leen},
  title     = {Automatic verification of behavior preservation at the transformation level for relational model transformation},
  series = {Software and systems modeling},
  volume    = {18},
  journal   = {Software and systems modeling},
  number    = {5},
  publisher = {Springer},
  address   = {Heidelberg},
  issn      = {1619-1366},
  doi       = {10.1007/s10270-018-00706-9},
  pages     = {2937 -- 2972},
  year      = {2019},
  abstract  = {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.},
  language  = {en}
}
@book{DyckGieseLambers2017,
  author    = {Dyck, Johannes and Giese, Holger and Lambers, Leen},
  title     = {Automatic verification of behavior preservation at the transformation level for relational model transformation},
  number    = {112},
  publisher = {Universit{\"a}tsverlag Potsdam},
  address   = {Potsdam},
  isbn      = {978-3-86956-391-6},
  issn      = {1613-5652},
  url       = {http://nbn-resolving.de/urn:nbn:de:kobv:517-opus4-100279},
  publisher      = {Universit{\"a}t Potsdam},
  pages     = {viii, 112},
  year      = {2017},
  abstract  = {The correctness of model transformations is a crucial element for model-driven engineering of high quality software. In particular, behavior preservation is the most important correctness property avoiding the introduction of semantic errors during the model-driven engineering process. Behavior preservation verification techniques either show that specific properties are preserved, or more generally and complex, they show some kind of behavioral equivalence or refinement between source and target model of the transformation. Both kinds of behavior preservation verification goals have been presented with automatic tool support for the instance level, i.e. for a given source and target model specified by the model transformation. However, up until now there is no automatic verification approach available at the transformation level, i.e. for all source and target models specified by the model transformation. In this report, we extend our results presented in [27] and outline a new sophisticated approach for the automatic verification of behavior preservation captured by bisimulation resp. simulation for model transformations specified by triple graph grammars and semantic definitions given by graph transformation rules. In particular, we show that the behavior preservation problem can be reduced to invariant checking for graph transformation and that the resulting checking problem can be addressed by our own invariant checker even for a complex example where a sequence chart is transformed into communicating automata. We further discuss today's limitations of invariant checking for graph transformation and motivate further lines of future work in this direction.},
  language  = {en}
}