Abstract graph transformation theory and practice

Eduardo Zambon

Abstract

The verification of systems with respect to a desired set of behavioural properties is a crucial step in increasing our confidence that these systems will correctly function under all circumstances. Although it would be desirable to verify all (computer) systems that we use in our daily life, the sheer complexity of the verification tasks often limit their application to critical systems. A system is considered critical when its incorrect behaviour can cause severe damage, such as loss of lives or the destruction of valuable equipment. In this thesis, we use graph transformation as our modelling formalism for system specification. Graph transformation (GT) is a Turing-powerful, declarative rule-based formalism, with a mature theoretical foundation and a thriving tool environment. Our work focus on the behavioural analysis of GT systems, where a GT system semantics is represented by a labelled transition system, that can then be analysed by well-established verification methods, such as model checking. A key requirement in this approach is the capability to handle GT systems with (possibly) infinite state spaces. This thesis presents two abstraction techniques that yield a finite over-approximation of the behaviour of infinite-state GT systems, thus enabling verification on the abstract level. The two techniques, called neighbourhood abstraction and pattern abstraction, are discussed under both a theoretical and a practical focus; the former concerning the formal definition and correctness of the abstraction methods, and the latter discussing their implementation in GROOVE, our GT tool set. Experimental results are also given in order to assess the performance of the developed tools.
Original languageEnglish
Awarding Institution
  • University of Twente
Supervisors/Advisors
  • Rensink, Arend , Supervisor
Date of Award24 Jan 2013
Place of PublicationEnschede
Publisher
Print ISBNs978-90-365-3477-2
DOIs
StatePublished - 24 Jan 2013

Fingerprint

Model checking
Computer systems
Semantics
Specifications

Keywords

  • METIS-293491
  • IR-83260

Cite this

Zambon, E. (2013). Abstract graph transformation theory and practice Enschede: Universiteit Twente DOI: 10.3990/1.9789036534772
Zambon, Eduardo. / Abstract graph transformation theory and practice. Enschede : Universiteit Twente, 2013. 152 p.
@misc{d20d2d4948374285a8aac43b9f14c923,
title = "Abstract graph transformation theory and practice",
abstract = "The verification of systems with respect to a desired set of behavioural properties is a crucial step in increasing our confidence that these systems will correctly function under all circumstances. Although it would be desirable to verify all (computer) systems that we use in our daily life, the sheer complexity of the verification tasks often limit their application to critical systems. A system is considered critical when its incorrect behaviour can cause severe damage, such as loss of lives or the destruction of valuable equipment. In this thesis, we use graph transformation as our modelling formalism for system specification. Graph transformation (GT) is a Turing-powerful, declarative rule-based formalism, with a mature theoretical foundation and a thriving tool environment. Our work focus on the behavioural analysis of GT systems, where a GT system semantics is represented by a labelled transition system, that can then be analysed by well-established verification methods, such as model checking. A key requirement in this approach is the capability to handle GT systems with (possibly) infinite state spaces. This thesis presents two abstraction techniques that yield a finite over-approximation of the behaviour of infinite-state GT systems, thus enabling verification on the abstract level. The two techniques, called neighbourhood abstraction and pattern abstraction, are discussed under both a theoretical and a practical focus; the former concerning the formal definition and correctness of the abstraction methods, and the latter discussing their implementation in GROOVE, our GT tool set. Experimental results are also given in order to assess the performance of the developed tools.",
keywords = "METIS-293491, IR-83260",
author = "Eduardo Zambon",
note = "IPA Dissertation Series No. 2013-03",
year = "2013",
month = "1",
doi = "10.3990/1.9789036534772",
isbn = "978-90-365-3477-2",
publisher = "Universiteit Twente",
school = "University of Twente",

}

Zambon, E 2013, 'Abstract graph transformation theory and practice', University of Twente, Enschede. DOI: 10.3990/1.9789036534772

Abstract graph transformation theory and practice. / Zambon, Eduardo.

Enschede : Universiteit Twente, 2013. 152 p.

Research output: ScientificPhD Thesis - Research UT, graduation UT

TY - THES

T1 - Abstract graph transformation theory and practice

AU - Zambon,Eduardo

N1 - IPA Dissertation Series No. 2013-03

PY - 2013/1/24

Y1 - 2013/1/24

N2 - The verification of systems with respect to a desired set of behavioural properties is a crucial step in increasing our confidence that these systems will correctly function under all circumstances. Although it would be desirable to verify all (computer) systems that we use in our daily life, the sheer complexity of the verification tasks often limit their application to critical systems. A system is considered critical when its incorrect behaviour can cause severe damage, such as loss of lives or the destruction of valuable equipment. In this thesis, we use graph transformation as our modelling formalism for system specification. Graph transformation (GT) is a Turing-powerful, declarative rule-based formalism, with a mature theoretical foundation and a thriving tool environment. Our work focus on the behavioural analysis of GT systems, where a GT system semantics is represented by a labelled transition system, that can then be analysed by well-established verification methods, such as model checking. A key requirement in this approach is the capability to handle GT systems with (possibly) infinite state spaces. This thesis presents two abstraction techniques that yield a finite over-approximation of the behaviour of infinite-state GT systems, thus enabling verification on the abstract level. The two techniques, called neighbourhood abstraction and pattern abstraction, are discussed under both a theoretical and a practical focus; the former concerning the formal definition and correctness of the abstraction methods, and the latter discussing their implementation in GROOVE, our GT tool set. Experimental results are also given in order to assess the performance of the developed tools.

AB - The verification of systems with respect to a desired set of behavioural properties is a crucial step in increasing our confidence that these systems will correctly function under all circumstances. Although it would be desirable to verify all (computer) systems that we use in our daily life, the sheer complexity of the verification tasks often limit their application to critical systems. A system is considered critical when its incorrect behaviour can cause severe damage, such as loss of lives or the destruction of valuable equipment. In this thesis, we use graph transformation as our modelling formalism for system specification. Graph transformation (GT) is a Turing-powerful, declarative rule-based formalism, with a mature theoretical foundation and a thriving tool environment. Our work focus on the behavioural analysis of GT systems, where a GT system semantics is represented by a labelled transition system, that can then be analysed by well-established verification methods, such as model checking. A key requirement in this approach is the capability to handle GT systems with (possibly) infinite state spaces. This thesis presents two abstraction techniques that yield a finite over-approximation of the behaviour of infinite-state GT systems, thus enabling verification on the abstract level. The two techniques, called neighbourhood abstraction and pattern abstraction, are discussed under both a theoretical and a practical focus; the former concerning the formal definition and correctness of the abstraction methods, and the latter discussing their implementation in GROOVE, our GT tool set. Experimental results are also given in order to assess the performance of the developed tools.

KW - METIS-293491

KW - IR-83260

U2 - 10.3990/1.9789036534772

DO - 10.3990/1.9789036534772

M3 - PhD Thesis - Research UT, graduation UT

SN - 978-90-365-3477-2

PB - Universiteit Twente

ER -

Zambon E. Abstract graph transformation theory and practice. Enschede: Universiteit Twente, 2013. 152 p. Available from, DOI: 10.3990/1.9789036534772