Directed Model Checking for B: An Evaluation and New Techniques - Formal Methods: Foundations and Applications - page 2

study also found out that in practice both model checkers ProB and spin were
comparable in model checking performance, despite ProB working on a much
higher-level input language and being much slower when looking purely at the
number of states that can be stored and processed per time unit. Other indepen-
dent experimental evaluations also report good performance of ProB compared
against SMV [15].
In [17] we first tried to analyse and understand this counter-intuitive fact. One
explanation was that pure depth-first as employed by spin and other low-level
model checkers fares very badly in the context of large state spaces. Similarly,
a pure breadth-first strategy has problems in detecting long counter examples.
We argued in [17] that ProB's mixed depth-first/breadth-first search enabled
it to effectively find a larger class of errors. In this paper we test this conjecture
empirically on a large number of B specifications. In addition, we present a new
directed model checking algorithm for ProB: rather than randomly choosing
between doing a depth-first or breadth-first step, we associate priorities with the
pending states of the model checker. We then evaluate various ways of computing
priorities on the same specifications.
In Section 2 we present the motivation for mixed depth-first/breadth-first
search in more detail, and in Section 3 we perform a thorough empirical eval-
uation. In Section 4 we present the new directed model checking algorithm of
ProB, along with a range of heuristic functions with their empirical evaluation.
We finish with more related work and a conclusion in Section 5.
2 Combining Depth-First and Breadth-First for
Improved Model Checking
In [17] we first tried to analyse and understand the counter-intuitive behaviour
described above. Below, we recall some of the conclusions from [17]. One tricky
issue is the much finer granularity of low-level models. If one is not careful, the
number of reachable states can explode exponentially, compared to a correspond-
ing high-level model. When writing Promela models, for example, great care has
to be taken to make use of atomic (or even dstep ) primitives and resetting dead
temporary variables to default values. However, restrictions of atomic make it
sometimes very dicult or impossible to hide all of the intermediate states. More
details can be found in [17].
Searching for Errors in Large State Spaces. Let us disregard the granularity issue
and let us look at simple problems, with simple datatypes, which can be easily
translated from B to Promela, so that we have a one-to-one correspondence of
the states of the models. In such a setting, one would assume that the spin model
checker for Promela will outperform ProB by several orders of magnitude. In-
deed, spin generates a specialised model checker in C which is then compiled,
whereas ProB uses an interpreter written in Prolog. Furthermore, spin has ac-
crued many optimisations over the years, such as partial order reduction [14,22]