Finding Deadlocks of Event-B Models by Constraint Solving
Establishing the absence of deadlocks is important in many applications of formal methods. The use of model checking for finding deadlocks in formal models is limited because in many industrial applications the state space is either infinite or much too large to be explored exhaustively. In this paper, the authors propose a constraint-based approach to finding deadlocks employing the ProB constraint solver to find values for the constants and variables of formal models that describe a deadlocking state. They discuss the principles of the technique implemented in ProB's Prolog kernel and present some results of a larger case study to which they have applied the approach.