This paper describes the results of a joint project between Carnegie Mellon University (CMU) and Istituto per la Ricerca Scientifica e Tecnologica (IRST) whose goal is the development of a new symbolic model checker.1 The new model checker, called NUSMV, is designed to be a well structured, open, flexible and documented platform for model checking. To be usable in technology transfer projects, NUSMV was designed to be very robust, easy to modify, and close to the standards required by industry.
NUSMV is the result of the reengineering and reimplementation of the CMU SMV [47,26] symbolic model checker. With respect to CMU SMV, NUSMV has been upgraded along three dimensions.
The paper is organized as follows: in Section 2 we briefly introduce the logical framework below symbolic model checking; Section 3 describes the interaction with the system; Section 4 explains the functionalities provided by the system; Section 5 describes the NUSMV system architecture; Section 6 describes the NUSMV implementation features. Finally, Section 7 describes the results of some tests and future development directions.
NUSMV is available at the url ``|http://nusmv.irst.itc.it|''.