Model Checking Dynamic States in GROOVE


Kastenberg, H. and Rensink, A. (2006) Model Checking Dynamic States in GROOVE. In: Model Checking Software (SPIN), 30 Mar - 1 Apr 2006, Vienna, Austria (pp. pp. 299-305).

[img] PDF
Restricted to UT campus only
: Request a copy
Abstract:Much research has been done in the field of model-checking complex systems (either hardware or software). Approaches that use explicit state modelling mostly use bit vectors to represent the states of such systems. Unfortunately, that kind of representation does not extend smoothly to systems in which the states contain values from a domain other than primitive types, such as reference values commonly used in object-oriented systems.

In this paper we report preliminary results on applying CTL model checking on state spaces generated using graph transformations. The states of such state spaces have an internal graph structure which makes it possible to represent complex system states without the need to know the exact structure beforehand as when using bit vectors.
Item Type:Conference or Workshop Item
Electrical Engineering, Mathematics and Computer Science (EEMCS)
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: 238019