Model Checking Dynamic States in GROOVE

H. Kastenberg, Arend Rensink

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

64 Citations (Scopus)

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.
Original languageUndefined
Title of host publicationModel Checking Software (SPIN)
EditorsA. Valmari
Place of PublicationBerlin
PublisherSpringer
Pages299-305
Number of pages7
ISBN (Print)3-540-33102-6
DOIs
Publication statusPublished - 2006

Publication series

NameLecture Notes in Computer Science
PublisherSpringer-Verlag
Number2
Volume3925
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Keywords

  • IR-62876
  • EWI-2793
  • METIS-238019

Cite this

Kastenberg, H., & Rensink, A. (2006). Model Checking Dynamic States in GROOVE. In A. Valmari (Ed.), Model Checking Software (SPIN) (pp. 299-305). [10.1007/11691617_19] (Lecture Notes in Computer Science; Vol. 3925, No. 2). Berlin: Springer. https://doi.org/10.1007/11691617_19
Kastenberg, H. ; Rensink, Arend. / Model Checking Dynamic States in GROOVE. Model Checking Software (SPIN). editor / A. Valmari. Berlin : Springer, 2006. pp. 299-305 (Lecture Notes in Computer Science; 2).
@inproceedings{01fb2487368f4ca89b2d87d7485a05e8,
title = "Model Checking Dynamic States in GROOVE",
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.",
keywords = "IR-62876, EWI-2793, METIS-238019",
author = "H. Kastenberg and Arend Rensink",
note = "10.1007/11691617_19",
year = "2006",
doi = "10.1007/11691617_19",
language = "Undefined",
isbn = "3-540-33102-6",
series = "Lecture Notes in Computer Science",
publisher = "Springer",
number = "2",
pages = "299--305",
editor = "A. Valmari",
booktitle = "Model Checking Software (SPIN)",

}

Kastenberg, H & Rensink, A 2006, Model Checking Dynamic States in GROOVE. in A Valmari (ed.), Model Checking Software (SPIN)., 10.1007/11691617_19, Lecture Notes in Computer Science, no. 2, vol. 3925, Springer, Berlin, pp. 299-305. https://doi.org/10.1007/11691617_19

Model Checking Dynamic States in GROOVE. / Kastenberg, H.; Rensink, Arend.

Model Checking Software (SPIN). ed. / A. Valmari. Berlin : Springer, 2006. p. 299-305 10.1007/11691617_19 (Lecture Notes in Computer Science; Vol. 3925, No. 2).

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

TY - GEN

T1 - Model Checking Dynamic States in GROOVE

AU - Kastenberg, H.

AU - Rensink, Arend

N1 - 10.1007/11691617_19

PY - 2006

Y1 - 2006

N2 - 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.

AB - 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.

KW - IR-62876

KW - EWI-2793

KW - METIS-238019

U2 - 10.1007/11691617_19

DO - 10.1007/11691617_19

M3 - Conference contribution

SN - 3-540-33102-6

T3 - Lecture Notes in Computer Science

SP - 299

EP - 305

BT - Model Checking Software (SPIN)

A2 - Valmari, A.

PB - Springer

CY - Berlin

ER -

Kastenberg H, Rensink A. Model Checking Dynamic States in GROOVE. In Valmari A, editor, Model Checking Software (SPIN). Berlin: Springer. 2006. p. 299-305. 10.1007/11691617_19. (Lecture Notes in Computer Science; 2). https://doi.org/10.1007/11691617_19