An Object-Oriented Framework for Explicit-State Model Checking

Mark Kattenbelt; Theo C. Ruys; Arend Rensink

An Object-Oriented Framework for Explicit-State Model Checking

Mark Kattenbelt
, Theo C. Ruys
, Arend Rensink

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

67 Downloads (Pure)

Abstract

This paper presents a conceptual architecture for an object-oriented framework to support the development of formal verification tools (i.e. model checkers). The objective of the architecture is to support the reuse of algorithms and to encourage a modular design of tools. The conceptual framework is accompanied by a C++ implementation which provides reusable algorithms for the simulation and verification of explicit-state models as well as a model representation for simple models based on guard-based process descriptions. The framework has been successfully used to develop a model checker for a subset of PROMELA.

Original language	English
Title of host publication	Proceedings of the 3rd European Symposium on Verification and Validation of Software Systems (VVSS 2007)
Editors	P. Groot, A. Serebrenik, M. van Eekelen
Place of Publication	Eindhoven
Publisher	Eindhoven University of Technology
Pages	84-92
Number of pages	9
Publication status	Published - 23 Mar 2007
Event	3rd European Symposium on Verification and Validation of Software Systems, VVSS 2007 - Eindhoven, Netherlands Duration: 23 Mar 2007 → 23 Mar 2007 Conference number: 3

Publication series

Name	TUE Computer Science Reports
Publisher	Eindhoven University of Technology (TUE)
Number	07-04
ISSN (Print)	0926-4515

Conference

Conference	3rd European Symposium on Verification and Validation of Software Systems, VVSS 2007
Abbreviated title	VVSS
Country/Territory	Netherlands
City	Eindhoven
Period	23/03/07 → 23/03/07

Keywords

FMT-MC: MODEL CHECKING

Access to Document

ReportFinal published version, 160 KB

Cite this

Kattenbelt, Mark ; Ruys, Theo C. ; Rensink, Arend. / An Object-Oriented Framework for Explicit-State Model Checking. Proceedings of the 3rd European Symposium on Verification and Validation of Software Systems (VVSS 2007). editor / P. Groot ; A. Serebrenik ; M. van Eekelen. Eindhoven : Eindhoven University of Technology, 2007. pp. 84-92 (TUE Computer Science Reports; 07-04).

@inproceedings{fb4d3645fad7483397b67fd1221739e5,

title = "An Object-Oriented Framework for Explicit-State Model Checking",

abstract = "This paper presents a conceptual architecture for an object-oriented framework to support the development of formal verification tools (i.e. model checkers). The objective of the architecture is to support the reuse of algorithms and to encourage a modular design of tools. The conceptual framework is accompanied by a C++ implementation which provides reusable algorithms for the simulation and verification of explicit-state models as well as a model representation for simple models based on guard-based process descriptions. The framework has been successfully used to develop a model checker for a subset of PROMELA.",

keywords = "FMT-MC: MODEL CHECKING",

author = "Mark Kattenbelt and Ruys, \{Theo C.\} and Arend Rensink",

year = "2007",

month = mar,

day = "23",

language = "English",

series = "TUE Computer Science Reports",

publisher = "Eindhoven University of Technology",

number = "07-04",

pages = "84--92",

editor = "P. Groot and A. Serebrenik and \{van Eekelen\}, M.",

booktitle = "Proceedings of the 3rd European Symposium on Verification and Validation of Software Systems (VVSS 2007)",

address = "Netherlands",

note = "3rd European Symposium on Verification and Validation of Software Systems, VVSS 2007, VVSS ; Conference date: 23-03-2007 Through 23-03-2007",

}

Kattenbelt, M, Ruys, TC & Rensink, A 2007, An Object-Oriented Framework for Explicit-State Model Checking. in P Groot, A Serebrenik & M van Eekelen (eds), Proceedings of the 3rd European Symposium on Verification and Validation of Software Systems (VVSS 2007). TUE Computer Science Reports, no. 07-04, Eindhoven University of Technology, Eindhoven, pp. 84-92, 3rd European Symposium on Verification and Validation of Software Systems, VVSS 2007, Eindhoven, Netherlands, 23/03/07.

An Object-Oriented Framework for Explicit-State Model Checking. / Kattenbelt, Mark; Ruys, Theo C.; Rensink, Arend.
Proceedings of the 3rd European Symposium on Verification and Validation of Software Systems (VVSS 2007). ed. / P. Groot; A. Serebrenik; M. van Eekelen. Eindhoven: Eindhoven University of Technology, 2007. p. 84-92 (TUE Computer Science Reports; No. 07-04).

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

TY - GEN

T1 - An Object-Oriented Framework for Explicit-State Model Checking

AU - Kattenbelt, Mark

AU - Ruys, Theo C.

AU - Rensink, Arend

N1 - Conference code: 3

PY - 2007/3/23

Y1 - 2007/3/23

N2 - This paper presents a conceptual architecture for an object-oriented framework to support the development of formal verification tools (i.e. model checkers). The objective of the architecture is to support the reuse of algorithms and to encourage a modular design of tools. The conceptual framework is accompanied by a C++ implementation which provides reusable algorithms for the simulation and verification of explicit-state models as well as a model representation for simple models based on guard-based process descriptions. The framework has been successfully used to develop a model checker for a subset of PROMELA.

AB - This paper presents a conceptual architecture for an object-oriented framework to support the development of formal verification tools (i.e. model checkers). The objective of the architecture is to support the reuse of algorithms and to encourage a modular design of tools. The conceptual framework is accompanied by a C++ implementation which provides reusable algorithms for the simulation and verification of explicit-state models as well as a model representation for simple models based on guard-based process descriptions. The framework has been successfully used to develop a model checker for a subset of PROMELA.

KW - FMT-MC: MODEL CHECKING

M3 - Conference contribution

T3 - TUE Computer Science Reports

SP - 84

EP - 92

BT - Proceedings of the 3rd European Symposium on Verification and Validation of Software Systems (VVSS 2007)

A2 - Groot, P.

A2 - Serebrenik, A.

A2 - van Eekelen, M.

PB - Eindhoven University of Technology

CY - Eindhoven

T2 - 3rd European Symposium on Verification and Validation of Software Systems, VVSS 2007

Y2 - 23 March 2007 through 23 March 2007

ER -

An Object-Oriented Framework for Explicit-State Model Checking

Abstract

Publication series

Conference

Keywords

Access to Document

Fingerprint

Cite this