up: Publications

Rule-level verification of graph transformations for invariants based on edges' transitive closure

Christian Percebois, Martin Strecker, Hanh Nhi Tran

SEFM 2013



 
 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