Go to the first, previous, next, last section, table of contents.
NuSMV is a symbolic model checker jointly developed by Carnegie
Mellon University (CMU) and Istituto per la Ricerca Scientifica e
Tecnologica (IRST).
The NuSMV project aims at the development of an open architecture
for model checking, which can be reliably used for the verification of
industrial designs, as a core for custom verification tools, as a
testbed for formal verification techniques, and applied to other
research areas.
NuSMV is available at http://nusmv.irst.itc.it/
and at http://www.cs.cmu.edu/~modelcheck/.
The main features of NuSMV are the following:
NuSMV allows for the representation of synchronous and
asynchronous finite state systems, and the analysis of specifications
expressed in Computation Tree Logic (CTL) and Linear Temporal Logic
(LTL). Heuristics are available for achieving efficiency and partially
controlling the state explosion. The interaction with the user can be
carried on with a textual, as well as graphical, interface.
NuSMV have been isolated and separated
in modules. Interfaces between modules have been provided. This should
allow to reduce the effort needed to modify and extend NuSMV.
NuSMV is written in ANSI C, is POSIX compliant, and has been
debugged with Purify in order to detect memory leaks. Furthermore, the
system code is thoroughly commented. NuSMV uses the state of the
art BDD package developed at Colorado University. This makes it very
robust, portable, efficient. Furthermore, its code should be easy to
understand and modify by other people than the developers.
This document is structured as follows.
NuSMV.
NuSMV.
NuSMV interactively the commands of the
interaction shell are described.
NuSMV batch we define the batch mode of NuSMV.