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

5 Future and Related Work and Conclusion
Regarding directed model checking using heuristics there are a number of other
approaches such as a directed extension [10] for Java PathFinder, a tool to mod-
elcheck Java bytecode in order to find deadlocks or problems with null pointers.
Edelkamp et al. describe in [7,6,5] various methods to do directed searches for
counterexamples to LTL properties within spin. A way to use abstraction in
order to direct a model checker is described in [4].
Our experiments have confirmed the conjecture of [17], namely that a mixed
depth-first/breadth-first strategy for model checking is much more robust than
either pure depth-first or breadth-first search. Of particular interest is one indus-
trial model (from Alstom), where neither pure depth-first nor pure breadth-first
was capable of detecting the deadlock. We have presented a new model checking
algorithm for ProB, which stores the pending list of states in a priority queue.
We have presented several heuristic functions and have evaluated them on a wide
variety of B models, including several industrial case studies. The experiments
have shown that directed model checking can provide a considerable performance
improvement. We have shown how one technique, combining the out-degree with
a random component, performs very well for finding deadlocks. An adaption of
the hamming distance for B states has proven to be very effective in guiding the
model checker towards specific goal predicates.
In the future we want to develop more intelligent heuristic functions to guide
ProB, e.g., using information we get from an automatic flow analyzer. We cur-
rently investigate a method to extract information about the control flow of
software systems from Event-B models using a theorem prover. We hope that
flow analysis guided model checking will further improve upon the out-degree
heuristic for finding deadlocks and would also be helpful to find traces to states
where a particular event is enabled. The latter is particularly interesting for
test-case generation.
Acknowledgements. We would like to thank the SBMF reviewers for their feed-
back and many useful suggestions. We are also grateful to the various industrial
partners for giving us access to their B models. This research is being carried out
as part of the DFG funded research project GEPAVAS and the EU funded FP7
research project 214158: DEPLOY (Industrial deployment of advanced system
engineering methods for high productivity and dependability).
References
1. Abrial, J.-R.: The B-Book. Cambridge University Press, Cambridge (1996)
2. Ben-Ari, M.: Principles of the Spin Model Checker. Springer, Heidelberg (2008)
3. Burch, J.R., Clarke, E.M., McMillan, K.L., Dill, D.L., Hwang, L.J.: Symbolic model
checking: 10 20 states and beyond. Information and Computation 98(2), 142-170
(1992)
4. Drager, K., Finkbeiner, B., Podelski, A.: Directed model checking with distance-
preserving abstractions. In: Valmari, A. (ed.) SPIN 2006. LNCS, vol. 3925,
pp. 19-34. Springer, Heidelberg (2006)