The NUSMV interactive shell

In this mode the system enters a read-eval-print loop. The user can activate the various NUSMV computation steps as system commands with different options. These steps can therefore be invoked separately, possibly undone or repeated. These steps include the construction of the model in different ways and the model checking of specifications.

The NUSMV interactive shell allows for the full configuration of the BDD options. For instance, several automatic variable ordering methods and cache configuration mechanisms can be suitably tuned according to the application.

Moreover, the NUSMV interactive shell provides the user with a script language that makes it possible to define different model checking algorithms that can be invoked as model checking tactics. These algorithms are provided via parameterized scripts.

The interactive shell of NUSMV is activated from the system prompt as follows (``NuSMV>'' is the default prompt that NUSMV prints out to indicate that it is ready to evaluate commands):

 system_prompt> NuSMV -int
 NuSMV release 1.0 (compiled 11-Nov-98 at 8:28 PM)
 NuSMV >

In Figure 6 we can see a typical interaction with NUSMV through the interactive shell.⁵ The file ``counter.smv'' contains the example depicted in Figure 4. The verification process in NUSMV can be decomposed into the following sequence of basic steps.

  

Figure 6: A typical interaction with NuSMV via the interactive shell. NuSMV commands are in boldface.

1.

The first step towards verification is reading the model. This is performed by typing the NUSMV command read_model. This command takes as argument a file name containing the model specification. After the correct execution of this command an internal representation of the read file is built and stored.

2.

The second step consists in transforming the hierarchical description into a flattened description. This is performed by typing the command flatten_hierarchy. After the correct execution of this command all the information needed to build the automaton is separated out (e.g., the variable names, their range, a symbolic representation of the initial states and of the transition relation of the flattened system).

3.

The third step consists in the encoding of the scalar variables into boolean variables. The NUSMV command
build_variables is responsible for this task. It takes an optional argument specifying a file containing the ordering in which the variables have to be built.⁶ As a default, the order of variables used by NUSMV corresponds to the order in which the variables appear in a depth first traversal of the hierarchy [19].

4.

The fourth step consists of the compilation of the structures built by the flatten_hierarchy into BDDs using the encoding performed by build_variables. During this step some checks are performed that avoid circular dependencies in assignments and multiple definitions [19]. The NUSMV command that implements this step is build_model. This command has an option specifying the partitioning method to be used, i.e. monolithic, conjunctive, or disjunctive (see Section 4). It is possible to build first the transition relation in different formats and then choose the most appropriate to the specific problem.

5.

The fifth step deals with the fairness constraints [12]. This command can be executed only when all the previous commands have been executed. This is due to the fact that fairness constraints are CTL formulas whose evaluation uses a previously computed transition relation.

After these five steps, the internal representation of the automaton is available to perform model checking.

6.

It is possible to compute the set of reachable states, via the compute_reachable command. This allows the user to simplify the evaluation of all the specifications by restricting the search only to reachable states.

7.

It is possible to start the verification of CTL specifications (via the check_spec command), of LTL specifications (via the check_ltlspec command), and of invariants (via the check_invar command). All these commands, if called with no arguments, apply to the specifications of the respective type, if any, listed in the source file. Optionally a CTL, LTL or propositional formula can be given as an argument. In the transcript of Figure 6 first we check the property AG AF bit2.carry_out (the execution of check_spec without arguments, thus verifying the properties listed in the input file). Then we check the property AG AX bit2.carry_out (invariantly in the next state bit2.carry_out is 1). This property appear to be false and a counterexample exploiting why the formula is not verified is computed and printed out.