id: 06089215
dt: a
an: 06089215
au: Giese, Holger; Lambers, Leen
ti: Towards automatic verification of behavior preservation for model
    transformation via invariant checking.
so: Ehrig, Hartmut (ed.) et al., Graph transformations. 6th international
    conference, ICGT 2012, Bremen, Germany, September 24‒29, 2012.
    Proceedings. Berlin: Springer (ISBN 978-3-642-33653-9/pbk). Lecture
    Notes in Computer Science 7562, 249-263 (2012).
py: 2012
pu: Berlin: Springer
la: EN
cc: 
ut: 
ci: 
li: doi:10.1007/978-3-642-33654-6_17
ab: Summary: 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 bisimulation 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 paper, we present a first approach towards
    automatic behavior preservation verification 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. We discuss today’s limitations of invariant checking
    for graph transformation and motivate further lines of future work in
    this direction.
rv: