ProB is a model checker for high-level formalisms such as B, Event-B, CSP and Z. ProB uses a mixed depth-first/breadth-first search strategy, and in previous work we have argued that this can perform better in practice than pure depth-first or breadth-first search, as employed by low-level model checkers. In this paper we present a thorough empirical evaluation of this technique, which confirms our conjecture. The experiments were conducted on a wide variety of B and Event-B models, including several industrial case studies. Furthermore, we have extended ProB to be able to perform directed model checking, where each state is associated with a priority computed by a heuristic function. We evaluate various heuristic functions, on a series of problems, and find some interesting candidates for detecting deadlocks and finding specific target states. © 2011 Springer-Verlag Berlin Heidelberg.
CITATION STYLE
Leuschel, M., & Bendisposto, J. (2011). Directed model checking for B: An evaluation and new techniques. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 6527 LNCS, pp. 1–16). https://doi.org/10.1007/978-3-642-19829-8_1
Mendeley helps you to discover research relevant for your work.