Neighbourhood Abstraction in GROOVE - Tool Paper

Arend Rensink; Eduardo Zambon

Neighbourhood Abstraction in GROOVE - Tool Paper

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

52 Downloads (Pure)

Abstract

In this paper we discuss the implementation of neighbourhood graph abstraction in the GROOVE tool set. Important classes of graph grammars may have unbounded state spaces and therefore cannot be verified with traditional model checking techniques. One way to address this problem is to perform graph abstraction, which allows us to generate a finite abstract state space that over-approximates the original one. In previous work we presented the theory of neighbourhood abstraction. In this paper, we present the implementation of this theory in GROOVE and illustrate its applicability with a case study that models a single-linked list.

Original language	Undefined
Title of host publication	Proceedings of the Fourth International Workshop on Graph-Based Tools (GraBaTs 2010)
Editors	Juan de Lara, Daniel Varro
Place of Publication	Enschede
Publisher	Centre for Telematics and Information Technology (CTIT)
Pages	55-61
Number of pages	6
Publication status	Published - Jun 2010
Event	Fourth International Workshop on Graph-Based Tools, GraBaTs 2010: Proceedings of the Fourth International Workshop on Graph-Based Tools (GraBaTs 2010) - University of Twente, Enschede, Netherlands Duration: 28 Sept 2010 → 28 Sept 2010 Conference number: 4

Publication series

Name	CTIT Workshop Proceedings
Publisher	Centre for Telematics and Information Technology University of Twente
Number	WP 10-06
ISSN (Print)	0929-0672
ISSN (Electronic)	0929-0672

Conference

Conference	Fourth International Workshop on Graph-Based Tools, GraBaTs 2010
Abbreviated title	GraBaTs 2010
Country/Territory	Netherlands
City	Enschede
Period	28/09/10 → 28/09/10
Other	28 September 2010

Keywords

METIS-276081
GROOVE
Model Checking
EWI-18316
Graph Abstraction
Graph Transformation
IR-72606

Access to Document

abs-grooveFinal published version, 182 KB

Cite this

@inproceedings{b40d2643b92f445d879238d7fa11af31,

title = "Neighbourhood Abstraction in GROOVE - Tool Paper",

abstract = "In this paper we discuss the implementation of neighbourhood graph abstraction in the GROOVE tool set. Important classes of graph grammars may have unbounded state spaces and therefore cannot be verified with traditional model checking techniques. One way to address this problem is to perform graph abstraction, which allows us to generate a finite abstract state space that over-approximates the original one. In previous work we presented the theory of neighbourhood abstraction. In this paper, we present the implementation of this theory in GROOVE and illustrate its applicability with a case study that models a single-linked list.",

keywords = "METIS-276081, GROOVE, Model Checking, EWI-18316, Graph Abstraction, Graph Transformation, IR-72606",

author = "Arend Rensink and Eduardo Zambon",

note = "preproceedings; Fourth International Workshop on Graph-Based Tools, GraBaTs 2010 ; Conference date: 28-09-2010 Through 28-09-2010",

year = "2010",

month = jun,

language = "Undefined",

series = "CTIT Workshop Proceedings",

publisher = "Centre for Telematics and Information Technology (CTIT)",

number = "WP 10-06",

pages = "55--61",

editor = "{de Lara}, Juan and Daniel Varro",

booktitle = "Proceedings of the Fourth International Workshop on Graph-Based Tools (GraBaTs 2010)",

address = "Netherlands",

}

Rensink, A & Zambon, E 2010, Neighbourhood Abstraction in GROOVE - Tool Paper. in J de Lara & D Varro (eds), Proceedings of the Fourth International Workshop on Graph-Based Tools (GraBaTs 2010). CTIT Workshop Proceedings, no. WP 10-06, Centre for Telematics and Information Technology (CTIT), Enschede, pp. 55-61, Fourth International Workshop on Graph-Based Tools, GraBaTs 2010, Enschede, Netherlands, 28/09/10.

Neighbourhood Abstraction in GROOVE - Tool Paper. / Rensink, Arend; Zambon, Eduardo.
Proceedings of the Fourth International Workshop on Graph-Based Tools (GraBaTs 2010). ed. / Juan de Lara; Daniel Varro. Enschede: Centre for Telematics and Information Technology (CTIT), 2010. p. 55-61 (CTIT Workshop Proceedings; No. WP 10-06).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

TY - GEN

T1 - Neighbourhood Abstraction in GROOVE - Tool Paper

AU - Rensink, Arend

AU - Zambon, Eduardo

N1 - Conference code: 4

PY - 2010/6

Y1 - 2010/6

N2 - In this paper we discuss the implementation of neighbourhood graph abstraction in the GROOVE tool set. Important classes of graph grammars may have unbounded state spaces and therefore cannot be verified with traditional model checking techniques. One way to address this problem is to perform graph abstraction, which allows us to generate a finite abstract state space that over-approximates the original one. In previous work we presented the theory of neighbourhood abstraction. In this paper, we present the implementation of this theory in GROOVE and illustrate its applicability with a case study that models a single-linked list.

AB - In this paper we discuss the implementation of neighbourhood graph abstraction in the GROOVE tool set. Important classes of graph grammars may have unbounded state spaces and therefore cannot be verified with traditional model checking techniques. One way to address this problem is to perform graph abstraction, which allows us to generate a finite abstract state space that over-approximates the original one. In previous work we presented the theory of neighbourhood abstraction. In this paper, we present the implementation of this theory in GROOVE and illustrate its applicability with a case study that models a single-linked list.

KW - METIS-276081

KW - GROOVE

KW - Model Checking

KW - EWI-18316

KW - Graph Abstraction

KW - Graph Transformation

KW - IR-72606

M3 - Conference contribution

T3 - CTIT Workshop Proceedings

SP - 55

EP - 61

BT - Proceedings of the Fourth International Workshop on Graph-Based Tools (GraBaTs 2010)

A2 - de Lara, Juan

A2 - Varro, Daniel

PB - Centre for Telematics and Information Technology (CTIT)

CY - Enschede

T2 - Fourth International Workshop on Graph-Based Tools, GraBaTs 2010

Y2 - 28 September 2010 through 28 September 2010

ER -