The GROOVE Simulator: A Tool for State Space Generation

Arend Rensink

Research output: Contribution to conference › Paper › Academic › peer-review

188 Citations (Scopus)
56 Downloads (Pure)

Abstract

The tool described here is the first part of a tool set called GROOVE (GRaph-based Object-Oriented VErification) for software model checking of object-oriented systems. The special feature of GROOVE, which sets it apart from other model checking approaches, is that it is based on graph transformations. It uses graphs to represent state snapshots; transitions arise from the application of graph production rules. This yields so-called Graph Transition Systems (GTSrsquos) as computational models.
Original languageEnglish
Pages479-485
Number of pages7
DOIs
Publication statusPublished - 2004
Event2nd International Workshop on Applications of Graph Transformations with Industrial Relevance, AGTIVE 2003 - Charlottesville, United States
Duration: 27 Sep 2003 → 1 Oct 2003
Conference number: 2

Conference

Conference2nd International Workshop on Applications of Graph Transformations with Industrial Relevance, AGTIVE 2003
Abbreviated titleAGTIVE
CountryUnited States
CityCharlottesville
Period27/09/03 → 1/10/03

Fingerprint

Model checking
Simulators

Keywords

  • EWI-6926
  • IR-66357
  • METIS-220514

Cite this

Rensink, A. (2004). The GROOVE Simulator: A Tool for State Space Generation. 479-485. Paper presented at 2nd International Workshop on Applications of Graph Transformations with Industrial Relevance, AGTIVE 2003, Charlottesville, United States. https://doi.org/10.1007/978-3-540-25959-6_40
Rensink, Arend. / The GROOVE Simulator : A Tool for State Space Generation. Paper presented at 2nd International Workshop on Applications of Graph Transformations with Industrial Relevance, AGTIVE 2003, Charlottesville, United States.7 p.
@conference{a3f121be8ae341abab9774e0f4995a73,
title = "The GROOVE Simulator: A Tool for State Space Generation",
abstract = "The tool described here is the first part of a tool set called GROOVE (GRaph-based Object-Oriented VErification) for software model checking of object-oriented systems. The special feature of GROOVE, which sets it apart from other model checking approaches, is that it is based on graph transformations. It uses graphs to represent state snapshots; transitions arise from the application of graph production rules. This yields so-called Graph Transition Systems (GTSrsquos) as computational models.",
keywords = "EWI-6926, IR-66357, METIS-220514",
author = "Arend Rensink",
year = "2004",
doi = "10.1007/978-3-540-25959-6_40",
language = "English",
pages = "479--485",
note = "2nd International Workshop on Applications of Graph Transformations with Industrial Relevance, AGTIVE 2003, AGTIVE ; Conference date: 27-09-2003 Through 01-10-2003",

}

Rensink, A 2004, 'The GROOVE Simulator: A Tool for State Space Generation' Paper presented at 2nd International Workshop on Applications of Graph Transformations with Industrial Relevance, AGTIVE 2003, Charlottesville, United States, 27/09/03 - 1/10/03, pp. 479-485. https://doi.org/10.1007/978-3-540-25959-6_40

The GROOVE Simulator : A Tool for State Space Generation. / Rensink, Arend.

2004. 479-485 Paper presented at 2nd International Workshop on Applications of Graph Transformations with Industrial Relevance, AGTIVE 2003, Charlottesville, United States.

Research output: Contribution to conference › Paper › Academic › peer-review

TY - CONF

T1 - The GROOVE Simulator

T2 - A Tool for State Space Generation

AU - Rensink, Arend

PY - 2004

Y1 - 2004

N2 - The tool described here is the first part of a tool set called GROOVE (GRaph-based Object-Oriented VErification) for software model checking of object-oriented systems. The special feature of GROOVE, which sets it apart from other model checking approaches, is that it is based on graph transformations. It uses graphs to represent state snapshots; transitions arise from the application of graph production rules. This yields so-called Graph Transition Systems (GTSrsquos) as computational models.

AB - The tool described here is the first part of a tool set called GROOVE (GRaph-based Object-Oriented VErification) for software model checking of object-oriented systems. The special feature of GROOVE, which sets it apart from other model checking approaches, is that it is based on graph transformations. It uses graphs to represent state snapshots; transitions arise from the application of graph production rules. This yields so-called Graph Transition Systems (GTSrsquos) as computational models.

KW - EWI-6926

KW - IR-66357

KW - METIS-220514

U2 - 10.1007/978-3-540-25959-6_40

DO - 10.1007/978-3-540-25959-6_40

M3 - Paper

SP - 479

EP - 485

ER -

Rensink A. The GROOVE Simulator: A Tool for State Space Generation. 2004. Paper presented at 2nd International Workshop on Applications of Graph Transformations with Industrial Relevance, AGTIVE 2003, Charlottesville, United States. https://doi.org/10.1007/978-3-540-25959-6_40

Access to Document