2012 IEEE Fifth International Conference on Software Testing, Verification and Validation (2012)
Montreal, Quebec Canada
Apr. 17, 2012 to Apr. 21, 2012
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/ICST.2012.200
We report in this paper a method for proving that a graph transformation is property-preserving. Our approach uses a relational representation for graph grammar and a logical representation for graph properties with first-order logic formulas. The presented work consists in identifying the general conditions for a graph grammar to preserve graph properties, in particular structural properties. We aim to implement all the relevant notions of graph grammar in the Isabelle/HOL proof assistant in order to allow a (semi) automatic verification of graph transformation with a reasonable complexity. Given an input graph and a set of graph transformation rules, we can use mathematical induction strategies to verify statically if the transformation preserves a particular property of the initial graph. The main highlight of our approach is that such a verification is done without calculating the resulting graph and thus without using a transformation engine.
verification of graph transformations, property-preserving graph grammar, theorem proving, Isabelle/HOL
C. Percebois and H. N. Tran, "Towards a Rule-Level Verification Framework for Property-Preserving Graph Transformations," 2012 IEEE Fifth International Conference on Software Testing, Verification and Validation(ICST), Montreal, Quebec Canada, 2012, pp. 946-953.