2012 IEEE Fifth International Conference on Software Testing, Verification and Validation (2012)

Montreal, Quebec Canada

Apr. 17, 2012 to Apr. 21, 2012

ISBN: 978-0-7695-4670-4

pp: 946-953

DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/ICST.2012.200

ABSTRACT

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.

INDEX TERMS

verification of graph transformations, property-preserving graph grammar, theorem proving, Isabelle/HOL

CITATION

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.

doi:10.1109/ICST.2012.200

CITATIONS