NuSMV
{{Short description|Reimplementation and extension of SMV model checker}}
{{Infobox software
| name = NuSMV
| developer = FBK-irst (Trento, Italy), CMU (Pittsburgh, PA), The University of Genova (Italy), The University of Trento (Italy)
| latest release version = 2.7.0
| latest release date = {{Release date and age|2024|10|25}}{{cite press release |title=Version 2.7.0 |url=https://nusmv.fbk.eu/articles/270/ |website=NuSMV |publisher=Fondazione Bruno Kessler |date=October 25, 2024}}
| programming language = ANSI C
| operating_system = Linux, Mac OS X, Microsoft Windows
| genre = Model Checking
| license = LGPL v2.1
| website = [http://nusmv.fbk.eu/ nusmv.fbk.eu]
}}
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).K.L. McMillan. Symbolic model checking. In Kluwer Academic Publ.,1993.
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 ({{ill|Istituto trentino di cultura|it}} 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.A. Biere, A. Cimatti, E. Clarke, and Y. Zhu. Symbolic model checking without BDDs. In Tools and Algorithms for Construction and Analysis of Systems, In TACAS’99, March 1999. It is maintained by [http://www.fbk.eu Fondazione Bruno Kessler], the successor organization of ITC-IRST.
Functionalities
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.
= 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
File
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
[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
Checking for LTL specification or CTL specification
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:
CTLSPEC EF(proc5.state = critical);
This specification is true if there exists an execution path such that the component
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
If some specification fails, NuSMV will return a full trace of execution showing how it fails, if possible.
See also
- Spin Model Checker a general model checker for asynchronous software systems
- CADP (Construction and Analysis of Distributed Processes), a toolbox for the formal design of asynchronous concurrent systems
References
{{Reflist|30em}}
External links
- [http://nusmv.fbk.eu/ NuSMV website]
- [https://sourceforge.net/projects/nuseen/ Nuseen website]: a set of tools based on eclipse for the model checker NuSMV.
- [https://nuxmv.fbk.eu nuXmv]: Extends NuSMV with SMT-based verification and updated SAT solving techniques