Towards a Rule-level Verification Framework for Property-Preserving Graph Transformations

Hanh Nhi Tran (1, 2) , Christian Percebois (3)

1 Lab-STICC_ENSTAB_CACS_MOCS
2 IRIT-ARGOS - Advancing Rigorous Software and System Engineering
3 IRIT-MACAO - Modèles, Architectures, Composants, Agilité et prOcessus

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.

Mots clés: verification of graph transformations; propertypreserving graph grammar; theorem proving; Isabelle/HOL

Domaines: Génie logiciel [cs.SE]

Hanh Nhi Tran, Christian Percebois. Towards a Rule-level Verification Framework for Property-Preserving Graph Transformations. Workshop on Verification and validation Of model Transformations (VOLT 2012) @ ICST 2012 : International Conference on Software Testing, Verification and Validation, IEEE, Apr 2012, Montreal, Canada. ⟨10.1109/ICST.2012.200⟩. ⟨hal-00690923⟩