The kernel of NUSMV provides low level functionalities, such as dynamic memory allocation, in a way independent from the underlying operating system. Moreover, it provides routines for the manipulation of basic data structures such as cons cells, hash tables, arrays of generic types, and encapsulates the CUDD BDD package [8].
In order to implement the architecture depicted in Section 3, the source code of NUSMV has been organized in different packages. NUSMV is composed of 11 packages. Each package exports a set of routines which manipulate the data structures defined in the package and which allow to modify the options associated to the functionalities provided by the package itself. Moreover, each package is associated with a set of commands which can be interpreted by the NUSMV interactive shell. We have packages for model checking, FSM compilation, BDD interface, LTL model checking and kernel functionalities. New packages can be added relatively easily, following precisely defined rules.
The GUI has been developed in Tcl/Tk. It runs as a separate process, synchronously communicating with NUSMV by issuing textual commands to the interactive shell, and processing the resulting output to display it graphically.
The code of NUSMV has been documented following the standards of the ext tool (http://alumnus.caltech.edu/~sedwards/ext), which allows for the automatic extraction of the programmer manual from the comments in the system source code. The programmer manual is available in TXT or HTML format, and can be browsed 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 interface.
The user manual has been written following the TEXINFO standard, from which different formats (i.e. POSTSCRIPT, PDF, DVI, INFO, HTML) can be automatically generated, and accessed via an HTML viewer or in hardcopy.
>