Bridging the Gap between Enumerative and Symbolic Model Checkers

Stefan Blom, Jan Cornelis van de Pol, M. Weber

Abstract

We present a method to perform symbolic state space generation for languages with existing enumerative state generators. The method is largely independent from the chosen modelling language. We validated this on three different types of languages and tools: state-based languages (PROMELA), action-based process algebras (muCRL, mCRL2), and discrete abstractions of ODEs (Maple). Only little information about the combinatorial structure of the underlying model checking problem need to be provided. The key enabling data structure is the "PINS" dependency matrix. Moreover, it can be provided gradually (more precise information yield better results). Second, in addition to symbolic reachability, the same PINS matrix contains enough information to enable new optimizations in state space generation (transition caching), again independent from the chosen modelling language. We have also based existing optimizations, like (recursive) state collapsing, on top of PINS and hint at how to support partial order reduction techniques. Third, PINS allows interfacing of existing state generators to, e.g., distributed reachability tools. Thus, besides the stated novelties, the method we propose also significantly reduces the complexity of building modular yet still efficient model checking tools. Our experiments show that we can match or even outperform existing tools by reusing their own state generators, which we have linked into an implementation of our ideas.
Original languageUndefined
Place of PublicationEnschede
PublisherCentre for Telematics and Information Technology (CTIT)
Number of pages8
StatePublished - 5 Jun 2009

Publication series

NameCTIT Technical Report Series
PublisherUniversity of Twente, Centre for Telematics and Information Technology
No.TR-CTIT-09-30
ISSN (Print)1381-3625

Fingerprint

Model checking
Algebra
Data structures
Experiments
Modeling languages

Keywords

  • IR-67526
  • Model Checking
  • State Space Exploration
  • METIS-263921
  • EC Grant Agreement nr.: FP6/043235
  • EWI-15703
  • Symbolic reachability

Cite this

Blom, S., van de Pol, J. C., & Weber, M. (2009). Bridging the Gap between Enumerative and Symbolic Model Checkers. (CTIT Technical Report Series; No. TR-CTIT-09-30). Enschede: Centre for Telematics and Information Technology (CTIT).

Blom, Stefan; van de Pol, Jan Cornelis; Weber, M. / Bridging the Gap between Enumerative and Symbolic Model Checkers.

Enschede : Centre for Telematics and Information Technology (CTIT), 2009. 8 p. (CTIT Technical Report Series; No. TR-CTIT-09-30).

Research output: ProfessionalReport

@book{a05e219ada9e4773afa69d041faedb66,
title = "Bridging the Gap between Enumerative and Symbolic Model Checkers",
abstract = "We present a method to perform symbolic state space generation for languages with existing enumerative state generators. The method is largely independent from the chosen modelling language. We validated this on three different types of languages and tools: state-based languages (PROMELA), action-based process algebras (muCRL, mCRL2), and discrete abstractions of ODEs (Maple). Only little information about the combinatorial structure of the underlying model checking problem need to be provided. The key enabling data structure is the {"}PINS{"} dependency matrix. Moreover, it can be provided gradually (more precise information yield better results). Second, in addition to symbolic reachability, the same PINS matrix contains enough information to enable new optimizations in state space generation (transition caching), again independent from the chosen modelling language. We have also based existing optimizations, like (recursive) state collapsing, on top of PINS and hint at how to support partial order reduction techniques. Third, PINS allows interfacing of existing state generators to, e.g., distributed reachability tools. Thus, besides the stated novelties, the method we propose also significantly reduces the complexity of building modular yet still efficient model checking tools. Our experiments show that we can match or even outperform existing tools by reusing their own state generators, which we have linked into an implementation of our ideas.",
keywords = "IR-67526, Model Checking, State Space Exploration, METIS-263921, EC Grant Agreement nr.: FP6/043235, EWI-15703, Symbolic reachability",
author = "Stefan Blom and {van de Pol}, {Jan Cornelis} and M. Weber",
year = "2009",
month = "6",
series = "CTIT Technical Report Series",
publisher = "Centre for Telematics and Information Technology (CTIT)",
number = "TR-CTIT-09-30",
address = "Netherlands",

}

