NUSMV: A New Symbolic Model Verifier
NUSMV: A New Symbolic Model Verifier
复制标题
DOI：
10.1007/3-540-48683-6_44
复制
发表时间：
1999-07
期刊：
影响因子：
--
通讯作者：
A. Cimatti;E. Clarke;Fausto Giunchiglia;Marco Roveri
中科院分区：
文献类型：
--
作者：
A. Cimatti;E. Clarke;Fausto Giunchiglia;Marco Roveri
本文介绍了NuSMV，一个新的符号模型检查器开发的卡内基梅隆大学（CMU）和Istituto每拉Ricerca科技（IRST）之间的联合项目。NuSMV被设计成一个结构良好、开放、灵活和文档化的模型检查平台。为了使NuSMV适用于技术转让项目，它被设计得非常健壮，接近工业所需的标准，并允许表达性的规范语言。NuSMV是SMV [6] 2.4版的重新设计、重新实现和扩展的结果。4（SMV从现在开始）。在SMV方面，NuSMV沿着沿着三个维度进行了扩展和升级。首先，从系统功能的角度来看，NuSMV具有文本交互外壳和图形界面，扩展的模型划分技术，并允许LTL模型检查。其次，NuSMV的系统架构设计为高度模块化和开放式。不同模块之间的相互依赖性已经被分离，并且外部的最先进的BDD包[8]已经被集成到系统内核中。三是执行质量有力提升。这使得NuSMV成为一个强大的，可维护的和有良好文档记录的系统，具有相对容易修改的源代码。NuSMV可在http：//afrodite上查阅。国贸中心。它：1024/nusmv/。
This paper describes NuSMV, a new symbolic model checker developed as a joint project between Carnegie Mellon University (CMU) and Istituto per la Ricerca Scientifica e Tecnolgica (IRST). NuSMV is designed to be a well structured, open, flexible and documented platform for model checking. In order to make NuSMV applicable in technology transfer projects, it was designed to be very robust, close to the standards required by industry, and to allow for expressive specification languages. NuSMV is the result of the reengineering, reimplementation and extension of SMV [6], version 2.4. 4 (SMV from now on). With respect to SMV, NuSMV has been extended and upgraded along three dimensions. First, from the point of view of the system functionalities, NuSMV features a textual interaction shell and a graphical interface, extended model partitioning techniques, and allows for LTL model checking. Second, the system architecture of NuSMV has been designed to be highly modular and open. The interdependencies between different modules have been separated, and an external, state of the art BDD package [8] has been integrated in the system kernel. Third, the quality of the implementation has been strongly enhanced. This makes of NuSMV a robust, maintainable and well documented system, with a relatively easy to modify source code. NuSMV is available at http://afrodite. itc. it: 1024/nusmv/.