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. One well-established verification method is model checking. This method takes as input a system specification (the model) and a desired property, and checks if the model satisfies the property. A usual approach within this technique is explicit state model checking, which tries to exhaustively enumerate all configurations (states) that the system may exhibit. This enumerative procedure is called the exploration of the model state space. State space exploration can be used in many different settings but it cannot be directly applied to systems that have infinite state spaces. Classes of such systems include any model where an unbounded number of entities can be created. This is the case, for example, in a model representing a memory heap, where data structures can be dynamically allocated. To handle infinite-state models, some form of abstraction is necessary to ensure that the verification will terminate. An obvious requirement for such abstractions is that it should still be possible to use the abstract state space representation to check if the system conforms to the property of interest. In this thesis, we use graph transformation as our modelling formalism for system specification. Graph transformation is a Turing-powerful, declarative rule-based formalism, with a mature theoretical foundation and a thriving tool environment. Our work focus on model checking of graph transformation systems, more specifically on the exploration of their state spaces, and in particular for infinite-state graph transformation systems. We present two abstraction techniques that yield a finite over-approximation of the behaviour of such infinite-state graph transformation systems, thus enabling verification on the abstract level. The first technique, called neighbourhood abstraction is discussed under both a theoretical and a practical focus; the former concerning the formal definition and correctness of the abstraction method, and the latter discussing its implementation in GROOVE, our graph transformation tool set. Experimental results are also given in order to assess the performance of the developed tools. For the second abstraction technique, called pattern abstraction, we present its complete theoretical foundation while providing some indications on how its practical implementation can be realised.
Original languageUndefined
Supervisors/Advisors
  • Rensink, Arend , Supervisor
Sponsors
Date of Award24 Jan 2013
Place of PublicationEnschede
Publisher
Print ISBNs978-90-365-3477-2
DOIs
StatePublished - 24 Jan 2013

Fingerprint

Model checking
Specifications
Data structures
Computer systems

Keywords

  • Graph-based Modelling
  • EWI-22860
  • GROOVE
  • Graph Transformation
  • Graph Abstraction
  • Model Checking
  • NWO 612.000.632

Cite this

Zambon, E. (2013). Abstract Graph Transformation - Theory and Practice Enschede: Centre for Telematics and Information Technology (CTIT) DOI: 10.3990/1.9789036534772
Zambon, Eduardo. / Abstract Graph Transformation - Theory and Practice. Enschede : Centre for Telematics and Information Technology (CTIT), 2013. 162 p.
@misc{8ee3191dfbe54a6eb12dd71c46090023,
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. One well-established verification method is model checking. This method takes as input a system specification (the model) and a desired property, and checks if the model satisfies the property. A usual approach within this technique is explicit state model checking, which tries to exhaustively enumerate all configurations (states) that the system may exhibit. This enumerative procedure is called the exploration of the model state space. State space exploration can be used in many different settings but it cannot be directly applied to systems that have infinite state spaces. Classes of such systems include any model where an unbounded number of entities can be created. This is the case, for example, in a model representing a memory heap, where data structures can be dynamically allocated. To handle infinite-state models, some form of abstraction is necessary to ensure that the verification will terminate. An obvious requirement for such abstractions is that it should still be possible to use the abstract state space representation to check if the system conforms to the property of interest. In this thesis, we use graph transformation as our modelling formalism for system specification. Graph transformation is a Turing-powerful, declarative rule-based formalism, with a mature theoretical foundation and a thriving tool environment. Our work focus on model checking of graph transformation systems, more specifically on the exploration of their state spaces, and in particular for infinite-state graph transformation systems. We present two abstraction techniques that yield a finite over-approximation of the behaviour of such infinite-state graph transformation systems, thus enabling verification on the abstract level. The first technique, called neighbourhood abstraction is discussed under both a theoretical and a practical focus; the former concerning the formal definition and correctness of the abstraction method, and the latter discussing its implementation in GROOVE, our graph transformation tool set. Experimental results are also given in order to assess the performance of the developed tools. For the second abstraction technique, called pattern abstraction, we present its complete theoretical foundation while providing some indications on how its practical implementation can be realised.",
keywords = "Graph-based Modelling, EWI-22860, GROOVE, Graph Transformation, Graph Abstraction, Model Checking, NWO 612.000.632",
author = "Eduardo Zambon",
note = "NWO 612.000.632",
year = "2013",
month = "1",
doi = "10.3990/1.9789036534772",
isbn = "978-90-365-3477-2",
publisher = "Centre for Telematics and Information Technology (CTIT)",
address = "Netherlands",

}

