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

    33 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 languageUndefined
    Place of PublicationEnschede
    PublisherCentre for Telematics and Information Technology (CTIT)
    Number of pages54
    Publication statusPublished - Oct 2012

    Publication series

    NameCTIT Technical Report Series
    PublisherCentre 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

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

    }

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

    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 -

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

    Access to Document