Abstract
The (in)correct functioning of many software systems heavily influences how we qualify our daily lives. Software companies as well as academic computer science research groups spend much effort on applying and developing techniques for improving the correctness of software systems. In this dissertation we focus on using and developing graphbased techniques to specify and verify the behaviour of software systems in general, and objectoriented systems more specically. We elaborate on two ways to improve the correctness (and thereby the quality) of such systems.
Firstly, we investigate the potential of using the graph transformation technique to formally specify the dynamic semantics of (objectoriented) programming languages. Those semantics are typically specied in natural language. Such specications are often hard to understand or even ambiguous. We show how the graph transformation framework provides formal and intuitive means for their specication.
Secondly, we develop techniques to verify systems of which the behaviour is specied as graph production systems. For the verication of such systems, we introduce an algorithm that combines a wellknown onthey model checking algorithm with ideas from bounded model checking. One of the main problems of model checking is the stateexplosion problem. This problem is often tackled using partial order reduction techniques. Unfortunately, many such techniques are based on assumptions that do not hold for graph production systems. Therefore, we develop a new dynamic partial order reduction algorithm based on selecting socalled probe sets and prove its correctness.
Most of the techniques developed in this dissertation have been implemented in the graph transformation tool GROOVE.
Firstly, we investigate the potential of using the graph transformation technique to formally specify the dynamic semantics of (objectoriented) programming languages. Those semantics are typically specied in natural language. Such specications are often hard to understand or even ambiguous. We show how the graph transformation framework provides formal and intuitive means for their specication.
Secondly, we develop techniques to verify systems of which the behaviour is specied as graph production systems. For the verication of such systems, we introduce an algorithm that combines a wellknown onthey model checking algorithm with ideas from bounded model checking. One of the main problems of model checking is the stateexplosion problem. This problem is often tackled using partial order reduction techniques. Unfortunately, many such techniques are based on assumptions that do not hold for graph production systems. Therefore, we develop a new dynamic partial order reduction algorithm based on selecting socalled probe sets and prove its correctness.
Most of the techniques developed in this dissertation have been implemented in the graph transformation tool GROOVE.
Original language  Undefined 

Qualification  Doctor of Philosophy 
Awarding Institution 

Supervisors/Advisors 

Award date  3 Oct 2008 
Place of Publication  Enschede 
Publisher  
Print ISBNs  9789036527347 
DOIs  
Publication status  Published  3 Oct 2008 
Keywords
 METIS252059
 EWI13615
 IR59779