Consistency Checking

By manually animating a B machine it is possible to discover problems with the specification, such as invariant violations or deadlocks. The ProB model checker can do this exploration systematically and automatically. It will alert you as soon as a problem has been found, and will then present the shortest trace (within currently explored states) that leads from an initial state to the error.

The model checker will also detect when all states have been explored, and can thus also be used to formally guarantee the absence of errors. This will obviously only happen if the state space is finite, but the model checker can also be applied to B machines with infinite state spaces and will then explore the state space until it finds an error or runs out of memory.

Basics

During the initial draft of a specification, it is often useful to utilise the model checker to determine if there are any invariant violations or deadlocks. A model checker automatically explores the (finite or infinite) state space of a B machines. Recall, that the INVARIANT specifies both the types of variables and also may include relationships that must hold over them in all situations, that is properties of a B machine that are immutable and must be permanently established.

Since a graph of the visited states and the transformations (operations) between them is retained, it is therefore possible to produce traces (sequence of operations) of invariant violations when they are detected. Such a trace is called a “counter-example” and is useful in determining where and in what circumstances a specification contains errors.

Notice that if the model checker does not find any invariant violations or deadlocks when a traversal of the exhaustive state space has been performed, this does not imply that the specification is a correct specification. This should be understood as the fact that, given the initialisation stated and the model checker preferences set at the time of the check, no errors were found. The main difference is that the ProB animation preferences (such as number of initialisations and enablings, and size of unspecified sets) may be set too low for the exhaustive state space to be covered by the model checking.

As a final caveat, it is not possible to check a machine with an infinite state space. Anecdotal evidence does suggest however, that the model checker does find errors quite quickly. On that basis, it remains a useful tool even for specifications whose state space is infinite.

Using the Temporal Model Checker (TMC)

To model check a B machine loaded in ProB, launch the command from Verify|Temporal Model Check.

The entry Enter max nr. of nodes to check in the pop-up window indicates the number of states that ProB should compute. (This field has disappeared in version 1.3.1.) This computation is done by exploring the state space in a mixed depth-first/breadth-first manner, unless the setting pure Depth or pure Breadth First is toggled on. The two toggles Find Deadlocks and Find Invariant Violations add to this computation a verification of the corresponding property each time a new node is computed. The temporal model checker is started by clicking on the Model Check button. When the TMC computes and searches the state space, a line prefixed with Searching... at the bottom of the pop-up window will update in realtime the number of nodes that have been computed, until the number of nodes indicated in the Enter max nr. of nodes to check entry is reached or a node violating one of the properties verified has been found. The user can interrupt the model checking at any time by pressing the Cancel button.

Incremental Model Checking

It is important to understand that the computation of and search in the state space is an incremental process. The model checking can be done by running the TMC several times; if the number of nodes specified in the entry max nr. of nodes to check is less that the size of the state space that remains to be checked. If the model checking is done in several steps, the end of the model checking step is indicated by the line No error so far, ... nodes visited at the bottom of the pop-up window, unless a violation of the properties (deadlockfreeness, invariant) are found. Between each model checking step, the user can execute the various commands of ProB, notably those of the Analyse menu to display information on the state space (see The Analyse Menu) and the visualisation features (see State Space Visualization).

By default, each model checking step starts from the open nodes of the last computed state space. This means that a change in the settings of the TMC between two steps does not affect the non-open nodes (those already computed), unless there is an alternative path to an already computed node. This behaviour can be changed by toggling on the Inspect Existing Nodes setting. This forces ProB to reevaluate the properties set to be verified on the state space previously computed. Keep in mind that unless the Inspect Existing Nodes setting is on, the change of the TMC settings may not affect the state space already computed.

Results of the Model Checking

