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

3 Depth-First versus Breadth-First: An Empirical
Evaluation

We report on experiments conducted with ProB using pure depth-first, pure
breadth-first, as well as the default mixed depth-first/breadth-first approach of
ProB. We also investigate several variations of the mixed approach, varying the
probability with which a depth-first step is conducted.

3.1 The Models

We have chosen a variety of case studies for evaluating the effectiveness the
various model checking techniques. All models are either classical B models or
Rodin Event-B models. We have included several industrial specifications (some
stemming from various EU projects, such as Rodin and Deploy 1 ), as well as
academic specifications of various intricate algorithms. There are a few artificial
benchmarks as well, testing specific aspects of the model checking algorithm. We
have also included some classical puzzles as well, in particular to test directed
model checking.
The case studies have been partitioned into four classes:

1. Models with invariant violations,
2. Models with deadlocks,
3. Models with no errors (i.e., no deadlocks or invariant violations), but where
a particular goal predicate is to be found. Indeed, in ProB the user can
define a particular goal predicate and ask the model checker to find states
which make the predicate true. The main difference with point 1 is that the
goals are often much more precise (sometimes a concrete particular state)
than the invariant violations.
4. Models with no errors, and where the full state space needs to be explored.

A description of the models can be found in the extended version of the paper
[18]. Along with the extended version of the paper [18] we have also included
the publicly available models.

3.2 The Results

The results are summarised in Tables 1-6 in the Appendix A. Due to space
restrictions, we have not included the times for the models without errors; this
information can be found in [18]. Relative times are computed with ProB using
a mixed depth-first/breadth-first strategy with one-third probability of going
depth-first. We call this the reference settings of ProB (prior to the publication
of this paper this used to be the default setting; more on that below). The
experiments were run on a MacBook Pro with a 3.06 GHz Core2 Duo processor,
and ProB 1.3.2 compiled with SICStus Prolog 4.1.2.

1 EU funded FP7 research project 214158: DEPLOY (Industrial deployment of ad-
vanced system engineering methods for high productivity and dependability).