Accéder directement au contenu Accéder directement à la navigation
Communication dans un congrès

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

Hanh Nhi Tran 1 Christian Percebois 2
1 Lab-STICC_ENSTAB_CACS_MOCS ; IDM
Lab-STICC - Laboratoire des sciences et techniques de l'information, de la communication et de la connaissance (UMR 3192), STIC - Pôle STIC [Brest]
2 IRIT-MACAO - Modèles, Architectures, Composants, Agilité et prOcessus
IRIT - Institut de recherche en informatique de Toulouse
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.
Type de document :
Communication dans un congrès
Liste complète des métadonnées

Littérature citée [18 références]  Voir  Masquer  Télécharger

https://hal-ensta-bretagne.archives-ouvertes.fr/hal-00690923
Contributeur : Annick Billon-Coat <>
Soumis le : lundi 4 juin 2012 - 09:55:29
Dernière modification le : mercredi 24 juin 2020 - 16:19:28
Archivage à long terme le : : mercredi 5 septembre 2012 - 02:16:16

Fichier

PID2249161.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : hal-00690923, version 1

Citation

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

Partager

Métriques

Consultations de la notice

472

Téléchargements de fichiers

663