Guided Search for Deadlocks in Actor-Based Models

摘要

Model checking is used to uncover errors by searching the state space of a model. Informed search algorithms use heuristic strategies with problem-specific knowledge to find solutions efficiently. Generally, such heuristics estimate the distance from a given state to a goal state. In this paper, we present seven heuristics for guiding search algorithms through the state-space of actor-based models to a deadlock. In many cases, our methods can find a deadlock more efficiently than uninformed searches. The A~* search algorithm guarantees an optimal solution and returns the shortest counter-example when used with an admissible heuristic. These methods are supported by a tool that performs directed search for the deadlock property. The objective is to detect errors that might not be found by simulation or by conventional model checkers before reaching an upper bound or state-space explosion.