Abstract Graph Transformation - Theory and Practice

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.