Bounded Model Checking

Revision as of 15:59, 25 June 2015 by Michael Leuschel (talk | contribs)
(diff) ← Older revision | Latest revision (diff) | Newer revision → (diff)

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
PROPERTIES lim = 2**25
 ct:INTEGER & ct < lim
INITIALISATION ct::0..(lim-1)
  Inc(i) = PRE i:1..1000 & ct + i <= lim THEN ct := ct+i END;
  Reset = PRE ct = lim THEN ct := 0 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

CBC test search: starting length 1
CBC test search: covered event Inc
Found counter example

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 file) Running the command on the above example will generate the following counter-example:

BMC Counter Wrong.png