Introduction

REMARK. This manual is outdated and does not describe all the new features of NuSMV2. An updated version of the manual will be made available as soon as possible. section Getting started with BMC contains a quick introduction to the SAT based Bounded Model Checking provided by NuSMV2.

NuSMV is a symbolic model checker jointly developed by Carnegie Mellon University (CMU) and Istituto per la Ricerca Scientifica e Tecnologica (IRST). The NuSMV project aims at the development of an open architecture for model checking, which can be reliably used for the verification of industrial designs, as a core for custom verification tools, as a testbed for formal verification techniques, and applied to other research areas. NuSMV is available at http://nusmv.irst.itc.it.

The main features of NuSMV are the following:

• Functionalities. NuSMV allows for the representation of synchronous and asynchronous finite state systems, and the analysis of specifications expressed in Computation Tree Logic (CTL) and Linear Temporal Logic (LTL). Heuristics are available for achieving efficiency and partially controlling the state explosion. The interaction with the user can be carried on with a textual, as well as graphical, interface.
• Architecture. A software architecture has been defined. The different components and functionalities of NuSMV have been isolated and separated in modules. Interfaces between modules have been provided. This should allow to reduce the effort needed to modify and extend NuSMV.
• Quality of the implementation. NuSMV is written in ANSI C, is POSIX compliant, and has been debugged with Purify in order to detect memory leaks. Furthermore, the system code is thoroughly commented. NuSMV uses the state of the art BDD package developed at Colorado University. This makes it very robust, portable, efficient. Furthermore, its code should be easy to understand and modify by other people than the developers.

This document is structured as follows.

• In section Examples we present some examples of usage of NuSMV.
• In section Syntax we define the syntax of the input language of NuSMV.
• In section Running NuSMV interactively the commands of the interaction shell are described.
• In section Running NuSMV batch we define the batch mode of NuSMV.
• In section Getting started with BMC we describe the SAT based Bounded Model Checking provided by NuSMV.

Go to the first, previous, next, last section, table of contents.