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)
CY - Enschede
ER -