SMV and nuXmV Quickstart
IA169: Model Checking
Martin Jon´aˇs
Faculty of Informatics, Masaryk University
SMV
SMV
• a language for describing transition systems
• we use its extension that is used in a model checker nuXmv
1
Variables
Variable definitons
1 VAR
2 name1 : boolean;
3 name2 : {ready , waiting , stopped };
4 name3 : 1..8;
Possible types
• boolean (values TRUE and FALSE)
• enumerative: e.g., { ready, waiting, stopped }
• bounded interval: e.g, 1..8
• C integers: integer
• real numbers: real
• bit-vectors: unsigned word[8] or signed word[16] or . . .
And more.
2
Operations
Boolean
• &, |, xor, ->, <-> (all infix)
• ! (prefix)
Arithmetic
• +, -, *, /, mod (all infix)
Comparisons
• =, !=, <, >, <=, >= (all infix)
And more.
3
Initial values and successor values
1 ASSIGN
2 init(var1) := TRUE;
3 next(var1) := !var1;
4 init(var2) := 0;
5 next(var2) := var2 + var3;
6 init(var3) := {ready , wating };
For each variable, specify its initial value and its new value based on the current values of the
variables. Can specify a set of variables: nondeterminism.
If an initial value or the next value are not specified, they can be arbitrary (are unconstrained).
4
Initial and successor conditions
Alternatively
1 INIT
2 var1 <-> TRUE;
3 INIT
4 var2 >= 10;
5 INIT
6 var3 != waiting;
7
8 TRANS
9 var1 = !next(var1);
10 TRANS
11 next(var4) >= var4 + var5;
Specify a set of formulas that has to hold in the initial states.
Specify a set of formulas that have to hold for transition (use var and next(var)).
5
Case expression
1 ASSIGN
2 next(var1) :=
3 case
4 var2 = waiting : 10;
5 var2 = ready : 12;
6 TRUE : 42;
7 esac;
Returns a body of the first condition that is true.
Can contain more complex formulas:
1 ASSIGN
2 next(var1) :=
3 case
4 var2 = waiting & request & var3 > 12 : !var1;
5 TRUE : var1;
6 esac;
6
Fairness constrains
1 FAIRNESS (state = ready);
Restricts the runs to those where the formula state = ready holds infinitely often.
Equivalent to
1 JUSTICE (state = ready);
7
nuXmv
nuXmv
• a symbolic model checker for transition systems
• supports reachability, ltl, and ctl properties
• also supports infinite-state systems (will not be needed in this course)
• free only for non-commercial and academic usage
8
Running nuXmv
• ./nuXmv -it for interactive usage
• ./nuXmv -source filename.cmd for batch usage
9
Useful commands
• read model model.smv to read a smv model from a given file
• go to set up all internal data structures
• pick state -v -r picks a random (-r) initial state and prints it (-v)
• simulate -v -r -k 10 runs 10 steps (-k) of a simulation from the picked state, prints
all the states (-v), chooses the successors randomly (-r)
• reset resets everything (if you want to use a new model)
• check ltlspec -p "ltl formula" checks whether the given ltl formula holds in the
model
• check invar -p "property" checks whether the given property holds in all reachable
states of the model
• help lists all commands
• help [command] shows help for the given command
• exit
10