NuSMV2.6符号模型检查器的用户手册

　　NUSMV是一个符号模型检查器，源于CMU-SMV的重新设计、实现和扩展，CMU-SMV是CMU［McM93］开发的基于BDD的原始模型检查器。NUSMV项目旨在开发一个最先进的符号模型检查器，设计用于技术转让项目：它是一个很好的结构化的、开放的、灵活的和有文件化的模型检查平台，并且是鲁棒的并且接近工业系统标准CGR00。

　　NUSMV的版本1基本上实现了基于BDD的符号模型检查。NUSMV的版本2（以下简称NUSMV2）继承了前一版本的所有功能，并在多个方向上进行了扩展〔CCG+02〕。NUSMV2的主要创新之处在于集成了基于命题可满足性（SAT）的模型检测技术〔BCCZ99〕。目前基于SAT的模型检测正受到人们的青睐在多个工业领域取得重大成功，开辟了新的研究方向。基于BDD和基于SAT的模型检查通常能够解决不同类别的问题，因此可以看作是互补技术。

　　从NUSMV2开始，我们也采用了一种新的开发和许可模式。NUSMV2是与一个开源许可证1一起发布的，它允许任何感兴趣的人自由使用该工具并参与其开发。NUSMV开源项目的目的是为模型检查社区提供一个研究、实现和比较新的符号模型检查技术的通用平台。自NUSMV2发布以来，NUSMV团队已经收到了系统不同部分的代码贡献。一些研究机构和商业公司表示有兴趣合作开发NUSMV。NUSMV的主要特点如下：

　　•功能。NUSMV允许同步和异步有限状态系统2的表示，并允许使用基于BDD和基于SAT的模型检查技术分析以计算树逻辑（CTL）和线性时序逻辑（LTL）表示的规范。启发式方法可用于实现效率和部分控制状态爆炸。与用户的交互可以通过文本界面进行，也可以在批处理模式下进行。

　　建筑。定义了一个软件体系结构。NUSMV的不同组成部分和功能在模块中被隔离和分离。提供了模块之间的接口。这减少了修改和扩展NUSMV所需的工作量。

　　执行质量。NUSMV是用ANSI C编写的，符合POSIX，并且已经用Purify进行了调试，以便检测内存泄漏。此外，对系统代码进行了彻底的注释。NUSMV使用了科罗拉多大学开发的最新BDD包，并提供了一个通用接口，用于连接最新的SAT解算器。这使得NUSMV非常健壮、可移植、高效，并且容易被开发人员以外的人理解。

　　在本章中，我们将介绍NUSMV输入语言的语法和语义。在讨论语言的细节之前，让我们先给出一些关于语法的一般注释。在下面使用的语法符号中，语法类别（非终端）用单空格字体表示，标记和字符集成员（终端）用粗体字体表示。方括号（“［”）中包含的语法结果是可选的，而竖线（“|”）用于分隔语法规则中的替代项。有时，在规则的开头使用一个of作为在多个备选方案中进行选择的速记。如果字符|、〔和〕是粗体，它们就失去了特殊的意义，成为常规的标记。在下面的代码中，标识符可以是任何字符序列，以集合{a-Za-z}中的一个字符开始，然后是属于集合{a-Za-z0-9$#-}的一个可能为空的字符序列。标识符中的所有字符和大小写都是有意义的。空白字符是空格（）、制表符（）和换行符（）。任何以两个破折号（‘--’）开头、以换行符结尾的字符串都是注释，解析器将忽略这些字符串。多行注释以“-/--”开头，以“--/”结尾。标识符的语法规则为：