When the state space has been computed by ProB, the pop-up window is replaced by a dialog window stating No error state found. All new nodes visited. If ProB finds a node where one of the property that was checked is not verified, it displays a similar pop-up window but with the text Error state was found for new node: invariant violation or Error state was found for new node: deadlock. Then, ProB displays in the animation panes the state of the B machine corresponding to the property violation. From there, the user can examine the state in the State Properties pane, the enabled operations (including the backtrack virtual operation to go back to the valid state that lead to the property violation) in the Enabled Operations pane, and the trace (sequence of operations) leading to the invalid state in the History pane.

Preferences of the Model Checking

The preferences Nr of Initialisations shown and Max Number of Enablings shown (described in Animation Preferences) affect the model checking in exactly the same way as they do for the animation. These preferences are particularly important for the model checking, as setting the number of initialisations or the number of enablings too low will lead to computing and searching a state space that is too small. On the other hand, the user may have to set these preferences to a lower value if the exhaustive state space is too big to be covered by ProB.

Once the state space of the B specification has been computed by ProB, the commands from the Analyse menu (see The Analyse menu) and the visualisation features (see State Space Visualization) are then very useful to examine the state space. The features used to visualise a reduced state space are particularly useful as examining a huge state space may not yield to interesting observations due to excessive cluttering ^[1].

Machines with Invariant Violations and Deadlocks

When the two properties (invariant and deadlockfreeness) are checked and a state violates both , only the invariant violation is reported. In that situation, the deadlock can be observed either from the Enabled Operations (as only the backtrack virtual operation is enabled), or from the state space graph (as the current node has no successors).

During the model checking of a specification which contains both of these errors, it is often useful to be able to focus exclusively upon the detection of one type of error. For example, since an invariant violation is only reported the first time it is encountered, subsequent invocations of the TMC may yield deadlocks whose cause is the invariant violation. This is done by toggling off the corresponding settings of the temporal model checker pop-up window.

HINT: Turning off invariant violation and deadlock detection will simply compute the entire state space until the user press the Cancel button or the specified number of nodes is reached.

Two Phase Verification

If the state space of the specification can be exhaustively searched, check for deadlocks and invariant violations in two phases. To do this, set Inspect Existing Nodes off and set one of Check for Deadlocks or Check for Invariant Violations on and the other off. Perform the temporal model check until either all the deadlocks (resp. invariant violations) are detected or shown to be absent. To recheck the whole state space either turn on the option Inspect Existing Nodes on, or else purge the states space already computed by reopening the machine. Now deselect the previous property to be checked, and select the alternative property for checking. Now perform a temporal model check again searching for a violation of the second property.

HINT: At any time during animation and model checking, the user can reopen the the B specification to purge the state space.

Interleaved deadlock and invariant violation checking

If you wish to determine if an already encountered invariant violation is also a deadlocked node, turn the option Inspect Existing Nodes on, turn Detect Invariant Violations off, and ensure that Detect Deadlocks is on. Performing a temporal model check now will traverse the state space including the previously found node that violates the invariant.

WARNING: Enabling Inspect Existing Nodes will continually report the first error it encounters until that error is corrected.

Specifying Goals and Assertions

The ASSERTIONS clause of a B machine enables the user to define predicates that are supposed to be deducible from the INVARIANT or PROPERTIES clauses. If the B specification opened in ProB contains an ASSERTIONS clause, the TMC pop-up window enables to check if the assertion can be violated. If enabled and a state corresponding to the violation of the assertion is found, a message Error state was found for new node: assertion violation is displayed, and then ProB displays this state in the animation panes

A feature that is similar to the assertions is the notion of a goal. A goal is a macro in the DEFINITIONS section whose name is GOAL and whose content is a predicate. If the B specification defines such a macro, the TMC pop-up window enables to check if a state satisfies this goal. If enabled and a state corresponding to the goal is found, a message State satisfying GOAL predicate was found is displayed, and then ProB displays this state in the animation panes.

It is also possible to find a state of the B machine that satisfies such a goal without defining it explicitely in the B specification. The Verify|Advanced Find... command enables the user to type a predicate directly in a text field. ProB then searches for a state of the state space currently computed that satisfies this goal.

References