CISC/CMPE 422, CISC 835: Formal Methods in Software Engineering Using NuSMV

Getting NuSMV

The NuSMV model-checker is available at http://nusmv.fbk.eu. Binaries are available for Linux and Windows. Sources are also available. When you download it you are asked to register, but you do not have to give your name if you don't want to (just click on "Do not register"). The website also provides a User Manual and a Tutorial, which are quite useful.

Once installed, you run NuSMV from the command line by typing NuSMV -int your_smv_file.smv.

Editors with NuSMV support

If you really want editor support for NuSMV though, here are some options:

• In class, I have been using GNU Emacs together with the NuSMV mode provided here.
• An NuSMV plugin for VIM is here. To install, follow the instructions below (thanks, Ally), which assume you've SSH'd in already or have a terminal open on a CASLAB Linux machine in the lab:
  1. In your home directory, run: git clone https://github.com/wannesm/wmnusmv.vim. This will create a directory called wmnusmv.vim
  2. Now create a vim plugins folder, assuming you don't already have one, in your home folder (Note: the name HAS to be what is written below verbatim. That's the place where vim looks for plugins. It's just not there by default.): mkdir -p ~/.vim/plugin
  3. Now copy the syntax file to that folder: cp ~/wmnusmv.vim/syntax/nusmv.vim ~/.vim/plugin/nusmv.vim
  4. That should do it. You can delete the wmnusmv.vim folder in your home directory. Now just open vim with a .smv file and it should work. You might have to turn syntax highlighting on with :syntax on in vim command mode.
• An Eclipse plugin for NuSMV with an editor with syntax highlighting here.
• Also, many editors such as ultraedit or scite can be customized to a new language fairly easily. The list of NuSMV keywords can be found on top of page 7 in the NuSMV 2.6 User Manual.

Notes on using NuSMV

• On the command line use the -int option to run NuSMV in interactive mode.
• Once in NuSMV, the help command will list all commands available, and help command will provide help on a specific command.
• The commands you'll most likely need are:
  • go: reads your model and prepares the internal representation for simulation and analysis.
  • pick_state -i -a: chooses an initial state.
  • simulate -i -a number_of_steps: starts a simulation.
  • show_traces: prints simulations traces
  • check_spec
• The most useful command options are: (use the help command to see the exact options available for each command.)
  • -i: "interactive"
  • -a: "display all state variables"
  • -v: "verbose"
  • -r: "random"
• To save a trace to a file, use show_traces -v -o trace_file_name.txt after a simulation.
• To simulate or analyze a different model the simplest way is to quit NuSMV and restart it with the new model given in the command line.
• There must always be a top-level module called main.
• In order to model-check a specification (not just simulate it) you must add all the specifications to your modules as in

  MODULE main
  ...
  SPEC formula1
  SPEC formula2
  ...
  

  and then you can do one of the following:
  • Run NuSMV in interactive mode (NuSMV -int model.smv) and use the command check_spec, or
  • Run NuSMV in standard checking (non-interactive) mode (NuSMV model.smv)