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

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.


Home : Teaching : Courses : Fv 

Informatics Forum, 10 Crichton Street, Edinburgh, EH8 9AB, Scotland, UK
Tel: +44 131 651 5661, Fax: +44 131 651 1426, E-mail: school-office@inf.ed.ac.uk
Please contact our webadmin with any comments or corrections. Logging and Cookies
Unless explicitly stated otherwise, all material is copyright © The University of Edinburgh