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).

More details and examples can be found in the tutorial page on model checking, proof and CBC.

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. In other words, the constraint-based checker verifies that the invariant is inductive.

A comparison between all ProB validation methods can be found on a separate manual page.

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.

Within the command-line version of ProB, there are also several commands available:

• cbc <OP> to check whether an operation preserves the invariant
• cbc_deadlock to check whether the invariant implies that no deadlock is possible
• cbc_assertions to check whether the static assertions (on constants) are implied by the axioms/properties.

The following command is related to the above:

• cbc_sequence <SEQ> to find a sequence of operations using the constraint solver

References