Technical Report TR-2006-01

BibliographyKönig, Barbara; Kozioura, Vitali: Counterexample-guided Abstraction Refinement for the Analysis of Graph Transformation Systems.
University of Stuttgart, Faculty of Computer Science, Electrical Engineering, and Information Technology, Technical Report Computer Science No. 2006/01.
25 pages, english.
CR-SchemaF.3.1 (Specifying and Verifying and Reasoning about Programs)
F.4.2 (Grammars and Other Rewriting Systems)
Keywordscounterexample; abstraction; refinement; graph transformation
Abstract

Graph transformation systems are a general specification language for systems with dynamically changing topologies, such as mobile and distributed systems. Although in the last few years several analysis and verification methods have been proposed for graph transformation systems, counterexample-guided abstraction refinement has not yet been studied in this setting.

We propose a counterexample-guided abstraction refinement technique which is based on the over-approximation of graph transformation systems by Petri nets. We show that a spurious counterexample is caused by merging nodes during the approximation. We present a technique for identifying these merged nodes and splitting them using abstraction refinement, which removes the spurious run. The technique has been implemented in the Augur tool and experimental results are discussed.

Full text and
other links
PDF (289110 Bytes)
PostScript (881284 Bytes)
Contactkoziouvi@informatik.uni-stuttgart.de
Department(s)University of Stuttgart, Institute of Formal Methods in Computer Science, Software Reliability and Security
Entry dateFebruary 2, 2006
   Publ. Computer Science