Information Technology Reference
In-Depth Information
Directed Model Checking for B:
An Evaluation and New Techniques
Michael Leuschel and Jens Bendisposto
Institut fur Informatik, Universitat Dusseldorf
Universitatsstr. 1, D-40225 Dusseldorf
{
leuschel,bendisposto
}
@cs.uni-duesseldorf.de
Abstract.
ProB is a model checker for high-level formalisms such as B,
Event-B, CSP and Z. ProB uses a mixed depth-first/breadth-first search
strategy, and in previous work we have argued that this can perform bet-
ter in practice than pure depth-first or breadth-first search, as employed
by low-level model checkers. In this paper we present a thorough em-
pirical evaluation of this technique, which confirms our conjecture. The
experiments were conducted on a wide variety of B and Event-B models,
including several industrial case studies. Furthermore, we have extended
ProB to be able to perform directed model checking, where each state
is associated with a priority computed by a heuristic function. We eval-
uate various heuristic functions, on a series of problems, and find some
interesting candidates for detecting deadlocks and finding specific target
states.
Keywords:
Model Checking, B-Method, Tool Support, Directed Model
Checking, Search, Industrial Case Studies, spin.
1
Introduction
Many model checking tools, such as smv [21,3] and spin [11,13,2], work on
relatively low-level formalisms. Recently, however, there have also been model
checkers which work on higher-level formalisms, such as tlc [25] for TLA
+
, fdr
[9] for CSP and alloy [16] for a formalism of the same name (although the
latter two are strictly speaking not model checkers). Another example is ProB
[19,20] which accepts B [1].
It is relatively clear that a higher level specification formalism enables a more
convenient modelling. On the other hand, conventional wisdom would dictate
that a lower-level formalism will lead to more ecient model checking. However,
our own experience has been different. During previous teaching and research
activities, we have accumulated anecdotal evidence that using a high-level for-
malism such as B
can
be much more productive than using a low-level formalism
such as Promela. The study [24,23] examined the elaboration of B models for
ProB and Promela models for spin on ten different problems. Unsurprisingly,
the time required to develop the Promela models was markedly higher than for
the B models, (and some models could not be fully completed in Promela). The
