NuSMV工具的安装与使用

1. NuSMV的下载安装

1.1 NuSMV的下载安装

点击此处 (opens new window)下载NuSMV-2.6.0-win64.tar.gz，并将其中的bin目录添加到环境变量。

1.2 NuSMV的使用

NuSMV的运行命令为：nusmv [command line options] input-file

给定SMV语言定义的模型输入文件input-file，工具将建立其模型对应的有限状态自动机，然后对输入文件中的验证属性进行验证。验证属性通过LTL或CTL语言定义。对每个不成立的属性，工具将给出一条反例。默认情况下，工具采用基于BDD的模型检验方法。

工具要用到的主要控制选项包括：

选项	主要功能
-int	采用交互模式进行验证
-source sc_file	从sc_file中读取NuSMV命令
-lp	显示SMV模型的所有属性
-n idx	指定需要验证的属性
-is	不验证SPEC属性
-ic	不验证COMPUTE属性
-ils	不验证LTLSPEC属性
-ips	不验证PSLSPEC属性
-ii	不验证INVARSPEC属性
-AG	只验证AG属性
-coi	启用cone of influence reduction策略
-bmc	使用基于BMC的模型检验方法(仅针对LTL和PSL属性)
-bmc-length k	设置限界模型检验的展开长度k，默认长度为10
-sat_solver_name	设置使用的SAT求解器，默认求解器为MiniSat

2. SMV语言介绍

2.1 SMV语言的保留关键字

MODULE, DEFINE, MDEFINE, CONSTANTS, VAR, IVAR, FROZENVAR, INIT, TRANS, INVAR, SPEC, CTLSPEC, LTLSPEC, PSLSPEC, COMPUTE, NAME, INVARSPEC, FAIRNESS, JUSTICE, COMPASSION, ISA, ASSIGN, CONSTRAINT, SIMPWFF, CTLWFF, LTLWFF, PSLWFF, COMPWFF, IN, MIN, MAX, MIRROR, PRED, PREDICATES, process, array, of, boolean, integer, real, word, word1, bool, signed, unsigned, extend, resize, sizeof, uwconst, swconst, EX, AX, EF, AF, EG, AG, E, F, O, G, H, X, Y, Z, A, U, S, V, T, BU, EBF, ABF, EBG, ABG, case, esac, mod, next, init, union, in, xor, xnor, self, TRUE, FALSE, count, abs, max, min

2.2 数据类型

类型名称	取值
boolean	FALSE,TRUE
integer	-(231-1)...(231-1)
枚举类型
word

1. 枚举类型

枚举类型是NuSMV中的一种常用类型，其基本定义方式如下：
{stopped, running, waiting, finished}
{2, 4, -2, 0}
{FALL, 1, 3, 7, OK}

2. Word

        word用来表示位向量，其基本写法是unsigned word[•]或signed word[•]。该类型允许按位的逻辑和算术运算。例如，unsigned word[3]表示包含3个bit，且允许各种无符号运算，signed word[7]表示7个bit，且允许各种有符号运算。

3. Array

数组的定义方式如下，在数组的定义中需要定义数组下标的下界和上界，以及数组元素的类型。

array 0..3 of boolean
array 10..20 of {OK, y, z}
array 1..8 of array -1..2 of unsigned word[5]

2.3 表达式

2.4 有限状态自动机的定义

2.5 属性描述