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

and bitstate hashing [12]. However, even in this setting, this advantage of spin
does not necessarily translate into better performance for real-life scenarios, in
particular when using the model checker as a debugging tool for software systems,
i.e., trying to find errors in a very large state space.
One experiment reported on in [17] is the NastyVendingMachine. It has a very
large state space, where there is a systematic error in one of the operations of the
model (as well as a deadlock when all tickets have been withdrawn). To detect the
error, it is important to exercise this operation repeatedly. It is not important to
generate long traces of the system, but it is important to systematically execute
combinations of the individual operations. This explains why depth-first behaves
so badly on this model, as it will always try to exercise the first operation of the
model first. Note that a very large state space is a typical situation in software
verification (sometimes the state space is even infinite).
Fortunately, spin provides a breadth-first option, with which it then finds
the above error very quickly. However, for another class of problems, breadth-
first fares badly. Indeed, in a corrected non-deadlocking model of the vending
machine in [17], with again a large state space, the error occurs if the system
runs long enough: it is not very critical in which order operations are performed,
as long as the system is running long enough. This explains why for this model
breadth-first was performing badly, as it was not generating traces of the system
which were long enough to detect the error.
In order to detect both types of errors with a single model checking algorithm,
ProB has been using a mixed depth-first and breadth-first search [20]. More
precisely, at every step of the model checking, ProB randomly chooses between
a depth-first and a breadth-first step.
In summary, the motivation behind ProB's heuristic is that many errors in
software models fall into one of the following two categories:
- Some errors are due to an error in a particular operation of the system; hence
it makes sense to perform some breadth-first exploration to exercise all the
available functionality. In the early development stages of a system model,
this kind of error is very common.
- Some errors happen when the system runs for a long time; here it is often
not so important which path is chosen, as long as the system is running
long enough. An example of such an error is when a system fails to recover
resources which are no longer used, hence leading to a deadlock in the long
run.
Thus, if the state space is very large, depth-first search can perform very badly
as it fails to systematically test combinations of the various operations of the
system. Even partial order reduction and bitstate hashing often do not help.
Similarly, breadth-first search can perform badly, failing to locate errors that
require the system to run for very long. We have argued that ProB's combined
depth-first breadth-first search with a random component does not have these
pitfalls. In the next section, we will validate this claim empirically.