Sebastian Krings: Created page with "= Overview = The current nightly builds of ProB support different symbolic model checking algorithms: * Bounded Model Checking (BMC), * k-Induction, and * different Variant..."

2016-01-22T15:53:45Z

Created page with "= Overview = The current nightly builds of ProB support different symbolic model checking algorithms: * Bounded Model Checking (BMC), * k-Induction, and * different Variant..."

New page

= Overview =

The current nightly builds of ProB support different symbolic model checking algorithms:

* Bounded Model Checking (BMC),
* k-Induction, and
* different Variants of the IC3 algorithm.

As opposed to [[Constraint_Based_Checking|constraint-based checking]], these algorithms find counterexamples which are reachable from the INITIALISATION. As opposed to [[Consistency_Checking |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 [[Bounded Model Checking|its wiki page]] for details.

= Usage =

Take the following example:

<pre>
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
</pre>

The ProB model checker will here run for a very long time before uncovering the error that occurs when <tt>ct</tt> is set to lim. If you run the [[TLC|TLC backend]] you will get the error message "<tt>Too many possible next states for the last state in the trace.</tt>"

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:

<pre>
$ 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
</pre>

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.

= More details =

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.

Symbolic Model Checking - Revision history

Sebastian Krings: Created page with "= Overview = The current nightly builds of ProB support different symbolic model checking algorithms: * Bounded Model Checking (BMC), * k-Induction, and * different Variant..."