Abstract
Original language  Undefined 

Supervisors/Advisors 

Sponsors  
Date of Award  24 Jan 2013 
Place of Publication  Enschede 
Publisher  
Print ISBNs  9789036534772 
DOIs  
State  Published  24 Jan 2013 
Fingerprint
Keywords
 Graphbased Modelling
 EWI22860
 GROOVE
 Graph Transformation
 Graph Abstraction
 Model Checking
 NWO 612.000.632
Cite this
}
Abstract Graph Transformation  Theory and Practice. / Zambon, Eduardo.
Enschede : Centre for Telematics and Information Technology (CTIT), 2013. 162 p.Research output: Scientific › PhD 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 wellestablished 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 infinitestate 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 Turingpowerful, declarative rulebased 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 infinitestate graph transformation systems. We present two abstraction techniques that yield a finite overapproximation of the behaviour of such infinitestate 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 wellestablished 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 infinitestate 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 Turingpowerful, declarative rulebased 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 infinitestate graph transformation systems. We present two abstraction techniques that yield a finite overapproximation of the behaviour of such infinitestate 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  Graphbased Modelling
KW  EWI22860
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  9789036534772
PB  Centre for Telematics and Information Technology (CTIT)
ER 