An overview of NuSMV

NuSMV is a software tool for the formal verification of finite state systems. It has been developed jointly by FBK-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, bit vectors 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:

1. Interaction. In addition to the usual SMV batch mode, NuSMV provides a textual interaction shell.
   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.
2. 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.
3. Partitioning methods. The model can be partitioned conjunctively and disjunctively [burch2]. The partitions can be inspected, and (for the conjunctive case) ordered according to the heuristics defined in [ranjan1].
4. 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 model.
5. PSL Model Checking. Property Specification Language, [psl03] that includes CTL and LTL with Sequencial Extended Regular Expressions (SERE), a variant of classical regular expressions.
6. SAT-based Bounded Model Checking.

For more details about NuSMV see the overview paper.