Towards Automatic Verification of Behavior Preservation for Model Transformation via Invariant Checking (bibtex)
Reference:
Holger Giese and Leen Lambers, "Towards Automatic Verification of Behavior Preservation for Model Transformation via Invariant Checking", in Hartmut Ehrig, Gregor Engels, Hans Kreowski, Grzegorz Rozenberg, Eds., Proceedings of Intern. Conf. on Graph Transformation (ICGT' 12), vol. 7562 of LNCS, pp. 249-263, Springer, 2012.
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 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.
Links:
Copyright notice: This material is presented to ensure timely dissemination of scholarly and technical work. Copyright and all rights therein are retained by authors or by other copyright holders. All persons copying this information are expected to adhere to the terms and constraints invoked by each author's copyright. In most cases, these works may not be reposted without the explicit permission of the copyright holder.
Powered by bibtexbrowser