Warning This page has not yet been reviewed. Parts of it may no longer be up to date

ProB also offers an alternative checking method, inspired by the Alloy ^[1] analyser. In this mode of operation, ProB does not explore the reachable states starting from the initial state(s), but checks whether applying a single operation can result in a property violation (invariant and assertion) independently of the particular initialization of the B machine. This is done by symbolic constraint solving, and we call this approach constraint based checking (another sensible name would be model finding).

Warning: this feature of ProB has not received the same level of attention and testing as the animation or temporal model checking. We have not had the time to put a lot of effort into this feature in the past years, so it will probably only work for simpler B machines.

Difference between Constraint Based Checking and Model Checking

Model checking tries to find a sequence of operations that, starting from an initial state, leads to a state which violates a property. Constraint based checking tries to find a state of the machine that satisfies the property but where we can apply a single operation to reach a state that violates this property. If the constraint based checker finds a counter-example, this indicates that the B specification may contain a problem. The sequence of operations discovered by the constraint based checker leads from a valid state to a property violation, meaning that the B machine may have to be corrected. The valid state is not necessarily reachable from a valid initial state. This situation further indicates that it will be impossible to prove the machine using the B proof rules.

Commands of the Constraint Based Checker

These commands are only accessible in the "Normal" mode of ProB (see General Presentation) and are in the sub-menu "Verify|Constraint Based Checking". The command "Constraint Search for Invariant Violations" will execute the constraint based checking described above to check for invariant violations. The process stops as soon as a counterexample has been found and then displays the counter-example in the animation panes. The command "Constraint Search for Invariant Violations..." enables the user to specify which particular operation leading from the valid state to the invariant violation of the B specification should be considered during the constraint based checking.

The "Constraint Search for Assertion Violations" command executes the constraint based checking looking for assertion violations, while the command "Constraint Search for Abort Conditions" executes it looking for abort conditions.

References