Model Checking Dynamic States in GROOVE

H. Kastenberg, Arend Rensink

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

    67 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