In computer science, NuSMV is a reimplementation and extension of the SMV symbolic model checker, the first model checking tool based on binary decision diagrams (BDDs). The tool has been designed as an open architecture for model checking. It is aimed at reliable verification of industrially sized designs, for use as a backend for other verification tools and as a research tool for formal verification techniques.
NuSMV has been developed as a joint project between ITC-IRST ( in Trento), Carnegie Mellon University, the University of Genoa and the University of Trento.
NuSMV 2, version 2 of NuSMV, inherits all the functionalities of NuSMV. Furthermore, it combines BDD-based model checking with SAT-based model checking. It is maintained by Fondazione Bruno Kessler, the successor organization of ITC-IRST.
NuSMV supports the analysis of specifications expressed in computation tree logic (CTL) and linear temporal logic (LTL). It can be run in batch mode, or interactively with a textual user interface.
The interaction shell of NuSMV is activated from the system prompt as follows:
NuSMV first tries to read and execute commands from an initialization file if such file exists and is readable unless was passed on the command line. File is looked for in the directories defined in environment variable or in the default library path if no such variable is defined. If no such file exists, user's home directory and the current directory will also be checked. Commands in the initialization file are executed consecutively. When the initialization phase is completed the NuSMV shell prompt is displayed and the system is now ready to execute user commands.
A NuSMV command usually consists of a command name and arguments to the invoked command. It is possible to make NuSMV read and execute a sequence of commands from a file, through the command line option :
When the -int option is not specified, NuSMV runs as a batch program, which is with the form as follows:
NuSMV can be used to check whether given LTL or CTL constraints holds for a given model. For example, we have a CTL specification that we want to check:
This specification is true if there exists an execution path such that the component of the process has the value at some point. User can check to see if their model holds for this specification using the following commands.
If the specification is true, NuSMV will inform you with
If some specification fails, NuSMV will return a full trace of execution showing how it fails, if possible.