Maintainability.

• 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 [58] 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 [6] system.
• The code of NUSMV is documented following the standards of the ext tool.¹⁶ 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 interface.
• The user manual is written following the standard TEXINFO[16]. 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.