Blom, S, van de Pol, JC & Weber, M 2009, Bridging the Gap between Enumerative and Symbolic Model Checkers. CTIT Technical Report Series, no. TR-CTIT-09-30, Centre for Telematics and Information Technology (CTIT), Enschede.

Bridging the Gap between Enumerative and Symbolic Model Checkers. / Blom, Stefan; van de Pol, Jan Cornelis; Weber, M.

Enschede : Centre for Telematics and Information Technology (CTIT), 2009. 8 p. (CTIT Technical Report Series; No. TR-CTIT-09-30).

Research output: ProfessionalReport

TY - BOOK

T1 - Bridging the Gap between Enumerative and Symbolic Model Checkers

AU - Blom,Stefan

AU - van de Pol,Jan Cornelis

AU - Weber,M.

PY - 2009/6/5

Y1 - 2009/6/5

N2 - We present a method to perform symbolic state space generation for languages with existing enumerative state generators. The method is largely independent from the chosen modelling language. We validated this on three different types of languages and tools: state-based languages (PROMELA), action-based process algebras (muCRL, mCRL2), and discrete abstractions of ODEs (Maple). Only little information about the combinatorial structure of the underlying model checking problem need to be provided. The key enabling data structure is the "PINS" dependency matrix. Moreover, it can be provided gradually (more precise information yield better results). Second, in addition to symbolic reachability, the same PINS matrix contains enough information to enable new optimizations in state space generation (transition caching), again independent from the chosen modelling language. We have also based existing optimizations, like (recursive) state collapsing, on top of PINS and hint at how to support partial order reduction techniques. Third, PINS allows interfacing of existing state generators to, e.g., distributed reachability tools. Thus, besides the stated novelties, the method we propose also significantly reduces the complexity of building modular yet still efficient model checking tools. Our experiments show that we can match or even outperform existing tools by reusing their own state generators, which we have linked into an implementation of our ideas.

AB - We present a method to perform symbolic state space generation for languages with existing enumerative state generators. The method is largely independent from the chosen modelling language. We validated this on three different types of languages and tools: state-based languages (PROMELA), action-based process algebras (muCRL, mCRL2), and discrete abstractions of ODEs (Maple). Only little information about the combinatorial structure of the underlying model checking problem need to be provided. The key enabling data structure is the "PINS" dependency matrix. Moreover, it can be provided gradually (more precise information yield better results). Second, in addition to symbolic reachability, the same PINS matrix contains enough information to enable new optimizations in state space generation (transition caching), again independent from the chosen modelling language. We have also based existing optimizations, like (recursive) state collapsing, on top of PINS and hint at how to support partial order reduction techniques. Third, PINS allows interfacing of existing state generators to, e.g., distributed reachability tools. Thus, besides the stated novelties, the method we propose also significantly reduces the complexity of building modular yet still efficient model checking tools. Our experiments show that we can match or even outperform existing tools by reusing their own state generators, which we have linked into an implementation of our ideas.

KW - IR-67526

KW - Model Checking

KW - State Space Exploration

KW - METIS-263921

KW - EC Grant Agreement nr.: FP6/043235

KW - EWI-15703

KW - Symbolic reachability

M3 - Report

T3 - CTIT Technical Report Series

BT - Bridging the Gap between Enumerative and Symbolic Model Checkers

PB - Centre for Telematics and Information Technology (CTIT)

ER -

Blom S, van de Pol JC, Weber M. Bridging the Gap between Enumerative and Symbolic Model Checkers. Enschede: Centre for Telematics and Information Technology (CTIT), 2009. 8 p. (CTIT Technical Report Series; TR-CTIT-09-30).