Graph abstraction and abstract graph transformations (Amended version)

I.B. Boneva; Jörg Kreiker; M.E. Kurban; Arend Rensink; Eduardo Zambon

Graph abstraction and abstract graph transformations (Amended version)

I.B. Boneva, Jörg Kreiker, M.E. Kurban, Arend Rensink, Eduardo Zambon

Research output: Book/Report › Report › Professional

38 Downloads (Pure)

Abstract

Many important systems such as concurrent heap-manipulating programs, communication networks, or distributed algorithms, are hard to verify due to their inherent dynamics and unboundedness. Graphs are an intuitive representation for the states of these systems, where transitions can be conveniently described by graph transformation rules. We present a framework for the abstraction of graphs supporting abstract graph transformation. The abstraction method naturally generalises previous approaches to abstract graph transformation. The set of possible abstract graphs is finite. This has the pleasant consequence of generating a finite transition system for any start graph and any finite set of transformation rules. Moreover, abstraction preserves a simple logic for expressing properties on graph nodes. The precision of the abstraction can be adjusted according to the properties expressed in this logic that are to be verified.

Original language	Undefined
Place of Publication	Enschede
Publisher	Centre for Telematics and Information Technology (CTIT)
Number of pages	54
Publication status	Published - Oct 2012

Publication series

Name	CTIT Technical Report Series
Publisher	Centre for Telematics and Information Technology, University of Twente
No.	TR-CTIT-12-26
ISSN (Print)	1381-3625

Keywords

IR-84368
System Verification
Graph Abstraction
GROOVE
METIS-289767
EWI-22466
Graph Transformation

Access to Document

neigh_abs_tech_rep
open
neigh_abs_tech_rep
open

Cite this

Boneva, I. B., Kreiker, J., Kurban, M. E., Rensink, A., & Zambon, E. (2012). Graph abstraction and abstract graph transformations (Amended version). (CTIT Technical Report Series; No. TR-CTIT-12-26). Enschede: Centre for Telematics and Information Technology (CTIT).

@book{2ed3f0ef7f4d4e3c90bc1203b4c0d227,

title = "Graph abstraction and abstract graph transformations (Amended version)",

abstract = "Many important systems such as concurrent heap-manipulating programs, communication networks, or distributed algorithms, are hard to verify due to their inherent dynamics and unboundedness. Graphs are an intuitive representation for the states of these systems, where transitions can be conveniently described by graph transformation rules. We present a framework for the abstraction of graphs supporting abstract graph transformation. The abstraction method naturally generalises previous approaches to abstract graph transformation. The set of possible abstract graphs is finite. This has the pleasant consequence of generating a finite transition system for any start graph and any finite set of transformation rules. Moreover, abstraction preserves a simple logic for expressing properties on graph nodes. The precision of the abstraction can be adjusted according to the properties expressed in this logic that are to be verified.",

keywords = "IR-84368, System Verification, Graph Abstraction, GROOVE, METIS-289767, EWI-22466, Graph Transformation",

author = "I.B. Boneva and J{\"o}rg Kreiker and M.E. Kurban and Arend Rensink and Eduardo Zambon",

year = "2012",

month = "10",

language = "Undefined",

series = "CTIT Technical Report Series",

publisher = "Centre for Telematics and Information Technology (CTIT)",

number = "TR-CTIT-12-26",

address = "Netherlands",

}

TY - BOOK

T1 - Graph abstraction and abstract graph transformations (Amended version)

AU - Boneva, I.B.

AU - Kreiker, Jörg

AU - Kurban, M.E.

AU - Rensink, Arend

AU - Zambon, Eduardo

PY - 2012/10

Y1 - 2012/10

N2 - Many important systems such as concurrent heap-manipulating programs, communication networks, or distributed algorithms, are hard to verify due to their inherent dynamics and unboundedness. Graphs are an intuitive representation for the states of these systems, where transitions can be conveniently described by graph transformation rules. We present a framework for the abstraction of graphs supporting abstract graph transformation. The abstraction method naturally generalises previous approaches to abstract graph transformation. The set of possible abstract graphs is finite. This has the pleasant consequence of generating a finite transition system for any start graph and any finite set of transformation rules. Moreover, abstraction preserves a simple logic for expressing properties on graph nodes. The precision of the abstraction can be adjusted according to the properties expressed in this logic that are to be verified.

AB - Many important systems such as concurrent heap-manipulating programs, communication networks, or distributed algorithms, are hard to verify due to their inherent dynamics and unboundedness. Graphs are an intuitive representation for the states of these systems, where transitions can be conveniently described by graph transformation rules. We present a framework for the abstraction of graphs supporting abstract graph transformation. The abstraction method naturally generalises previous approaches to abstract graph transformation. The set of possible abstract graphs is finite. This has the pleasant consequence of generating a finite transition system for any start graph and any finite set of transformation rules. Moreover, abstraction preserves a simple logic for expressing properties on graph nodes. The precision of the abstraction can be adjusted according to the properties expressed in this logic that are to be verified.

KW - IR-84368

KW - System Verification

KW - Graph Abstraction

KW - GROOVE

KW - METIS-289767

KW - EWI-22466

KW - Graph Transformation

M3 - Report

T3 - CTIT Technical Report Series

BT - Graph abstraction and abstract graph transformations (Amended version)

PB - Centre for Telematics and Information Technology (CTIT)

CY - Enschede

ER -