2. System Functionalities

NUSMV can process files written in SMV language [6], and allows for the construction of the model with different modalities, reachability analysis, fair CTL model checking, computation of quantitative characteristics of the model, and generation of counterexamples. In addition, NUSMV features an enhanced partitioning method for synchronous models based on [7], and allows for disjunctive partitioning of asynchronous models, and for the verification of invariant properties in combination with reachability analysis. Furthermore, NUSMV supports LTL model checking. The algorithm is based on the combination of a tableau constructor for the LTL formula with standard CTL model checking, along the lines described in [5].

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).

Figure 1: A snapshot of the NuSMV GUI.

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.