NuSMV is a software tool for the formal verification of
finite state systems.
It has been developed jointly by ITC-IRST and by Carnegie Mellon University.
NuSMV allows to check finite state systems against specifications in
the temporal logic CTL.
The input language of NuSMV is designed to allow the description of
finite state systems that range from completely synchronous to
completely asynchronous. The NuSMV language (like the language of
SMV) provides for modular hierarchical descriptions and for the
definition of reusable components. The basic purpose of the NuSMV
language is to describe (using expressions in propositional
calculus) the transition relation of a finite Kripke structure. This
provides a great deal of flexibility, but at the same time it can
introduce danger of inconsistency (for non expert users).
Since NuSMV is intended to describe finite state machines, the only
data types in the language are finite ones, i.e. boolean,
scalar and fixed arrays of basic data types.
NuSMV is a reimplementation and a reengineering of the
SMV model checker developed by McMillan at Carnegie Mellon University
during his PhD.
With respect to SMV, NuSMV provides the following additional features:
In addition to the usual SMV batch mode, NuSMV provides a textual
Through the shell the user can activate
various NuSMV computation steps as system commands with different
options. These computation steps can therefore be invoked
separately and possibly undone.
- Analysis of invariants. Specialized routines allow for
checking invariants, i.e. formulae which must hold uniformly on
the model, on the fly during reachability analysis.
- Partitioning methods. The model can be partitioned
conjunctively and disjunctively
The partitions can be inspected, and (for the conjunctive case)
ordered according to the heuristics defined in
- LTL Model Checking. LTL model checking is performed via
reduction to CTL model checking, according to the algorithm proposed in
[clarke4]. An LTL
specification is automatically converted into a tableau, which is
then used to extend the model in synchronous product. The result is
provided by checking the truth of a CTL formula in the extended
For more details about NuSMV see the overview paper.