NUSMV can work in batch mode, just like SMV, processing an input file according to the specified command line options. In addition, NUSMV has an interactive mode: it enters a shell performing a read-eval-print loop, and the user can activate the various computation steps (e.g. parsing, model construction, reachability analysis, model checking) as system commands with different options. (This interaction mode is largely inspired by the VIS interaction mode [2].) These steps can therefore be invoked separately, possibly undone or repeated under different modalities. Each command is associated with an on-line help. Furthermore, the internal parameters of the system can be inspected and modified to tune the verification process. For instance, the NUSMV interactive shell provides full access to the configuration options of the underlying BDD package. Thus, it is possible to investigate the effect of different choices (e.g. whether and how to partition the model, the impact of different cache configurations) on the verification process. For instance, it is possible to control the application of BDD variable orderings in a particular phase of the verification (e.g. after the model is built).
On top of the interactive shell, a graphical user interface (GUI from now on) has been developed (Figure 1). The GUI provides an integrated environment to edit and verify the file containing the model description. It provides graphical access to all the commands interpreted by the textual shell of NUSMV, and allows for the modification of the options in a menu driven way. Moreover, the GUI offers a formula editor which helps the user in writing new specifications. Depending on the kind of formula being edited (e.g. propositional, CTL, LTL), various buttons corresponding to modalities and/or boolean connectors are activated and deactivated.