One of the most important features of NUSMV is that it is an open system, and can be easily modified, customized or extended.13 This is possible because the architecture of NUSMV is structured and organized in modules. Each module implements a set of functionalities and communicates with the others via a precisely defined interface. A schema of the system architecture can be found in Figure 10. The modules implementing reduction techniques were designed to work directly on the BDD representation, thus implementing their functionalities independently from the input language used to describe the system. This provides a clear distinction between the system back-end and front-end. This clear distinction makes NUSMV open and usable in different fields, simply replacing or removing the modules specific of the kind of input. Section 7.2 describes an example of extension of NUSMV.
The various modules of the architecture and the provided functionalities are described below.
>
