NUSMV has been explicitly designed to be an open system, which can be easily modified, customized or extended. The system architecture of NUSMV has been structured and organized in modules. Each module implements a set of functionalities and communicates with the others via a precisely defined interface. A clear distinction between the system back-end and front-end has been enforced, in order to make it possible to reuse the internal components independently of the input language being used to describe the model.
The architecture of NUSMV (see Figure 2) is composed of the following modules:
Kernel. The kernel provides the low level functionalities such as dynamic memory allocation, and manipulation of basic data structures (e.g. cons cells, hash tables). The kernel also provides all the basic BDD primitives, directly taken from the CUDD [8] BDD package. The integration of the CUDD package hides the details of the garbage collection. The NUSMV kernel can be used as a black box, following coding standards which have been precisely defined.
Parser. This module implements the routines to process a file written in NUSMV language, check its syntactic correctness, and build a parse tree representing the internal format of the input file.
Compiler. This module is responsible for the compilation of the parsed model into BDDs. The Instantiation submodule processes the parse tree, and performs the instantiation of the declared modules, building a description of the finite state machine (FSM) representing the model. The Encoding submodule performs the encoding of data types and finite ranges into boolean domains. Having separated this module makes it possible to have different encoding policies which can be more appropriate for different kind of variables (e.g. data path, control path). The FSM Compiler submodule provides the routines for constructing and manipulating FSM's at the BDD level. It is responsible of all the necessary semantic checks on the read model, such as the absence of circular definitions. The FSM's can be represented in monolithic or partitioned form [3]. The heuristics used to perform the conjunctive partitioning of the transition relation and reordering of the clusters [7] have been developed to work at the BDD level, independently of the input language. The interface to other modules is given by the primitives for the computation of the image and counter-image of a set of states. These primitives are independent of the method used to represent the transition relation.
Model Checking. This module provides the functionalities for reachability, fair CTL model checking, invariant checking, and computation of quantitative characteristics. Moreover, this module provides the routines for counterexample generation and inspection. Counterexamples can be produced with different levels of verbosity, in the form of reusable data structures, and can subsequently be inspected and navigated. All these routines are independent of the particular method used to represent the FSM.
LTL. The LTL module is a separated module which calls an external program that translates the LTL formula into a tableau suitable to be loaded into NUSMV. This program also generates a new CTL formula to be verified on the synchronous product of the original system and the generated tableau.
Interactive shell. From the interaction shell the user has full access to all the functionalities provided by the system.
Graphical user interface. The graphical user interface has been designed on top of the interactive shell. It allows the user to inspect and set the value of the environment variables of the system, and provides full access to all the functionalities.
>
