Constraint-Based Deadlock Checking Sample Clauses

Constraint-Based Deadlock Checking. Ensuring the absence of deadlocks is important for certain applications, in particular for Bosch's Cruise Control. We are tackling the problem of finding deadlocks via constraint solving rather than by model checking. Indeed, model checking is problematic when the out-degree is very large. In particular, quite often there can be a practically infinite number of ways to instantiate the constants of a B model. In this case, model checking will only find deadlocks for the given constants chosen. The basic idea is to generate deadlocks by solving a constraint consisting of the axioms Ax, the invariants Inv together with a constraint D specifying a deadlock. More formally, D is the negation of the disjunction of all the guards. The following tool developments were required to meet the challenges raised by the industrial application: • generation of the deadlock freedom proof obligation by ProB (to avoid dependence on other plug-ins and being able to control whether theorems are to be used or not; currently they are not used) • implementation of a constraint-based deadlock checking algorithm: • with the possibility to specify an additional goal predicate to restrict the deadlock search to certain scenarios: in Bosch's case due to the flow plugin, one wants to restrict deadlock checking e.g. to states with the variable Counter set to 10 • with semantic relevance filtering (to be able to filter out guards which are always false given the goal predicate). • with partitioning of the constraint predicate into components and optionally reordering according to usage (basic predicates which occur in most guards are listed first) • Improvements to ProB's constraint solving engine: (reification of constraints, detection of common sub-predicates, more precise information propagation for membership constraints, performance improvments in the typchecker and other parts of the kernel). ProB has been applied successfully to two models of the adaptive cruise control by Bosch. The more complicated model is CrCtrl_Comb2Final. To give an idea, here are some statistics of the deadlock freedom proof obligation for CrCtrl_Comb2Final: • when printed in 9-point Courier ASCII the formula takes 32 A4 pages (the disjunction of the guards starts at page 6) • the model contains 59 events with 837 guards (19 of them disjunctions, some of which themselves nested) • Bosch are interested in deadlocks that are possible according to a flow specified using the flow plugin; these can be found with ...