Abstract Graph Transformation - Theory and Practice. / Zambon, Eduardo.

Enschede : Centre for Telematics and Information Technology (CTIT), 2013. 162 p.

Research output: ScientificPhD Thesis - Research UT, graduation UT

TY - THES

T1 - Abstract Graph Transformation - Theory and Practice

AU - Zambon,Eduardo

N1 - NWO 612.000.632

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. One well-established verification method is model checking. This method takes as input a system specification (the model) and a desired property, and checks if the model satisfies the property. A usual approach within this technique is explicit state model checking, which tries to exhaustively enumerate all configurations (states) that the system may exhibit. This enumerative procedure is called the exploration of the model state space. State space exploration can be used in many different settings but it cannot be directly applied to systems that have infinite state spaces. Classes of such systems include any model where an unbounded number of entities can be created. This is the case, for example, in a model representing a memory heap, where data structures can be dynamically allocated. To handle infinite-state models, some form of abstraction is necessary to ensure that the verification will terminate. An obvious requirement for such abstractions is that it should still be possible to use the abstract state space representation to check if the system conforms to the property of interest. In this thesis, we use graph transformation as our modelling formalism for system specification. Graph transformation is a Turing-powerful, declarative rule-based formalism, with a mature theoretical foundation and a thriving tool environment. Our work focus on model checking of graph transformation systems, more specifically on the exploration of their state spaces, and in particular for infinite-state graph transformation systems. We present two abstraction techniques that yield a finite over-approximation of the behaviour of such infinite-state graph transformation systems, thus enabling verification on the abstract level. The first technique, called neighbourhood abstraction is discussed under both a theoretical and a practical focus; the former concerning the formal definition and correctness of the abstraction method, and the latter discussing its implementation in GROOVE, our graph transformation tool set. Experimental results are also given in order to assess the performance of the developed tools. For the second abstraction technique, called pattern abstraction, we present its complete theoretical foundation while providing some indications on how its practical implementation can be realised.

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. One well-established verification method is model checking. This method takes as input a system specification (the model) and a desired property, and checks if the model satisfies the property. A usual approach within this technique is explicit state model checking, which tries to exhaustively enumerate all configurations (states) that the system may exhibit. This enumerative procedure is called the exploration of the model state space. State space exploration can be used in many different settings but it cannot be directly applied to systems that have infinite state spaces. Classes of such systems include any model where an unbounded number of entities can be created. This is the case, for example, in a model representing a memory heap, where data structures can be dynamically allocated. To handle infinite-state models, some form of abstraction is necessary to ensure that the verification will terminate. An obvious requirement for such abstractions is that it should still be possible to use the abstract state space representation to check if the system conforms to the property of interest. In this thesis, we use graph transformation as our modelling formalism for system specification. Graph transformation is a Turing-powerful, declarative rule-based formalism, with a mature theoretical foundation and a thriving tool environment. Our work focus on model checking of graph transformation systems, more specifically on the exploration of their state spaces, and in particular for infinite-state graph transformation systems. We present two abstraction techniques that yield a finite over-approximation of the behaviour of such infinite-state graph transformation systems, thus enabling verification on the abstract level. The first technique, called neighbourhood abstraction is discussed under both a theoretical and a practical focus; the former concerning the formal definition and correctness of the abstraction method, and the latter discussing its implementation in GROOVE, our graph transformation tool set. Experimental results are also given in order to assess the performance of the developed tools. For the second abstraction technique, called pattern abstraction, we present its complete theoretical foundation while providing some indications on how its practical implementation can be realised.

KW - Graph-based Modelling

KW - EWI-22860

KW - GROOVE

KW - Graph Transformation

KW - Graph Abstraction

KW - Model Checking

KW - NWO 612.000.632

U2 - 10.3990/1.9789036534772

DO - 10.3990/1.9789036534772

M3 - PhD Thesis - Research UT, graduation UT

SN - 978-90-365-3477-2

PB - Centre for Telematics and Information Technology (CTIT)

ER -

Zambon E. Abstract Graph Transformation - Theory and Practice. Enschede: Centre for Telematics and Information Technology (CTIT), 2013. 162 p. Available from, DOI: 10.3990/1.9789036534772