NuSMV
Encyclopedia
Introduction
NuSMV is a reimplementation and extension of 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 (Istituto Trentino di Cultura, Istituto per la Ricerca Scientifica e Tecnologica in Trento
Trento
Trento is an Italian city located in the Adige River valley in Trentino-Alto Adige/Südtirol. It is the capital of Trentino...
, Italy
Italy
Italy , officially the Italian Republic languages]] under the European Charter for Regional or Minority Languages. In each of these, Italy's official name is as follows:;;;;;;;;), is a unitary parliamentary republic in South-Central Europe. To the north it borders France, Switzerland, Austria and...
), Carnegie Mellon University
Carnegie Mellon University
Carnegie Mellon University is a private research university in Pittsburgh, Pennsylvania, United States....
, the University of Genoa
University of Genoa
The University of Genoa is one of the largest universities in Italy.Located in Liguria on the Italian Riviera, the university was founded in 1471. It currently has about 40,000 students, 1,800 teaching and research staff and about 1,580 administrative staff.- Campus :The University of Genoa is...
and the University of Trento
University of Trento
The University of Trento is an Italian university located in the cities of Trento and Rovereto. It has been able to achieve considerable results in didactics, research and international relations, as shown by Censis University Guide and by the Italian Ministry of...
. .
NuSMV 2, version 2 of NuSMV, inherits all the functinalities of NuSMV. Furthermore, it combines BDD
Binary decision diagram
In the field of computer science, a binary decision diagram or branching program, like a negation normal form or a propositional directed acyclic graph , is a data structure that is used to represent a Boolean function. On a more abstract level, BDDs can be considered as a compressed...
-based model checking with SAT
Boolean satisfiability problem
In computer science, satisfiability is the problem of determining if the variables of a given Boolean formula can be assigned in such a way as to make the formula evaluate to TRUE...
-based model checking. It is maintained by Fondazione Bruno Kessler, the successor organization of ITC-IRST.
Functionalities
NuSMV supports the analysis of specifications expressed in CTL and LTLLinear temporal logic
In logic, Linear temporal logic is a modal temporal logic with modalities referring to time. In LTL, one can encode formulae about the future of paths such as that a condition will eventually be true, that a condition will be true until another fact becomes true, etc. It is a fragment of the more...
. User interaction is performed with a textual interface, as well as in batch mode.
Running NuSMV Interactively
The interaction shell of NuSMV is activated from the system prompt as follows:system_prompt> NuSMV -int
NuSMV> go
NuSMV>
NuSMV first tries to read and execute commands from an initialization file if such file exists and is readable unless -s is passed on the command line.
File master.nusmvrc is looked for in directory defined in environment variable NUSMV _LIBRARY_PATH or in default library path if no such variable is defined. If no such file exists, user's home directory and current directory will also be checked. Commands in the initialization file are executed consecutively. When initialization phase is completed the NuSMV shell 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 -source:
system_prompt> NuSMV -source cmd_file
Running NuSMV batch
When the -int option is not specified, NuSMV runs as a batch program, which is with the form as follows:system_prompt> NuSMV [command line options] input_file
The program described in input_file will be processed and the corresponding finite state is built.
Checking for LTL specification or CTL specification
NuSMV can be used to check whether the predefined LTLLinear temporal logic
In logic, Linear temporal logic is a modal temporal logic with modalities referring to time. In LTL, one can encode formulae about the future of paths such as that a condition will eventually be true, that a condition will be true until another fact becomes true, etc. It is a fragment of the more...
or CTL constraints holds for the defined model.
For example, we have an CTL specification that we want to check
CTLSPEC EF(proc5.state = critical);
This specification checks that if there exists an execution path such that the state of process 5 is critical at some point.
User can check to see if their model holds for this specification using the following commands.
system_prompt> NuSMV [command line options] input_file
NuSMV> go
NuSMV> check_ctlspec
If the specification is true, NuSMV will inform you with
-- specification EF proc5.state = critical is true
>NuSMV
However, if the specification fails at some state, NuSMV will retrun a full trace of execution showing how it fails.
External links
- NuSMV-tools website: a set of tools based on eclipse for the model checker NuSMV.