NuSMV 2: An OpenSource Tool for Symbolic Model Checking

摘要

This paper describes version 2 of the NuSMV tool. NuSMV is a symbolic model checker originated from the reengineering, reimplementation and extension of SMV, the original BDD-based model checker developed at CMU. The NuSMV project aims at the development of a state-of-the-art symbolic model checker, designed to be applicable in technology transfer projects: it is a well structured, open, flexible and documented platform for model checking, and is robust and close to industrial systems standards. The first version of NuSMV, referred with NuSMVl in the following, basically implements BDD-based symbolic model checking. The new version of NuSMV (NuSMV2 in the following) inherits all the functionalities of the previous version, and extend them in several directions. The main novelty in NuSMV2 is the integration of model checking techniques based on propositional satisfia- the comparison of new symbolic model checking techniques. NuSMV2 has been released in November 2001. Since then, the NuSMV team has received code contributions for different parts of the system. Several research institutes and commercial companies have express interest in collaborating to the development of NuSMV. In this paper we describe the goals of the NuSMV OpenSource project (Section 2), we give an overview of the system (Section 3), and we end with some concluding remarks (Section 4).