Also see the following tutorials:
ProB offers various validation techniques:
Here we want to describe the advantages and disadvantages of the various methods.
Question | Model Checking | LTL Model Checking | CBC Checking | Bounded Model Checking |
---|---|---|---|---|
Can find Invariant Violations ? | yes | yes (G{INV}) | yes | yes |
Only reachable counter-examples from initial state? | yes | yes | no | yes |
Search Technique for counter-examples? | mixed df/bf, df, bf | depth-first (df) | length 1 | breadth-first (bf) |
Can deal with large branching factor? | no | no | yes | yes |
Can find deep counter-examples? | yes | yes | n/a (length 1) | no |
Can find deadlocks ? | yes | yes (G not(deadlock)) | yes | not yet |
Can find assertion violations ? | yes | (G{ASS}) | static | no |
Can confirm absence of errors ? | finite statespace | finite statespace | invariant strong enough | bound on trace length |
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.
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.
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. As of version 1.5.1, additional options for directed model checking are available. For example, one can have truly random exploration or provide a custom heuristic function to guide the model checker. These features are illustrated using the the blocks world example.
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.
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.
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.
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]}.
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.
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.
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.
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.
Distributed Model Checking allows to check invariants and deadlock-freedom (and assertions) with additional computational power. The distributed version of ProB is named distb. In the following, we will document how to run it.
distb consists of three components.
It might be necessary to increase the limits of how much shared memory may be allocated, both per segment and overall. This is, to our knowledge, required for Mac OS X and older versions of Ubuntu. You can view the limits by running:
sysctl -a | grep shm
Per default, recent versions of Ubuntu set the following values:
kernel.shmall = 18446744073692774399 kernel.shmmax = 18446744073692774399 kernel.shmmni = 4096
On Mac OS X, the keys might be different and you can set them by executing:
sudo sysctl -w kern.sysv.shmmax=18446744073692774399 sudo sysctl -w kern.sysv.shmseg=4096 sudo sysctl -w kern.sysv.shmall=18446744073692774399
Run once per machine:
/path/to/prob/lib/proxy $MASTER_IP 5000 $IP 30 $LOGFILE_PROXY $PROXY_NUMBER
Note that on Linux systems you might need to set the LD_LIBRARY_PATH variable to find the ZeroMQ libraries beforehand (for all components):
export LD_LIBRARY_PATH=/path/to/prob/lib
Run once per model checking:
/path/to/prob/probcli -bf -zmq_master <unique identifier> $MODEL
Run as many workers as you want:
/path/to/prob/probcli -zmq_worker <unique identifier> &
You can fine-tune the following parameters by adding -p NAME VALUE to the corresponding call (e.g., ./probcli -zmq_worker worker1 -p port 5010 -p max_states_in_memory 100) :
Parameter | Default | Description | Applicable for... |
---|---|---|---|
port | 5000 | TCP ports should be used starting at... | master, worker |
ip | localhost | IP of the master component | master |
max_states | 0 | how many states should be checked at most (0 means all) | master |
tmpdir | /tmp/ | directory for temporary files | master, worker |
logdir | ./distb-logs | directory for log output (must exist) | master, worker |
proxynumber | 0 | which proxy should the component connect to (if multiple run on the same machine) | worker |
max_states_in_memory | 1000 | how many states may be kept in memory before written into a database | worker |
hash_cycle | 25 | minimum amount of milliseconds that has to pass between hash code updates from the master | master |
We used three different setups to evaluate the distributed version of ProB.
We used a hexacore 3.33GHz Mac Pro with 16GB of RAM. On this computer we benchmarked all models regardless whether we expected them to be scalable or not. We varied the number of used cores from 1 up to 12 hyperthreads. Each experiment was repeated at least 5 times.
We used c3.8xlarge instances, each of which has 32 virtual CPUs and is equipped with 64 GB of RAM. We used the Mac Pro to get an impression if and how well the B models scale. From the experiments, we chose those models that seemed to scale well and ran the benchmarks on the Amazon EC computer with a higher number of workers. Models that did not scale on the Mac Pro were not considered as they would not scale on more processors. We used 2 or 4 instances connected with 10 GBit ethernet connection. Each experiment was repeated at least 5 times.
We used the high performance cluster at the university of Düsseldorf (HILBERT) for a single model. The model could not be cheked using a single core because it would have taken too long. Based on a partial execution, it would take about 17 days on a single core on the Mac Pro. The model was checked with different numbers of cores on the HILBERT cluster. We varied between 44 and 140 cores. On the cluster we only executed the experiments once but all experiments on the other platforms indicated that the variation between experiments could be ignored. Also the execution times of all 6 experiments seem to be consistent.
We cannot make all models public, because they we provided by industrial partners from various research projects. The models that could be make available can be downloaded from [3]
The results of the experiments are shown in Jens Bendisposto's dissertation. A preprint is available from [4] Warning: Display title "Handbook/Validation" overrides earlier display title "Distributed Model Checking : Experimental evaluation".
This page explains how to run the distributed model checking prototype.
Note that the implementation does not work with Windows, only Linux andMac OS are supported.
It is required to set the limits for shared memory on some systems, this can be done using sysctl. Here is a little script that sets the limits. It takes the size of shared memory as parameter (usually the size of your memory in GB). You need to run the script with root rights.
#!/bin/bash if [ $# -gt 0 ]; then echo "Setting SHM sizes:" sysctl -w kern.sysv.shmmax=`perl -e "print 1073741824*$1"` sysctl -w kern.sysv.shmseg=4096 sysctl -w kern.sysv.shmall=`perl -e "print 262144*$1"` echo "Here are the current values:" sysctl -a | grep shm else echo "You need to provide the size of shared memort (in full GB)" fi
After setting up shared memory, you can use the parB.sh script that comes with the ProB distribution (see Download).
Usage
./parB <Nr. of workers> <file> [preferences to master/workers]
Example usage:
$ ./parB.sh 2 ~/parB.log scheduler.mch
The script can only be used for computation on a single physical computer. If you want to use multiple computers, the setup is a bit more complex:
lib/hasher <MASTER_IP> <MASTER_PORT> 1
probcli -zmq_worker2 <MASTER_IP> <MASTER_PORT> 0
probcli -zmq_master2 <MIN QUEUE SIZE> <MAX NR OF STATES> <MASTER_PORT> 0 <LOGFILE> <MODEL_FILE>
The minimal queue length is used to determine if a worker is allowed to share its queue. The experiments have shown, that a number between 10 and 100 is fine. parB will stop after (at least) the maximal number of states have been explored, a value of -1 will explore all states (beware of this, if the state space is infinite!).
As a rule of thumb use one real core for each of the processes. On hyperthreads the model checking still becomes faster, but the speedup is only 1/4 for each additional hyperthread.
We plan to develop a control interface that allows configuring the logical network in a more convenient way and running the model checker from within ProB.
You can use preferences in parB.sh (and the master) :
./parB <Nr. of workers> <logfile> <file> <additional probcli options> ./probcli <additional probcli options> -zmq_master2 <MIN QUEUE SIZE> <MAX NR OF STATES> <MASTER_PORT> 0 <LOGFILE> <MODEL_FILE> <additional probcli options>
If you use -strict, parB will stop as soon as a violation is found, otherwise parB will explore the full state space (up to the maximal number of states)
If something goes wrong it may be necessary to clean up your shared memory. You can find out if there are still memory blocks occupied using ipcs. Removal can be done using:
ipcrm -M `ipcs | grep <YOUR USERNAME> | grep -o "0x[^ ]*" | sed ':a;N;$!ba;s/\n/ -M /g'`
#!/bin/bash PROBCOMMAND=probcli if [ $# -lt 2 ] then echo "Too few parameters ($#) for parB" echo "Usage ./parB <Nr. of workers> <file> [preferences to master/workers]" exit -1 else PARB=$0 CORES=$1 FILE=$2 shift shift echo "Running ProB in Parallel (on .prob files)" # dirname if [ -h "$PARB" ] then realname=`readlink "$PARB"` dirname=`dirname "$realname"` else dirname=`dirname "$PARB"` fi #ulimit -d unlimited echo "Directory: $dirname" # dirname if [ -h "$PARB" ] then realname=`readlink "$PARB"` dirname=`dirname "$realname"` else dirname=`dirname "$PARB"` fi #ulimit -d unlimited # setting the library path to find the zmq shared libraries system=`uname` if [ $system = "Linux" ]; then export LD_LIBRARY_PATH="$dirname/lib${LD_LIBRARY_PATH:+:${LD_LIBRARY_PATH}}" fi echo "Directory: $dirname" echo "Starting workers in parallel" echo "$dirname/$PROBCOMMAND -zmq_worker <worker-id> $*" for (( i = 0 ; i < $CORES; i++ )) do "$dirname/$PROBCOMMAND" -zmq_worker $i $* & done ##Usage: ./proxy <master IP> <port start> <own IP> <queue threshold> <logfile> [<proxynumber>] echo "Starting proxy server: $dirname/lib/proxy localhost 5000" "$dirname/lib/proxy" localhost 5000 localhost 50 loggyMcLogface-proxy & echo "Starting master: $dirname/$PROBCOMMAND -bf -zmq_master master $FILE $*" time "$dirname/$PROBCOMMAND" -bf -zmq_master master $FILE $* fi
This file provides a few more options:
#!/bin/bash PROBCOMMAND=probcli if [ $# -lt 5 ] then echo "Usage ./parB2 <Nr. of workers> <minimum que size> <max number of states> <Port (usually 5000)> <logdir> <model>" exit -1 else echo "Running ProB in Parallel (on .prob files)" # dirname if [ -h "$0" ] then realname=`readlink "$0"` dirname=`dirname "$realname"` else dirname=`dirname "$0"` fi ulimit -d unlimited echo "Directory: $dirname" mkdir -p $5 # dirname if [ -h "$0" ] then realname=`readlink "$0"` dirname=`dirname "$realname"` else dirname=`dirname "$0"` fi ulimit -d unlimited # setting the library path to find the zmq shared libraries system=`uname` if [ $system = "Linux" ]; then export LD_LIBRARY_PATH="$dirname/lib${LD_LIBRARY_PATH:+:${LD_LIBRARY_PATH}}" fi echo "Directory: $dirname" #cd $dirname #ls echo "Starting workers in parallel" for (( i = 0 ; i < $1; i++ )) do "$dirname/$PROBCOMMAND" -bf -zmq_worker $i -p logdir $5 & done echo "Starting proxy server: $dirname/lib/proxy localhost $4 localhost $2 $5/log-proxy " "$dirname/lib/proxy" localhost $4 localhost $2 $5/log-proxy & echo "Starting master: $dirname/$PROBCOMMAND -bf -zmq_master master -p queue_threshold $2 -p max_states $3 -p port $4 -p logdir $5" time "$dirname/$PROBCOMMAND" -bf -zmq_master master $6 -p queue_threshold $2 -p max_states $3 -p port $4 -p logdir $5 fi
ProB provides support for LTL (linear temporal logic) model checking. For an introduction to LTL see the Wikipedia Article.
To use this feature, select "Check LTL/CTL Assertions" in the "Verify" menu. The feature can also be accessed by the key combination "Ctrl+L" under Windows and Linux, and by the key combination "Cmd+L" under MacOS. The following window appears:
All LTL formulas that are given in the "DEFINTIONS" section of a B machine are displayed in the list box of the LTL/CTL Assertions Viewer. For CSP-M specifications all LTL formulas given in the LTL pragmas of the loaded CSP-M file will be shown in the viewer. (For more detailed information of how LTL/CTL assertions can be stored into B and CSP-M models see Section Storing LTL Assertions into a Model).
A new LTL formula can be entered in the entry below the list box. (We explain the supported syntax below). The typed formula can then be either added to the list box by clicking the "Add" button or directly checked by clicking the "Check" button. Before doing that assure whether you are in the proper frame ("Add LTL Formula") of the bottom part of the LTL viewer.
The LTL model checker can be started for an LTL formula by performing a double-click on the respective formula or typing "Enter" after selecting the respective formula. Each LTL formula in the list box has on the left hand side a symbol that indicates what is the status of the respective formula. An LTL formula can have one of the following statuses (status symbols may differ under different operating systems):
All formulas can be checked by "Assertions -> Check All Assertions" in the menu bar. All formulas will be then checked from top to bottom in the list box.
Additionally, the viewer provides a context menu for the list box elements. The context menu can be popped-up by a right-mouse-click on a formula from the list box, and it performs a set of actions available to be performed on the currently selected formula (see Figure below).
The old LTL and CTL dialogs can be accessed from "OldLtlViewers" in the menu bar.
There is a set of options coming with the LTL model checker. In this section we give a brief overview of the preferences. The LTL preferences can be viewed by selecting "LTL Preferences" in the "Preferences" menu of the LTL/CTL Assertions Viewer.
Exploring new states
The LTL model checker searches in the already explored search space of the model. If a state is encountered that has not been explored before, the state will be explored (i.e. all transitions to successor states are computed). The number of how often this can happen is limited by the field "Max no. of new states".
Depending on the LTL formula, a partially explored state space can be sufficient to find a counterexample or to assure the absence of a counterexample. If there's still the possibility of a counterexample in the remaining unexplored state space, the user will get a message.
Optimizing the process of LTL model checking
The process of model checking can be optimized for B and Event-B models by using partial order reduction. The idea of partial order reduction is to execute only a subset of all enabled actions in each state. Thus, only a part of the original state space is checked for the checked property. The reduction of the state space depends on the number of concurrent and independent actions in the model, as well as on the property being checked.
With Safety Check
This checks whether a formula is a safety property or not.
If it is, this property is treated in an optimised way.
In some cases, this means that not the entire state space has to be computed.
For this optimisation to work, ProB needs the LTL2BA translator.
You can download and put it into ProB's lib folder, by choosing
Download and Install LTL2BA Tool
from the Help menu. More details can be found below.
Search Options
The model checker searches for a counterexample (i.e. a path that does not satisfy the current formula). Where the checked paths through the model's search space start depend on the following options in the LTL Preferences’ menu:
Note: Whereas `Y true` is always false when checked with option 1 or 2, it is usually true (but not in all cases) for option 3.
ProB supports LTL^{[e]}, an extended version of LTL. In contrast to the standard LTL, LTL^{[e]} provides also support for propositions on transitions, not only on states. In practice, writing propositions on transitions is allowed by using the constructs `e(...)` and `[...]`. (see below). The LTL model checker of ProB supports Past-LTL^{[e]} as well.
For safety properties ProB uses another checking algorithm, to avoid having to explore the entire SCC (strongly connected component) of a counter example. In general this requires installing the LTL2BA tool (see Help menu), but the following patterns are supported directly without LTL2BA:
G StateProposition G (StateProposition => X StateProposition)
where StateProposition is either an atomic proposition ({Pred}, e(Op), [Op], deadlock,...) or a propositional operators (not, &, =>, or) applied to StatePropositions.
Here are a few example patterns covered by the above:
G {Pred} Invariant G(e(Op) => {Pred}) Necessary precondition for operation Op G({Pred} => e(Op)) Sufficient precondition for operation Op G([Op] => X{Pred}) Postcondition of operation Op G(e(Op1) => not(e(Op2))) Enabling relations between operations G(not(deadlock(Op1,...,Opk))) Relative deadlock freedom G(deterministic(Op1,...,Opk)) Relative deadlock freedom G(controller(Op1,...,Opk)) Relative deadlock freedom and determinism
Fairness is a notion where the search for counterexamples is restricted to paths that do not ignore infinitely the execution of a set of enabled operations imposed by the user as "fair" constraints. One possibility to set fairness constraints in ProB is to encode them in the LTL^{[e]} formula intended to be checked. For example, for a given LTL^{[e]} formula "f" a set of weak fairness conditions {a1,…,an} can be given as follows:
(FG e(a1) => GF [a1]) & … & (FG e(an) => GF [an]) => f.
In a similar way, strong fairness constraints can be imposed expressed by means of an LTL^{[e]} formula:
(GF e(a1) => GF [a1]) & … & (GF e(an) => GF [an]) => f.
Checking fairness in this way is very often considered to be inefficient as usually the number of atoms (the possible valuations of the property) of the LTL property is exponential in the size of the formula.^{[1]} For this reason, the search algorithm of the LTL model checker has been extended in order to allow fairness to be checked efficiently. In addition, new operators have been added to the ProB’s LTL parser for setting fairness constraints to an LTL^{[e]} property. The new operators are WF(-) and SF(-) and both accept as argument an operation. The fairness constraints must be given by means of implication: "fair => f", where "f" is the property to be checked and "fair" the fairness constraints.
In particular, "fair" can have one of the forms: "wfair", "sfair", "wfair & sfair", and "sfair & wfair", where "wfair" and "sfair" represent the imposed weak and strong fairness constraints, respectively.
Basically, "wfair" and "sfair" are expressed by means of logical formulas having the following syntax:
For instance, if we want to check an LTL property "f" on paths that are weak fair in regard to the operations "a" and "b" and additionally strong fair in regard to "c" or "d", then this can be given as follows:
(WF(a) & WF(b)) & (SF(c) or SF(d)) => f
Note that the operators WF(-) and SF(-) cannot appear on the right side of the fairness implication. Basically, WF(-) and SF(-) can be described by the following equivalences:
WF(a) ≡ (FG e(a) => GF [a]) and SF(a) ≡ (GF e(a) => GF [a]), where a is an operation.
For setting fairness constraints on all possible operations of the model being checked use the operators "WEF" and "SEF". For instance, if "f" is a liveness property and we want to restrict the search only to strongly fair paths, then we can impose the fairness constraints by means of the formula "SEF => f".
The grammar for imposing fairness constraints by means of the fairness implication ("fair => f") looks as follows:
fair ::= WEF | SEF | wfair | sfair | wfair & sfair | sfair & wfair
wfair ::= wf(a) | ( wfair ) | wfair & wfair | wfair or wfair
sfair ::= sf(a) | ( sfair ) | sfair & sfair | sfair or sfair
where "a" is a transition proposition.
Storing LTL formulas in B machines
LTL formulas can be stored in the `DEFINITIONS` section of a B machine. The name of the definition must start with `ASSERT_LTL` and a string must be specified. In case there is more than one LTL assertion given in the ‘DEFINITIONS’ section, the particular LTL assertions must be separated by semicolon. For example:
DEFINITIONS ASSERT_LTL == "G (e(SetCruiseSpeed) => e(CruiseBecomesNotAllowed))"; ASSERT_LTL1 == "G (e(CruiseBecomesNotAllowed) => e(SetCruiseSpeed))"; ASSERT_LTL2 == "G (e(CruiseBecomesNotAllowed) => (ObstacleDisappears))"
Storing LTL formulas in CSP-M specifications
LTL formulas can be stored within pragmas in CSP-M specifications. A pragma in which a single LTL formula is stored is given by "{-# assert_ltl "f" "c" #-}", where "assert_ltl" indicates the type of the information stored in the pragma (there are currently two types: assert_ltl and assert_ctl), and is followed by the LTL formula `f` and a comment `c` (the comment is optional). Both, the LTL formula and the comment, must be enclosed in double quotes.
It is also possible to give several LTL formulas in a single pragma within which the corresponding LTL assertions are separated by semicolon. For example:
{-# assert_ltl "SF(enter.1) & WF(req.1) => GF([enter.1])"; assert_ltl "SF(enter.2) & WF(req.2) => GF([enter.2])"; assert_ltl "GF [enter.1] & GF [enter.2]" "Should fail."#-}
Note that a semicolon must not follow the last assertion in a pragma.
For CSP-M specifications, it is also possible to assert LTL-formulae to particular processes in the model. This is possible by means of ``assert`` declarations, which have been recently included to the CSP-M grammar of the ProB CSP-M parser:
assert P |= LTL: "ltl-formula", where `P` is an arbitrary process and `ltl-formula` an LTL formula.
With the command line version of ProB it is possible to check several LTL^{[e]} formulae with one call. The command has the following syntax
probcli -ltlfile FILE ...
The file FILE contains one or more sections where each section has the form
[Name] Formula
The formula itself can spread several lines. Additional comments can be added with a leading #. If a counter-example is found, the trace of the counter-example is saved into the file ltlce_Name.trace, where "Name" is the name of the formula in the LTL file.
One also can check a single LTL^{[e]} formula F using the option '-ltlformula' as follows:
probcli -ltlformula "F" ...
With the command line version of ProB it is possible to check several LTL^{[e]} formulae with one call. The command has the following syntax
probcli -ltlfile FILE ...
The file FILE contains one or more sections where each section has the form
[Name] Formula
The formula itself can spread in several lines. Additional comments can be added with a leading #. If a counter-example is found, the trace of the counter-example is saved into the file ltlce_Name.trace, where "Name" is the name of the formula in the LTL file.
One also can check a single LTL^{[e]} formula F using the option '-ltlformula' as follows:
probcli -ltlformula "F" ...
The output provided by the LTL model checker can sometimes reveal some interesting statistical facts about the model and the property being checked on the model. The LTL model checker of ProB uses the tableau approach for checking an LTL^{[e]} formula on a formal model. To check whether a model M satisfies a given formula f, the algorithm generates a search graph, called also tableau graph, composed from the tableau of the formula and the state space of the model. If there is a path in the search graph that is a model for f, then the formula is satisfiable. The nodes of the search graph are called atoms.
Basically, using the tableau approach we prove that M satisfies f by negating the given formula and searching for a path fulfilling ¬f. If such a path is found, then we infer that M violates f. Otherwise, if no path is found that satisfies ¬f, we conclude that M |= f. The LTL model checking algorithm of ProB is based on searching for strongly connected components (SCCs) with certain properties to determine whether M satisfies f. Finding such an SCC that can be reached from an initial state of M is a witness for a counter-example for f. Sometimes, we use fairness to ignore such SCCs that do not fulfill the imposed fairness constraints in order to not impede proving a property by returning of non-fair paths as counter-examples.
The LTL model checker algorithm of ProB is implemented in C using a callback mechanism for evaluating the atomic propositions and the outgoing transitions in SICStus Prolog. (For each state of the model a callback will be performed.) Additionally, the search for SCCs is based on the Tarjan's algorithm. In the terminal all messages coming from the LTL model checker are preceded either by "LTL (current statistics): " or "LTL model checking:". The output from the LTL model checker can give helpful insights about the model and the model checking process.
Consider the CSP specifications "dphil_ltl8.csp" representing a model of the dining philosophers problem for eight philosophers which resolves the starvation problem by always forcing the first philosopher to pick up first the right fork instead of the left one. In other words, "dphil_ltl8.csp" has no deadlock states. Checking the LTL formula "GF [eat.0]" from the command line will produce the following output:
$ probcli -ltlformula "GF [eat.0]" dphil_ltl8.csp .... LTL model checking formula % parsing_ltl_formula % initialising_ltlc starting_model_checking LTL (current statistics): 13280 atoms, 10070 transitions generated, and 2631 callbacks needed. LTL model checking: found counter-example (lasso-form): intro length = 1126, path in SCC of length = 5 LTL model checking: memory usage approx. 1924 KiB, 14104 atoms and 10724 transitions generated LTL model checking: total time 22492ms, 2803 callbacks needed 22465ms, netto 26ms. ! An error occurred ! ! source(ltl) ! Model Check Counter-Example found for: ! GF [eat.0] Formula FALSE. Runtime: 22220 ms ! *** error occurred *** ! ltl
As one can clearly see from the output, the LTL model checker fails to prove "GF [eat.0]" on the model since it has found a counter-example for the formula. Note that the ProB LTL model checker explores the search graph and the state space dynamically. The above data is to be understand as follows:
In the example above one can prove the LTL^{[e]} formula "GF [eat.0]" on dphil_ltl6.csp using fairness. One can impose, for example, strong fairness conditions on all transitions of the model and thus verify that "GF [eat.0]" is satisfied under strong fairness. The call looks as follows:
$ probcli -ltlformula "SEF => GF [eat.0]" dphil_ltl8.csp ... LTL model checking formula % parsing_ltl_formula % initialising_ltlc starting_model_checking LTL (current statistics): 13016 atoms, 9834 transitions generated, and 2578 callbacks needed. LTL (fairness): 0 strongly connected components were rejected, 0 callbacks needed. LTL (current statistics): 27540 atoms, 44422 transitions generated, and 5123 callbacks needed. LTL (fairness): 284 strongly connected components were rejected, 843 callbacks needed. ..... LTL (current statistics): 85980 atoms, 267821 transitions generated, and 19733 callbacks needed. LTL (fairness): 454 strongly connected components were rejected, 1924 callbacks needed. LTL (current statistics): 95648 atoms, 364288 transitions generated, and 22150 callbacks needed. LTL (fairness): 773 strongly connected components were rejected, 3085 callbacks needed. LTL model checking: memory usage approx. 13829 KiB, 96500 atoms and 381625 transitions generated LTL model checking: total time 190887ms, 22363 callbacks needed 186690ms, netto 467ms. LTL model checking (fairness): 800 strongly connected components were rejected. LTL model checking (fairness): total fairness checking time 3729ms, 3246 callbacks needed 3452ms, netto 277ms. LTL Formula TRUE. No counter example found for SEF => GF [eat.0]. Runtime: 188370 ms
In the above check no fair counter-example could be found for the formula "GF [eat.0]". For this check the search graph comprises 96500 atoms and 381625 transitions, far more than the previous formula check (without fairness assumptions). Since no fair counter-example was found we can infer that the whole state space of the model was explored. Further, since we know from above that 22363 callbacks were needed to explore the search graph, we can infer that the state space of the model has in total 22363 states.
In the output above there is also some information about the fairness checking being performed for the model checker run. Form the fairness statistics we can see that the model checker has refuted 800 SCCs in total, i.e. there were 800 SCCs in the search graph that could serve as a counter-example for "GF [eat.0]" in case no fairness constraints were imposed.
A brief tutorial on visualizing LTL counter-examples in the Rodin tool can be found here.
A tutorial of a simple case study, where setting fairness constraints to some of the LTL properties is required, can be found [[Mutual Exclusion (Fairness)|here]
CTL formulas f can be constructed from:
- atomic propositions:
{ Pred } to check if a B predicate Pred holds in the current state e(op) to check if an operation op is enabled
- propositional logic operators:
not f f or g f & g f => g
- temporal operators:
EX f there is a next state satisfying f EX[Op] f there is a next state via Op satisfying f, e.g. EX[reset]{db={}} AX f all next states satisfy f EF f there exists a path where f holds in the future EG f there exists a path where f holds globally AF f for all paths f holds in the future AG f for all paths f holds globally E f U g there exists a path where f holds until g
Note: a model satisfies a CTL formula iff the formula holds in all initial states.
ProB can make use of symmetries induced by the use of deferred sets in B (and given sets in Z).
ProB will perform a limited form of symmetry reduction for constants which are elements of deferred sets. Take the following example
MACHINE m SETS D CONSTANTS a,b,c,d PROPERTIES a:D & b:D & a/=b & c:D & d:D & card(D)=6 END
Elements of a deferred set D of cardinality n are given a number between 1 and n (the pretty printer of ProB renders those elements as D1,...,Dn respectively). Thus, in the example above we could have 1080 solutions (6*6*6*6 = 1296 solutions, if we ignore the constraint a/=b). Luckily, symmetry reduction will reduce this to 10 possibilities.
In a first phase ProB will detect, for every deferred set D, a maximal set ds of type D which are disjoint. In the example above, such a set ds is {a,b}. These elements will be fixed, in the sense that they will get the numbers 1..k, where k is the size of ds. Thus, a will denote D1, b will denote D2. ProB's pretty printer will actually use a instead of D1, and b instead of D2 (and a and b will actually disappear from the list of constants visible in the state properties view). This reduces the number of possibilities already to 36.
As of version 1.5, ProB will also further restrict the possible numbers of the remaining constants. It is an adapted technique described in Section 6 of the article "New Techniques that Improve MACE-style Finite Model Finding" (PDF). Basically, the technique ensures that c will not use the index 4 and that d will use the index 4 only if the index 3 was used by c. Thus only the 10 following possibilities are generated by ProB:
a b c d -------------------------- a b a a a b a b a b D3 D4 a b a D3 a b b a a b b b a b b D3 a b D3 a a b D3 b a b D3 D3
As of version 1.8, ProB will furthermore detect partition constraints for the deferred sets. This symmetry reduction is applied to the free, unconstrained deferred set elements. For the example above, these would be all elements with index 5 or higher (D5, D6, ...). For the example above, if we have a constraint
D = A \/ B & A /\ B = {}
the free deferred set elements D5,D6,... will be allocated in order to A and B. In other words, we can have D5 in A and D6 in B, but not D6 in A and D5 in B.
In the machine below all deferred set elements are free:
MACHINE m SETS D CONSTANTS A,B PROPERTIES D = A \/ B & A /\ B = {} & card(D)=6 & card(A) = 3 END
Hence, here ProB 1.8 will only generate one possible setup of the constants:
A = {D1,D2,D3} B = {D4,D5,D6}
In addition to the above, you can also turn of stronger symmetry reduction for model checking.
Warning: turning on symmetry reduction will also influence the way that animation works. In other words, when executing an operation, the animator may transfer you to an equivalent symmetric state (rather than to the one you may have expected).
In the "Symmetry" menu of the "Preferences" menu you can choose the following:
LTSmin is a high-performance language-independent model checker that allows numerous modelling language front-ends to be connected to various analysis algorithms, through a common interface.
We have implemented an integration of LTSmin with ProB for symbolic reachability and for explicit state model checking:
In order to set up the LTSmin and ProB integration, do the following:
Note that the LTSmin extension is not available for Windows.
Note that on Linux, you might prefix the commands with LD_LIBRARY_PATH=lib/
probcli Flag | Example | Description |
---|---|---|
-ltsmin | probcli -ltsmin FILE | Start the ProB server for LTSmin at the default endpoint /tmp/ltsmin.probz - it will use the machine FILE in order to provide information to LTSmin |
-ltsmin2 | probcli -ltsmin2 endpoint.probz FILE | Start the ProB server for LTSmin at the endpoint given by the specific endpoint.probz file. It will use the machine FILE in order to provide information to LTSmin |
-mc-with-lts-seq | probcli -nodead -mc-with-lts-seq FILE | Start invariant model checking with the sequential backend of LTSmin on FILE. Note that at least one of -nodead or -noinv must be provided. |
-mc-with-lts-sym | probcli -nodead -mc-with-lts-sym FILE | Start invariant model checking with the symbolic backend of LTSmin on FILE. Note that at least one of -nodead or -noinv must be provided. |
-p LTSMIN | -p LTSMIN /opt/ltsmin/ | Use the LTSmin commands in the provided directory (here /opt/ltsmin) |
An example run:
$ probcli scheduler.mch -mc_with_lts_seq -noinv -p LTSMIN ~/bin/ltsmin_v3.0.2/bin starting prob2lts-sym/seq (flags nodead=false, noinv=true, moreflags=[]) prob2lts-seq, 0.001: ProB module initialized prob2lts-seq, 0.001: Loading model from /tmp/ltsmin.probz prob2lts-seq, 0.001: ProB init prob2lts-seq, 0.002: connecting to zocket ipc:///private/tmp/ltsmin.probz pl_init_for_lts_min vars([active,ready,waiting]) prob2lts-seq, 0.026: There are 7 state labels and 1 edge labels prob2lts-seq, 0.026: State length is 4, there are 6 groups prob2lts-seq, 0.026: Running dfs search strategy prob2lts-seq, 0.026: Using a tree for state storage prob2lts-seq, 0.147: state space 30 levels, 36 states 156 transitions prob2lts-seq, 0.147: Deadlocks: >= 0 prob2lts-seq, 0.147: terminating ProB connection get-next-state: 121 get-next-state (short): 0 get-next-action: 0 get-next-action (short): 0 get-state-label: 0 get-state-label (short): 0 get-label-group: 0 prob2lts-seq, 0.147: disconnecting from zocket ipc:///private/tmp/ltsmin.probz /prob2lts-seq with [--trace,/tmp/prob-ltsmin-trace.gcf,-c,-d] exited with status: exit(0) LTSMin found no counter example
Here a run that finds a counter example:
probcli public_examples/B/Demo/CarlaTravelAgencyErr.mch -mc_with_lts_seq -nodead -p LTSMIN ~/bin/ltsmin_v3.0.2/bin % unused_constants(1,[AGENCY_USER]) prob2lts-seq, 0.000: ProB module initialized prob2lts-seq, 0.000: Loading model from /tmp/ltsmin.probz prob2lts-seq, 0.000: ProB init prob2lts-seq, 0.000: connecting to zocket ipc:///private/tmp/ltsmin.probz starting prob2lts-sym/seq (flags nodead=true, noinv=false, moreflags=[]) Merging last 9 of 16 invariants (LTSMin POR supports max 8 invariants) pl_init_for_lts_min vars([session,session_response,session_card,session_state,session_request,user_hotel_bookings,user_rental_bookings,rooms_hotel,cars_rental,global_room_bookings,global_car_bookings,AGENCY_USER]) prob2lts-seq, 0.024: "!is_init || (inv16 && inv15 && inv14 && inv13 && inv12 && inv11 && inv10 && inv9 && inv8 && inv7 && inv6 && inv5 && inv4 && inv3 && inv2 && inv1)" is not a file, parsing as formula... prob2lts-seq, 0.024: There are 18 state labels and 1 edge labels prob2lts-seq, 0.024: State length is 13, there are 11 groups prob2lts-seq, 0.024: Running dfs search strategy prob2lts-seq, 0.024: Using a tree for state storage % Runtime for SOLUTION for SETUP_CONSTANTS: 42 ms (walltime: 44 ms) % Runtime for SOLUTION for SETUP_CONSTANTS: 2 ms (walltime: 2 ms) % Runtime for SOLUTION for SETUP_CONSTANTS: 0 ms (walltime: 0 ms) % Runtime to FINALISE SETUP_CONSTANTS: 0 ms (walltime: 0 ms) prob2lts-seq, 0.258: prob2lts-seq, 0.258: Invariant violation (!is_init || (inv16 && inv15 && inv14 && inv13 && inv12 && inv11 && inv10 && inv9 && inv8 && inv7 && inv6 && inv5 && inv4 && inv3 && inv2 && inv1)) found at depth 38! prob2lts-seq, 0.258: prob2lts-seq, 0.258: Writing trace to /tmp/prob-ltsmin-trace.gcf prob2lts-seq, 0.264: terminating ProB connection get-next-state: 306 get-next-state (short): 0 get-next-action: 0 get-next-action (short): 0 get-state-label: 184 get-state-label (short): 0 get-label-group: 0 prob2lts-seq, 0.265: disconnecting from zocket ipc:///private/tmp/ltsmin.probz prob2lts-seq, 0.266: exiting now ltsmin-printtrace: Writing output to '/tmp/prob-ltsmin-trace.csv' ltsmin-printtrace: realloc ltsmin-printtrace: action labeled, detecting silent step ltsmin-printtrace: no silent label ltsmin-printtrace: length of trace is 37 writing trace to /tmp/prob-ltsmin-trace.csv /prob2lts-seq with [--trace,/tmp/prob-ltsmin-trace.gcf,-c,--invariant=!is_init || (inv16 && inv15 && inv14 && inv13 && inv12 && inv11 && inv10 && inv9 && inv8 && inv7 && inv6 && inv5 && inv4 && inv3 && inv2 && inv1)] exited with status: exit(1) ! An error occurred (source: ltsmin_counter_example_found) ! ! LTSMin found a counter example, written to: /tmp/prob-ltsmin-trace.csv *** TRACE: (37) $init_state login unbookCar enterCard logout login unbookCar enterCard logout login unbookCar enterCard response login logout unbookCar enterCard response login again unbookCar enterCard retryCard response unbookCar again enterCard retryCard response unbookCar enterCard logout login logout unbookCar enterCard response ! *** error occurred *** ! ltsmin_counter_example_found ! Total Errors: 1, Warnings:0
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.
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.
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:
The following command is related to the above:
As of version 1.5, ProB provides support for constraint-based bounded model checking (BMC). As opposed to constraint-based checking, BMC finds counterexamples which are reachable from the INITIALISATION. As opposed to ordinary model checking, it does not compute all possible solutions for parameters and constants, but constructs these on demand. This can be useful when the out-degree of the state-space is very high, i.e., when there are many possible solutions for the constants, the initialisation and/or the individual operations and their parameters.
Take the following example:
MACHINE VerySimpleCounterWrong CONSTANTS lim PROPERTIES lim = 2**25 VARIABLES ct INVARIANT ct:INTEGER & ct < lim INITIALISATION ct::0..(lim-1) OPERATIONS Inc(i) = PRE i:1..1000 & ct + i <= lim THEN ct := ct+i END; Reset = PRE ct = lim THEN ct := 0 END END
The ProB model checker will here run for a very long time before uncovering the error that occurs when ct is set to lim. If you run the TLC backend you will get the error message "Too many possible next states for the last state in the trace."
However, for the bounded model checker this is less of a problem; it will use the constraint solver to try and find suitable values of the constants, initial variable values and parameters to generate an invariant violation. The bounded model checker actually uses the same algorithm than the constraint-based test-case generator, but uses the negation of the invariant as target. You can use the command-line version of ProB, with the -bmc DEPTH command as follows:
$ probcli VerySimpleCounterWrong -bmc 10 constraint based test case generation, maximum search depth: 10 constraint based test case generation, target state predicate: #not_invariant constraint based test case generation, output file: constraint based test case generation, performing bounded model checking bounded_model_checking CBC test search: starting length 1 *1.!# CBC test search: covered event Inc Found counter example executing_stored_test_case(1,[Inc],[(2,Inc(int(1)),1,2)]) finding_trace_from_to(root) BMC counterexample found, Length=1 CBC Algorithm finished (1) Timeouts: total: 0 Checked paths (Depth:Paths): 1:1, total: 1 Found paths: 1:1, total: 1 Found test cases: 1:1, total: 1 Runtime (wall): 120 ms ! An error occurred ! ! source(invariant_violation) ! Invariant violation found by bmc ! *** error occurred *** ! invariant_violation
You can also use the bounded model checker from ProB Tcl/Tk. The command is situated inside the Experimental sub-menu of the Analyse menu (to see the command, you may have to change the preference entry to preference(user_is_an_expert_with_accessto_source_distribution,true). in the ProB_Preferences.pl file) Running the command on the above example will generate the following counter-example:
The current nightly builds of ProB support different symbolic model checking algorithms:
As opposed to constraint-based checking, these algorithms find counterexamples which are reachable from the INITIALISATION. As opposed to ordinary model checking, they do not build up the state space explicitly, e.g., they do not compute all possible solutions for parameters and constants. This can be useful when the out-degree of the state-space is very high, i.e., when there are many possible solutions for the constants, the initialisation and/or the individual operations and their parameters.
In addition to the algorithms explained here, BMC*, a bounded model checking algorithm based on a different technique is available in Prob. See its wiki page for details.
Take the following example:
MACHINE VerySimpleCounterWrong CONSTANTS lim PROPERTIES lim = 2**25 VARIABLES ct INVARIANT ct:INTEGER & ct < lim INITIALISATION ct::0..(lim-1) OPERATIONS Inc(i) = PRE i:1..1000 & ct + i <= lim THEN ct := ct+i END; Reset = PRE ct = lim THEN ct := 0 END END
The ProB model checker will here run for a very long time before uncovering the error that occurs when ct is set to lim. If you run the TLC backend you will get the error message "Too many possible next states for the last state in the trace."
However, for the symbolic model checking techniques this is less of a problem. You can use them via command-line version of ProB as follows:
$ probcli VerySimpleCounterWrong.mch -symbolic_model_check bmc K = 0 solve/2: result of prob: contradiction_found K = 1 solve/2: result of prob: contradiction_found K = 2 solve/2: result of prob: contradiction_found K = 3 solve/2: result of prob: contradiction_found K = 4 solve/2: result of prob: solution successor_found(0) --> INITIALISATION(0) successor_found(1) --> Inc successor_found(2) --> Inc successor_found(3) --> Inc successor_found(4) --> Inc ! *** error occurred *** ! invariant_violation
Instead of "bmc" you can use "kinduction" and "ic3" as command line arguments in order to use the other algorithms.
The algorithms are also available from within ProB Tcl/Tk. They can be found inside the "Symbolic Model Checking" sub-menu of the "Analyse" menu.
A paper describing the symbolic model checking algorithms and how they are applied to B and Event-B machines has been submitted to ABZ 2016.
Warning This page has not yet been reviewed. Parts of it may no longer be up to date |
ProB can be used for refinement checking of B, Z and CSP specifications. Below we first discuss refinement checking for B machines. There is a tutorial on checking CSP assertions in ProB which can be viewed here.
ProB checks trace refinement. In other words, it checks whether every trace (consisting of executed operations with their parameter values and return values) of a refinement machine can also be performed by the abstract specification.
Hence, ProB does *not* check the gluing invariant. Also, PRE-conditions are treated as SELECT and PRE-conditions of the abstract machine are *not* always propagated down to the refinement machine. Hence, refinement checking has to be used with care for classical B machines, but it is well suited for EventB-style machines.