up: Publications |
Abstract |
This paper develops methods to reason about graph transformations, and in
particular to show that transitivity and reachability invariants are preserved
during transformations. In our approach, graph transformations consist of a
pattern defining an applicability condition, and an operational description of
the desired transformation. Whereas previous work was restricted to Boolean
combinations of arc expressions as patterns, we extend the approach to
patterns containing transitive closure operations, which implicitly denote an
unbounded number of nodes. We show how these can be internalized into a
finite pattern graph so that model checking techniques can be applied for
verification.
Online Copy |
Conference version: PDF (preliminary)
BibTeX Entry |
@InProceedings{percebois13:_rule, author = {Christian Percebois and Martin Strecker and Hanh Nhi Tran}, title = {Rule-level verification of graph transformations for invariants based on edges' transitive closure}, pages = {106-121}, ee = {http://dx.doi.org/10.1007/978-3-642-40561-7_8}, url = {http://www.irit.fr/~Martin.Strecker/Publications/sefm2013.html}, editor = {Robert M. Hierons and Mercedes G. Merayo and Mario Bravetti}, booktitle = {Software Engineering and Formal Methods - 11th International Conference, SEFM 2013, Madrid, Spain, September 25-27, 2013. Proceedings}, publisher = {Springer}, series = {Lecture Notes in Computer Science}, volume = {8137}, year = {2013}, isbn = {978-3-642-40560-0} }
Last modified: Sat Apr 20 04:47:24 CEST 2013 |