In this chapter we give a short introduction to the use of Bounded Model
Checking (BMC) in NuSMV2. The aim is to get the user start using the BMC
functionality of NuSMV2 in a fast and easy way. The tutorial is based
on a simple example that can be found in the file bmc_tutorial.smv, in
the distribution package.
No background on BMC is assumed. For a more in-depth
introduction to the theory underlying BMC please refer to [BCCZ99].
Consider the following model, representing a simple, deterministic counter modulo 8:
MODULE main
VAR
y : 0..15;
ASSIGN
init(y) := 0;
TRANS
case
y = 7 : next(y) = 0;
1 : next(y) = ((y + 1) mod 16);
esac
This slightly artificial model has only the state variable 'y', ranging from 0 to 15. The values of 'y' are limited by the transition relation to the [0, 7] interval. The counter starts from 0, deterministically increments by one the value of 'y' at each transition up to 7, and then restarts from zero.
We would like to check with BMC the LTL specification 'G ( y=4 -> X y=6 )'
expressing that "each time the counter value is 4, the next counter
value will be 6". This specification is obviously false, and our first
step is to use NuSMV2 BMC to demonstrate its falsity.
So let's start NuSMV2: open a shell, make your current directory
where the tutorial file bmc_tutorial.smv is located, make sure that the
NuSMV executable file can be found by the underling system, and finally
launch it:
system_prompt> NuSMV -int bmc_tutorial.smv *** This is NuSMV <version> (compiled ...) *** For more information of NuSMV see <http://nusmv.irst.itc.it> *** or email to <nusmv-users@irst.itc.it>. *** Please report bugs to <nusmv-users@irst.itc.it>. NuSMV >
Now setup the BMC module in NuSMV2, using the command
'go_bmc':
NuSMV > go_bmc NuSMV >
NuSMV2 has silently setup its BMC module and you can now work
with it. It is time to try to check the false property 'G ( y=4 -> X
y=6 )'. You can use the command 'check_ltlspec_bmc' specifying the
property you are interested in checking through the option '-p':
NuSMV > check_ltlspec_bmc -p "G ( y=4 -> X y=6 )" -- no counterexample found with bound 0 for specification G(y = 4 -> X y = 6) -- no counterexample found with bound 1 for ... -- no counterexample found with bound 2 for ... -- no counterexample found with bound 3 for ... -- no counterexample found with bound 4 for ... -- specification G (y = 4 -> X y = 6) is false -- as demonstrated by the following execution sequence State 1.1: y = 0 State 1.2: y = 1 State 1.3: y = 2 State 1.4: y = 3 State 1.5: y = 4 State 1.6: y = 5 NuSMV >
NuSMV2 has found that the specification is false, and is showing us a
counterexample, i.e. a trace where the value of y becomes 4 (at time
4) and at the next step is not 6.
length: 0 1 2 3 4 5
o--->o--->o--->o--->o--->o
state: y=0 y=1 y=2 y=3 y=4 y=5
If you look at the NuSMV2 output on the command
'check_ltlspec_bmc', you can see that, before finding the counterexample
of length 5, NuSMV2 also tried to construct counterexamples of
lower length (i.e. with bound from 0 to 4). However, there are no such
counterexamples. For instance, in the case of bound 4, the traces of the
model have the following form:
length: 0 1 2 3 4
o--->o--->o--->o--->o
state: y=0 y=1 y=2 y=3 y=4
In this situation, y gets the value 4, but it is impossible for
NuSMV2 to say anything about the following state.
In general, the 'check_ltlspec_bmc' command tries to find a
counterexample of increasing length, and immediately stops the iteration
when it succeeds, declaring the formula is false. You can control the
maximum number of iterations of 'check_ltlspec_bmc' by specifying a
value for the bmc_length environment variable. You can see and set the
values of environment variables using the 'set' command. Try what follows:
NuSMV > set The user variables are: ... bmc_length "10" ... NuSMV >
The default value for the variable bmc_length is '10'. In this way
the check_ltlspec_bmc command iterates length from 0 to 10 and then
exits even if no counterexample has been previously found. For
instance, if we set a smaller value NuSMV2 cannot prove
the falsity of the formula:
NuSMV > set bmc_length 4 NuSMV > set The user variables are: ... bmc_length "4" ... NuSMV >
NuSMV > check_ltlspec_bmc -p "G ( y=4 -> X y=6 )" -- no counterexample found with bound 0 for ... -- no counterexample found with bound 1 for ... -- no counterexample found with bound 2 for ... -- no counterexample found with bound 3 for ... -- no counterexample found with bound 4 for ... NuSMV >
It is possible to check a specification based on a single bound, without
iterating from 0 to bmc_length, by using the command
'check_ltlspec_bmc_onepb' as follows:
NuSMV > set bmc_length 5 NuSMV > check_ltlspec_bmc_onepb -p "G ( y=4 -> X y=6 )" -- specification G (y = 4 -> X y = 6) is false -- as demonstrated by the following execution sequence State 4.1: y = 0 State 4.2: y = 1 State 4.3: y = 2 State 4.4: y = 3 State 4.5: y = 4 State 4.6: y = 5 NuSMV >
Let us consider now another property, '!G F (y = 2)', stating that y gets the value 2 only a finite number of times. Again, this is a false property due to the cyclic nature of the model:
NuSMV > set bmc_length 10 NuSMV > check_ltlspec_bmc -p "!G F y = 2" -- no counterexample found with bound 0 for ... -- no counterexample found with bound 1 for ... -- no counterexample found with bound 2 for ... -- no counterexample found with bound 3 for ... -- no counterexample found with bound 4 for ... -- no counterexample found with bound 5 for ... -- no counterexample found with bound 6 for ... -- specification ! G F y = 2 is false -- as demonstrated by the following execution sequence State 2.1: y = 0 State 2.2: y = 1 State 2.3: y = 2 State 2.4: y = 3 State 2.5: y = 4 State 2.6: y = 5 State 2.7: y = 6 State 2.8: y = 7 NuSMV >
In this example NuSMV2 had been increasing problem length until
it found a loop around [0..7] which contains the y value 2, that shows
that the property cannot be true.
In general, BMC can find two kinds of counterexamples, depending on the
property being analyzed. For safety properties (e.g. like the first one
used in this tutorial), a counterexample is a finite sequence of
transitions through different states. For liveness properties,
counterexamples are infinite but periodic sequences, and can be
represented in a bounded setting as a finite prefix followed by a loop,
i.e. a finite sequence of states ending with a loop back to some
previous state. So a counterexample which demonstrates the falsity of a
liveness property as "!G F p" cannot be a finite sequence of
transitions. It must contain a loop which makes the infinite sequence of
transitions as well as we expected.
---------------------
| |
| |
V |
o--->o--->o--->o-...->o--->o--->o--->o--->
time: 0 1 2 3 k-2 k-1 k k+1 ...
l
Consider the above figure. It represents an examples of a generic
infinite counterexample, with its two parts: the prefix part (times from
0 to l-1), and the loop part (indefinitely from l to k). Because the
loop always jumps to a previous time it is called 'loopback'. Please
also note that because of the bound, state k+1 is forced to be equal to
state 2. You can control these two parts parameters (k and l) by setting
the environment variables bmc_length and bmc_loopback as
we are going to show now.
NuSMV > set bmc_length 7 NuSMV > set bmc_loopback 0 NuSMV > check_ltlspec_bmc_onepb -p "!G F (y =2)" -- specification ! G F y = 2 is false -- as demonstrated by the following execution sequence State 5.1: y = 0 State 5.2: y = 1 ... State 5.7: y = 6 State 5.8: y = 7 NuSMV >
----------------------------------
| |
| |
V |
o--->o--->o--->o--->o--->o--->o--->o
length: 0 1 2 3 4 5 6 7
y value: 0 1 2 3 4 5 6 7
As you can see by properly setting k and l NuSMV2 is able to
find a counterexample for a false liveness property.
Try now to change values of k and l:
NuSMV > set bmc_length 9 NuSMV > check_ltlspec_bmc_onepb -p "!G F (y =2)" -- no counterexample found with bound 9 and loop at 0 for specification ! G F y = 2 NuSMV > set bmc_length 7 NuSMV > set bmc_loopback 1 NuSMV > check_ltlspec_bmc_onepb -p "!G F (y =2)" -- no counterexample found with bound 7 and loop at 1 for specification ! G F y = 2 NuSMV >
In these two examples NuSMV2 did not find a counterexample. Look
at the following figures to understand this behaviour.
Case k = 9, l = 0:
--------------------------------------------
| |
| |
V |
o--->o--->o--->o--->o--->o--->o--->o--->o--->o
length: 0 1 2 3 4 5 6 7 8 9
y value: 0 1 2 3 4 5 6 7 0 1
Case k = 7, l = 1:
-----------------------------
| |
| |
V |
o--->o--->o--->o--->o--->o--->o--->o
length: 0 1 2 3 4 5 6 7
y value: 0 1 2 3 4 5 6 7
Cases (k=9, l=0) and (k=7, l=1) are counterexample structures which do
not match with the model of the counter, so it is not possible for
NuSMV2 to find a valid counterexample if its parameters are not
properly set.
In this specific case all couples of (k, l) which actually produce a
counterexamples have a loop length of 7.
In NuSMV2 it is possible to specify the loop in four
different ways by using always the bmc_loopback environment variable:
bmc_loopback environment variable.
bmc_loopback. The negative number is the
loop length, and you can also imagine it as a precise time-point loop
relative to the path bound.
bmc_loopback variable. In this case
NuSMV2 will not find infinite counterexamples.
bmc_loopback variable. In this case
NuSMV2 will search counterexamples for paths with any possible
loopbacks in the path bounds. A counterexample with no loop will be also
searched. This is the default value assigned to the bmc_loopback
variable when NuSMV2 starts its execution.
We show now that by setting the loop length to 7 NuSMV2 is able
to find a valid counterexample with any value of bmc_length:
NuSMV > set bmc_loopback -7 NuSMV > set bmc_length 12 NuSMV > check_ltlspec_bmc_onepb -p "!G F y = 2" -- specification ! G F y = 2 is false -- as demonstrated by the following execution sequence State 1.1: y = 0 State 1.2: y = 1 State 1.3: y = 2 State 1.4: y = 3 State 1.5: y = 4 State 1.6: y = 5 State 1.7: y = 6 State 1.8: y = 7 State 1.9: y = 0 State 1.10: y = 1 State 1.11: y = 2 State 1.12: y = 3 State 1.13: y = 4 NuSMV >
This picture illustrates the produced counterexample in a more effective way:
----------------------------------
| |
| |
V |
o--->o--->o--->o--->o--->o--->o--->o--->o--->o--->o--->o--->o
length: 0 1 2 3 4 5 6 7 8 9 10 11 12
y value: 0 1 2 3 4 5 6 7 0 1 2 3 4
If we had specified a greater value for bmc_length we would have
obtained again a valid counterexample whose loop would have been shifted
farther to the right in the figure.
If no loopback is specified, NuSMV2 is not able to
find a counterexample for the given liveness property:
NuSMV > set bmc_length 12 NuSMV > set bmc_loopback X NuSMV > check_ltlspec_bmc -p "!G F y = 2" -- no counterexample found with bound 0 and no loop for ... -- no counterexample found with bound 1 and no loop for ... -- no counterexample found with bound 2 and no loop for ... -- no counterexample found with bound 3 and no loop for ... -- no counterexample found with bound 4 and no loop for ... -- no counterexample found with bound 5 and no loop for ... -- no counterexample found with bound 6 and no loop for ... -- no counterexample found with bound 7 and no loop for ... -- no counterexample found with bound 8 and no loop for ... -- no counterexample found with bound 9 and no loop for ... -- no counterexample found with bound 10 and no loop for ... -- no counterexample found with bound 11 and no loop for ... -- no counterexample found with bound 12 and no loop for ... NuSMV >
Please note that in this example we used command 'check_ltlspec_bmc'
instead of command 'check_ltlspec_bmc_onepb' because we wanted make
NuSMV2 iterating length from 0 to 12, trying to find a
counterexample for several problem lengths.
Now let us start checking for a new kind of properties: invariants. An invariant is a propositional property which must always hold. BMC tries to prove the truth of invariants via an inductive reasoning, by checking if (i) the property holds in every initial state, and (ii) if it holds in any state reachable from any state where it holds.
To check invariants with BMC you can use the check_invar_bmc command.
Consider for example the formula 'y in (0..12)': we want to prove it is
an invariant property by using NuSMV2 BMC:
NuSMV > check_invar_bmc -p "y in (0..12)" -- cannot prove the invariant y in (0 .. 12) : the induction fails -- as demonstrated by the following execution sequence State 1.1: y = 12 State 1.2: y = 13 NuSMV >
NuSMV2 answered the given invariant cannot be proved, and it showed a
state satisfying "y in (0..12)" having a successor state not satisfying
"y in (0..12)". This two-steps sequence of assignments shows why the
induction fails. Note that NuSMV2 did not say the given formula
is really false, because the induction step can establish only if a
given formula is actually true, but cannot be sure if a formula it found
out to be false is really logically false. BMC-based invariants checking
is not always able to provide a precise answer as demonstrated by this
case.
Then we try to prove a stronger invariant, saying that 'y in (0..7)':
NuSMV > check_invar_bmc -p "y in (0..7)" -- invariant y in (0 .. 7) is true NuSMV >
In this case NuSMV2 is able to rove that "y in (0..7)" is
true. Indeed, sometimes it is easier to prove a stronger invariant.
Now we check a false invariant:
NuSMV > check_invar_bmc -p "y in (0..6)" -- cannot prove the invariant y in (0 .. 6) : the induction fails -- as demonstrated by the following execution sequence State 1.1: y = 6 State 1.2: y = 7 NuSMV >
As for property "y in (0..12)" NuSMV2 returns a two steps
sequence showing that the induction fails. The main difference is that
in the former case the state 'y=12' is NOT reachable, while in the
latter case the state 'y=6' can be reached.
The BMC-based invariant checker does not take into account reachability.
To resolve ambiguous cases you can use the BDD-based invariant checker,
which is based on reachability, to obtain a more satisfying result:
NuSMV > go NuSMV > check_invar -p "y in (0..12)" -- invariant y in (0 .. 12) is true NuSMV > check_invar -p "y in (0..6)" -- invariant y in (0 .. 6) is false -- as demonstrated by the following execution sequence State 2.1: y = 0 State 2.2: y = 1 State 2.3: y = 2 State 2.4: y = 3 State 2.5: y = 4 State 2.6: y = 5 State 2.7: y = 6 State 2.8: y = 7 NuSMV >
Sometimes however SAT-based model checking can tackle models that are out of reach for BDD-based approaches.
In this tutorial we have been using essentially three BMC commands (check_ltlspec_bmc, check_ltlspec_bmc_onepb and check_invar_bmc) and ignored several others. In general, all the commands can handle a large number of options which have not been discussed in this tutorial. Please refer to the detailed command descriptions for further information.
Each of the described commands is based on the reduction of the bounded
model checking problem to a propositional satisfiability problem. After
the problem is generated, NuSMV2 internally calls the SIM
propositional solver
in order to find an assignment which validates the problem. It is
also possible to generate the problem without calling to SIM
solver. Each generated problem is dumped in DIMACS format into a
file. DIMACS is the standard format used as input by most external SAT
solver, so it is possible to use NuSMV2 to generate problem only,
and then invoke an external SAT solver separately.
The commands which generate DIMACS problem are: gen_ltlspec_bmc,
gen_ltlspec_bmc_onepb and gen_invar_bmc. The default DIMACS filename is
held by the bmc_dimacs_filename and bmc_invar_dimacs_filename
variables. DIMACS filenames can contain some particular symbols which can be
automatically expanded by NuSMV2. Please refer to the detailed
commands descriptions for further information about pattern expansion.
It is also possible to specify the filename via the
command line of the command being invoked. You can also use the
commands check_ltlspec_bmc, check_ltlspec_bmc_onepb and check_invar_bmc
to dump DIMACS problem and then check via the '-o' option. If this
option is not activated, problem dumping will not be performed.
10.
The default value is *.
The default value is "@f_k@k_l@l_n@n.dimacs".
The default value is "@f_invar_n@n.dimacs".
check_ltlspec_bmc [-h | -n idx | -p "formula" [IN context]] [-k max_length] [-l loopback] [-o filename]
This command generates one or more problems, and calls
SAT solver for each one. Each problem is related to a specific problem
length, which increases from zero (0) to the given maximum problem
length. Here "length" is the length of the problem that system
is going to generate and/or solve.
In this context the maximum problem length is represented by the
-k command parameter, or by its default value stored in the
environment variable bmc_length.
The single generated problem also depends on the "loopback"
parameter you can explicitly specify by the -l option, or by its
default value stored in the environment variable bmc_loopback.
The property to be checked may be specified using the -n idx or
the -p "formula" options.
If you need to generate a dimacs dump file of all generated problems, you
must use the option -o "filename".
Command options:
-n index
-p "formula" [IN context]
formula specified on the command-line. context is the module instance name which the variables
in formula must be evaluated in.
-k max_length
-l loopback
-o filename
check_ltlspec_bmc_onepb [-h | -n idx | -p "formula" [IN context]] [-k length] [-l loopback] [-o filename]
As command check_ltlspec_bmc but it produces only one
single problem with fixed length and loopback values, with no iteration
of the problem length from zero to max_length.
Command options:
-n index
-p "formula [IN context]"
formula specified on the command-line. context is the module instance name which the variables
in formula must be evaluated in.
-k length
-l loopback
-o filename
DIMACS files generation, BMC commands for checking of LTL specifications, Getting started with BMC
check_invar_bmc [-h | -n idx | -p "formula" [IN context]] [-o filename]
Command options:
-n index
-p "formula [IN context]"
formula specified on the command-line. context is the module instance name which the variables
in formula must be evaluated in.
-o filename
gen_ltlspec_bmc [-h | -n idx | -p "formula" [IN context]] [-k max_length] [-l loopback] [-o filename]
This command generates one or more problems, and
dumps each problem into a dimacs file. Each problem is related to a specific
problem length, which increases from zero (0) to the given maximum problem
length. In this short description "length" is the length of the
problem that system is going to dump out.
In this context the maximum problem length is represented by the
max_length parameter, or by its default value stored in the
environment variable bmc_length.
Each dumped problem also depends on the loopback you can explicitly
specify by the -l option, or by its default value stored in the
environment variable bmc_loopback.
The property to be checked may be specified using the -n idx or
the -p "formula" options.
You may specify dimacs file name by using the option -o "filename",
otherwise the default value stored in the environment variable
bmc_dimacs_filename will be considered.
Command options:
-n index
-p "formula [IN context]"
formula specified on the command-line. context is the module instance name which the variables
in formula must be evaluated in.
-k max_length
-l loopback
-o filename
gen_ltlspec_bmc_onepb [-h | -n idx | -p "formula" [IN context]] [-k length] [-l loopback] [-o filename]
As the gen_ltlspec_bmc command, but it generates
and dumps only one problem given its length and loopback.
Command options:
-n index
-p "formula [IN context]"
formula specified on the command-line. context is the module instance name which the variables
in formula must be evaluated in.
-k length
-l loopback
-o filename
gen_invar_bmc [-h | -n idx | -p "formula" [IN context]] [-o filename]
Command options:
-n index
-p "formula" [IN context]
formula specified on the command-line. context is the module instance name which the variables
in formula must be evaluated in.
-o filename
bmc_simulate [-h]
bmc_simulate does not require a specification to build the problem, because only the model is used to build it.
Go to the first, previous, next, last section, table of contents.