- In order to implement the architecture depicted in
Section 5, the source code of NUSMV has
been separated into different packages. At the moment NUSMV is
composed of 11 packages. Each package exports a set of routines
that manipulate the data structures defined in the package and
modify the options associated to the functionalities
provided by the package itself. Moreover, each package is
associated with a set of commands that can be interpreted by
the NUSMV interactive shell. We have packages for model
checking, FSM compilation, BDD interfacing, LTL model
checking and kernel functionalities. New packages can be added
relatively easily, following precisely defined rules.
- The source code of NUSMV is maintained using a tool for
revision controls. We use the RCS  tool provided
by GNU. It automates the storing, retrieval, logging and merging of
revisions and provides a simple and user friendly interface.
- In the coding, we have used an object-oriented programming style,
following the ideas exploited by the VIS  system.
- The code of NUSMV is documented following the standards of the ext
This tool allows for the automatic extraction of the programmer
manual from the source comments in the system code. The
programmer manual is available in TXT or HTML
format, in a way that is browsable by an HTML viewer. This
tool is also used to generate the help on line available
through the interactive shell and via the graphical user
- The user manual is written following the standard
TEXINFO. This allows us to have the user
manual available in different formats (for instance
POSTSCRIPT, PDF, DVI, INFO,
HTML), directly from the NUSMV interactive shell, via
an HTML viewer or in hardcopy.