Information Technology Reference
In-Depth Information
In conclusion, breadth-first on its own is not appropriate, except in special cir-
cumstances. Note, a user can set ProB into breadth-first mode, but the default
is another setting (see below).
Mixed Depth-first/Breadth-first. The motivation behind ProB's mixed
depth-first/breadth-first 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 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.
An interesting real-life benchmark is Alstom ex7: here both pure depth-first and
pure breadth-first fail to find the deadlock. However, the mixed strategy finds
the deadlock.
We have experimented with four different versions of the mixed strategy:
DF75, DF50, DF33, DF25. The reference setting was DF33, where there is a
33 % chance of going depth-first at each step. Best overall geometric mean is
obtained when using DF50 (which is now the new default setting of ProB).
In summary, let us look at the radar plots in Table 7 in Appendix A, where we
summarise the results for pure depth-first, pure breadth-first, the old reference
setting and the new one. We can clearly see the quite erratic performance of pure
depth-first (relative to the reference setting), and the less erratic but usually
worse performance of pure breadth-first. We can also see that the new reference
setting usually lies within the reference setting circle, smoothing out most of the
(bad) erratic behaviour of the pure depth-first approach.
4 Evaluating Directed Model Checking
Directed Model Checking uses additional information about the model or the
destination state in form of a heuristic that guides the model checker towards
a target state. This additional information can be collected using for instance
static analysis or it can be given by the modeler.
Currently the state space of ProB is stored as a Prolog fact database. Every
state can be quickly accessed using its ID or using the hash-value of its state.
The model checker also maintains a pending list of open states, using two addi-
tional Prolog predicates: retracting a Prolog fact from one of the predicates yields
the most recently added open state (for depth-first traversal) and retracting from
 
Search WWH ::




Custom Search