Biased model checking using flows

Abstract

We describe two new state exploration algorithms, called biased-dfs and biased-bfs, that bias the search towards regions more likely to have error states using high level hints supplied by the user. These hints are in the form of priorities or markings describing which transitions are important and which aren't. We will then describe a natural way to mark the transitions using flows or partial orders on system events. Apart from being easy to understand, flows express succinctly the basic organization of a system. An advantage of this approach is that assigning priorities does not involve low level details of the system. Using flow-derived priorities we study the performance of the biased algorithms in the context of cache coherence protocols by comparing them against standard bfs, dfs and directed model checking. Preliminary results are encouraging with biased-bfs finding bugs about 3 times faster on average than standard bfs while returning shortest counter examples almost always. Biased-dfs on the other hand is couple of orders of magnitude faster than bfs and slightly faster than even standard dfs while being more robust than it. © 2011 Springer-Verlag.