Institut für Informatik
Softwaretechnik und Programmiersprachen

We have a new website! These are the old archived pages.

For our up-to-date pages, please visit our new website.

Constraint-Based Deadlock Checking of High-Level Specifications

AuthorsStefan Hallerstede, Michael Leuschel
TitleConstraint-Based Deadlock Checking of High-Level Specifications
Published Proceedings ICLP'2011, 2011, Cambridge University Press
AbstractEstablishing 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 we 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. We present the general technique, as well as various improvements that had to be performed on ProB's Prolog kernel, such as reification of membership and arithmetic constraints. % boolean constraint solver with reification This work was guided by an industrial case study, where a team from Bosch was modeling a cruise control system. Applied to this case study ProB typically finds counter examples to deadlock-freedom constraints, a formula of about 900 partly nested conjunctions and disjunction among them 80 arithmetic and 150 set-theoretic predicates (in total a formula of 30 pages), in under two seconds. We also present other successful applications of this new technique, in particular to BPEL processes. Experiments using SAT and SMT solvers on these constraints were thus far unsuccessful.
Keywords ProB, Constraint Programming, Formal Methods
NoteTo appear.