| 词条 | NuSMV |
| 释义 |
| name = NuSMV | developer = FBK-irst (Trento, Italy), CMU (Pittsburgh, PA), The University of Genova (Italy), The University of Trento (Italy) | latest release version = 2.6.0 | latest release date = {{Release date and age|2015|10|14}} | programming language = ANSI C | operating_system = Linux, Mac OS X, Microsoft Windows | genre = Model Checking | license = LGPL v2.1 | website = nusmv.fbk.eu }}NuSMV is a reimplementation and extension of SMV symbolic model checker, the first model checking tool based on Binary Decision Diagrams (BDDs).[1] 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 in Trento, Italy), 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.[2] It is maintained by Fondazione Bruno Kessler, the successor organization of ITC-IRST. FunctionalitiesNuSMV supports the analysis of specifications expressed in CTL and LTL. User interaction is performed with a textual interface, as well as in batch mode. Running NuSMV InteractivelyThe 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 batchWhen 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 specificationNuSMV can be used to check whether the predefined LTL or CTL constraints holds for the defined model. For example, we have a CTL specification that we want to check: CTLSPEC EF(proc5.state = critical); This specification checks 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 >NuSMV However, if the specification fails at some state, NuSMV will return a full trace of execution showing how it fails. See also
References1. ^K.L. McMillan. Symbolic model checking. In Kluwer Academic Publ.,1993. 2. ^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. External links
2 : Model checkers|Free software programmed in C |
| 随便看 |
|
开放百科全书收录14589846条英语、德语、日语等多语种百科知识，基本涵盖了大多数领域的百科知识，是一部内容自由、开放的电子版国际百科全书。