Introduction

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.¹ 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.

• From the point of view of the system functionalities, NUSMV has some features (e.g., multiple interfaces, LTL specifications) that enhance the user ability to interact with the system, and provide more heuristics for, e.g., achieving efficiency or partially controlling the state explosion.

• The system architecture of NUSMV is highly modular (thus allowing for the substitution or elimination of certain modules) and open (thus allowing for the addition of new modules). A further feature is that in NUSMV the user can control, and possibly change, the order of execution of some system modules.

• The quality of the implementation is much enhanced. NUSMV is a very robust and well documented system, whose code is (relatively) easy to modify.

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|''.