Abstract
| 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
Cite this
}
Graph abstraction and abstract graph transformations (Amended version). / Boneva, I.B.; Kreiker, Jörg; Kurban, M.E.; Rensink, Arend; Zambon, Eduardo.
Enschede : Centre for Telematics and Information Technology (CTIT), 2012. 54 p. (CTIT Technical Report Series; No. TR-CTIT-12-26).Research output: Book/Report › Report › Professional
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 -