University Homepage School Homepage School Contacts School Search

Formal Verificationy: NuSMV Startup Guide

NuSMV is available on DICE machines in the AT labs. We are using v2.6 (although version 2.5.4 should also be fine). A Tutorial and User Manual are available from the NuSMV website. Visit this website for binaries for Linux or Windows and for source code.

See the NuSMV lecture slides for a brief introduction to NuSMV. The input files discussed in the slides are

• toggle.smv
• count10.smv
• atm.smv
• count100.smv

The simplest way to run NuSMV is in batch mode: type NuSMV a.smv at a Unix command-line prompt to run NuSMV on file a.smv. Useful NuSMV command-line options include:

-n i

Check only specification i (numbered from 0)

-dcx

Disable display of counter examples to false specifications

NuSMV also has an interactive mode which allows much finer control of NuSMV's behaviour. To run in interactive mode on file a.smv, use the command NuSMV -int a.smv. Useful commands at the NuSMV> interactive prompt include

go

Run the commands read_model, flatten_hierarchy, encode_variables, build_model. This gets NuSMV ready for doing model checking.

check_ltlspec

Model check each of the LTL specifications from the SMV source file. Use option "-n i" to check only the specification with index i (starting from 0).

pick_state

Pick an initial state for a simulation of the model.

simulate -p n

Run a simulation for n steps, printing out at each step the values of state variables that have changed. When there are multiple next states, the choice is deterministic. Options for the simulate and pick_state commands allow random and interactive choices of states.

quit

Exit NuSMV

For a brief description of the options supported by a command, run the command with option -h. For more details, see the User Manual.