4 Model Checking and NuSMV

A model checker is defined as follows: given a desired property, expressed as temporal logic formula $\varphi$ , and a Kripke model M, decide if M, s $\vDash$ $\varphi$ , that is, if $\varphi$ is satisfied by M from a given state s. If it is, the model checker will simply output “yes”, otherwise the tool will print a counterexample in which the property is violated.

To see if a property is satisfied, the model checker examines a part of the model with a number k of interactions, starting from 0. It tries to find counter-examples for that piece of the Kripke structure and, if it doesn’t, it increases the k, otherwise the execution stops and the counterexample is shown.

NuSMV is short for New Symbolic Model Verifier and it’s a symbolic model checker that supports the analysis of specifications expressed in CTL and LTL. The aim of NuSMV is to have a robust, customizable and open-source model checker.

Following, an example of NuSMV program:

MODULE main
    VAR
        request : boolean;
        state : {ready, busy};
    ASSIGN
        init(state) := ready;
        next(state) :=
            case 
                state = ready & request : busy;
                TRUE : {ready, busy};
            esac;

VAR contains the variables declaration. Variables can be boolean, enum, bounded integers and finite arrays.
init(state) defines the initial value of a variable. If a variable is not initialized it means that it’s initial value can be one of the value in his range
next(state) specifies state transitions. It describes how the value of the variable changes in one step. A case statement assigns the value of the variable associated with each case condition when it is true.

An SMV program can consist of more than one module. In each SMV specification there must be a module main. All other modules are instantiated in main or other parent module:

MODULE counter_Cell(carry_in)
    VAR
        value : boolean;
    ASSIGN
        init(Value) := FALSE;
        next(value) := value xor carry_in;
    
    // C-like macros, do not defines new states
    DEFINE carry_out := value & carry_in; 

MODULE main 
    VAR
        bit0 : counter_cell(TRUE); // instance of the counter_cell module
        bit1 : counter_cell(bit0.carry_out);
        bit2 : counter_cell(bit1.carry_out);

Specifications can be added in any module, and each property is verified separately.

A property in LTL is specified with the keyword LTLSPEC:

LTLSPEC F (bit0.value & bit1.value & bit2.value)

LTLSPEC G F bit2.value

A property in CTL is specified with the keyword SPEC.