Checking Consistency via Model 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 utilize 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 the types of variables and also may include relationships that must be true in all situations. In other words, it specifies the 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 initialization 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 the number of initializations, times that an operation may be enabled, and the 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 Model Checker

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

By default the model checking 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 selected in the "Search Strategy" pop-up menu.

The two checkboxes "Find Deadlocks" and "Find Invariant Violations" control whether the model checker will report an error when a newly encountered state is deadlocked or respectively violates the invariant.

Similarly, if the model contains assertions (theorems for Event-B models), then the "Find B ASSERTION Violations" checkbox is enabled. You can then control whether the model checker cheeks the assertions (and stops upon encountering a false assertion). Also, if the B Machine contains a DEFINITION for GOAL, then the check box "Find GOAL" becomes enabled. You can then control whether the model checker cheeks the GOAL predicate (and stops when the predicate is true for a new state). More details about assertions and goals can be found below.

The model checker is started by clicking on the "Model Check" button. When the model checker computes and searches the state space, a line prefixed with Searching... at the bottom of the pop-up window will update in real-time the number of nodes that have been computed, until a node violating one of the properties verified has been found or the entire state space has been checked. 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 model checker 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 visualization 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 model checker 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 behavior 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 model checking 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 initializations or the number times than an operation may be enabled 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 visualization features (see State Space Visualization) are then very useful to examine the state space. The features used to visualize 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 deadlock-freeness) 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 model checker 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 presses the Cancel button or until 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" to off and turn either "Check for Deadlocks" or "Check for Invariant Violations" on and the other off. Perform the temporal model check until 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" or purge the state space already computed by reopening the machine. Now deselect the previous property checked, and select the alternative property for checking. Now perform a temporal model check again to search 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 model checking 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 model checking 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 explicitly 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