Abstract
Original language  English 

Awarding Institution 

Supervisors/Advisors 

Date of Award  24 Jan 2013 
Place of Publication  Enschede 
Publisher  
Print ISBNs  9789036534772 
DOIs  
State  Published  24 Jan 2013 
Fingerprint
Keywords
 METIS293491
 IR83260
Cite this
}
Abstract graph transformation theory and practice. / Zambon, Eduardo.
Enschede : Universiteit Twente, 2013. 152 p.Research output: Scientific › PhD Thesis  Research UT, graduation UT
TY  THES
T1  Abstract graph transformation theory and practice
AU  Zambon,Eduardo
N1  IPA Dissertation Series No. 201303
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 Turingpowerful, declarative rulebased 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 wellestablished 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 overapproximation of the behaviour of infinitestate 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 Turingpowerful, declarative rulebased 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 wellestablished 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 overapproximation of the behaviour of infinitestate 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  METIS293491
KW  IR83260
U2  10.3990/1.9789036534772
DO  10.3990/1.9789036534772
M3  PhD Thesis  Research UT, graduation UT
SN  9789036534772
PB  Universiteit Twente
ER 