Using heuristic search for finding deadlocks in concurrent systems

Model checking is a formal technique for proving the correctness of a system with respect to a desired behavior. This is accomplished by checking whether a structure representing the system (typically a labeled transition system) satisfies a temporal logic formula describing the expected behavior. Model checking has a number of advantages over traditional approaches that are based on simulation and testing: it is completely automatic and when the verification fails it returns a counterexample that can be used to pinpoint the source of the error. Nevertheless, model checking techniques often fail because of the state explosion problem: transition systems grow exponentially with the number of components. The aim of this paper is to attack the state explosion problem that may arise when looking for deadlocks in concurrent systems described through the calculus of communicating systems. We propose to use heuristics-based techniques, namely the A* algorithm, both to guide the search without constructing the complete transition system, and to provide minimal counterexamples. We have realized a prototype tool to evaluate the methodology. Experiments we have conducted on processes of different size show the benefit from using our technique against building the whole state space, or applying some other methods.