Graph-based software specification and verification


Kastenberg, Harmen (2008) Graph-based software specification and verification. thesis.

open access
[img] PDF
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 graph-based techniques to specify and verify
the behaviour of software systems in general, and object-oriented systems more
specifically. 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 tech-
nique to formally specify the dynamic semantics of (object-oriented) program-
ming languages. Those semantics are typically specified in natural language.
Such specifications are often hard to understand or even ambiguous. We show
how the graph transformation framework provides formal and intuitive means
for their specification.
Secondly, we develop techniques to verify systems of which the behaviour is
specified as graph production systems. For the verification of such systems, we
introduce an algorithm that combines a well-known on-the-
y model checking
algorithm with ideas from bounded model checking. One of the main prob-
lems of model checking is the state-explosion 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 sys-
tems. Therefore, we develop a new dynamic partial order reduction algorithm
based on selecting so-called probe sets and prove its correctness.
Most of the techniques developed in this dissertation have been implemented
in the graph transformation tool GROOVE.
Item Type:Thesis
Research Group:
Link to this item:
Official URL:
Export this item as:BibTeX
HTML Citation
Reference Manager


Repository Staff Only: item control page

Metis ID: 252059