### Abstract

Original language | Undefined |
---|---|

Title of host publication | Model Checking Software (SPIN) |

Editors | A. Valmari |

Place of Publication | Berlin |

Publisher | Springer |

Pages | 299-305 |

Number of pages | 7 |

ISBN (Print) | 3-540-33102-6 |

DOIs | |

Publication status | Published - 2006 |

### Publication series

Name | Lecture Notes in Computer Science |
---|---|

Publisher | Springer-Verlag |

Number | 2 |

Volume | 3925 |

ISSN (Print) | 0302-9743 |

ISSN (Electronic) | 1611-3349 |

### Keywords

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

### Cite this

*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

}

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

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-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 -