NuSMV2.6模型检查器用户手册与技术概述

需积分: 50 41 浏览量更新于2024-07-09 收藏 765KB PDF 举报

"NuSMV2.6是一个符号模型检查器，它主要用于验证离散时间系统的性质。这个技术资料和用户手册提供了关于如何使用NuSMV2.6的详细信息，包括其输入语言、表达式、状态机定义等多个方面。NuSMV是由FBK-irst（现称为FBK - Fondazione Bruno Kessler）开发的，它的源代码可以在http://nusmv.fbk.eu找到。该文档的部分内容参考了K. McMillan的"The SMV System-Draft"。" NuSMV是一个强大的工具，它使用符号方法进行模型检查，这使得它能够处理非常大的系统模型。模型检查是验证领域的一个关键技术，它允许我们在设计阶段就发现可能存在的错误，而无需实际构建和测试系统。在NuSMV2.6中，输入语言是定义模型的关键部分。它支持多种类型，如： 1. **布尔类型**: 用于表示逻辑值，通常用于描述系统的行为和条件。 2. **整数类型**: 支持整数运算，可以用于表示计数器或其他数值变量。 3. **枚举类型**: 允许定义有限的离散值集合，例如状态机的状态。 4. **字类型**: 用于表示位串，常用于处理位操作或硬件描述。 5. **数组类型**: 可以存储和操作多个相同类型的元素，类似于编程语言中的数组。 6. **集合类型**: 用于存储不重复的元素，可以用来表示一组对象或状态。 7. **类型顺序**: 定义了类型之间的比较规则。输入语言还包含各种表达式，如： - **隐式类型转换**: 系统会自动将一种类型转换为另一种类型，如果可能的话。 - **常量表达式**: 如数字、字符串等静态不变的值。 - **基本表达式**: 包括算术、逻辑和关系操作符。 - **简单和Next表达式**: 描述当前状态和下一个状态的变量。 - **类型转换运算符**: 显式地将一个类型的值转换为另一个类型。状态机（Finite State Machine, FSM）的定义是NuSMV模型的核心，它由变量声明、定义和赋值规则组成： - **变量声明**: 定义系统中的状态变量，它们可以是上述的任何类型。 - **DEFINE声明**: 用于创建别名或定义计算，简化模型的表述。 - **赋值规则**: 规定了在状态转移中变量如何改变。此外，NuSMV还包括了对LTL（Linear Temporal Logic）和CTL（Computation Tree Logic）等逻辑表达式的支持，这些逻辑语言可以用来描述复杂的系统性质和行为约束。用户可以通过这些表达式来指定系统应该满足的规范，并使用NuSMV来验证这些规范是否能够始终得到满足。 NuSMV2.6是模型检查者的一个强大工具，它提供了丰富的语言特性，可以帮助工程师和研究人员验证各种复杂系统的正确性。通过深入理解这个用户手册，用户可以有效地利用NuSMV进行形式验证，提高软件和硬件设计的质量。

Equality (=) and Inequality (!=)

The operators = (equality) and != (inequality) have the following signature:

=, != : boolean * boolean → boolean

: integer * integer → boolean

: symbolic enum * symbolic enum → boolean

: integers-and-symbolic enum * integers-and-symbolic enum → boolean

: unsigned word[N] * unsigned word[N] → boolean

: signed word[N] * signed word[N] → boolean

No implicit type conversion is performed. For example, in the expression

TRUE = 5

the left operand is of type boolean and the right one is of type integer. Though the signature

of the operation does not have a boolean * integer rule, the expression is not correct, because

no implicit type conversion will be performed. One can use the toint or the bool for explicit

casts.

For example:

toint(TRUE) = 5

TRUE = bool(5)

This is also true if one of the operands is of type unsigned word[1] and the other one is of the

type boolean. Explicit cast must be used (e.g. using word1 or bool)

Relational Operators >, <, >=, <=

The relational operators > (greater than), < (less than), >= (greater than or equal to) and <=

(less than or equal to) have the following signature:

>, <, >=, <= : integer * integer → boolean

: unsigned word[N] * unsigned word[N] → boolean

: signed word[N] * signed word[N] → boolean

Arithmetic Operators +, -,

, /

The arithmetic operators + (addition), - (unary negation or binary subtraction),

(multiplica-

tion) and / (division) have the following signature:

+, -,

, / : integer * integer → integer

: unsigned word[N] * unsigned word[N] → unsigned word[N]

: signed word[N] * signed word[N] → signed word[N]

- (unary) : integer → integer

: unsigned word[N] → unsigned word[N]

: signed word[N] → signed word[N]

Before checking the expression for being correctly typed, the implicit type conversion can be

applied to one of the operands. If the operators are applied to unsigned word[N] or signed

word[N] type, then the operations are performed modulo 2

The result of the / operator is the quotient from the division of the ﬁrst operand by the

second. The result of the / operator is the algebraic quotient with any fractional part discarded

(this is often called “truncation towards zero”). If the quotient a/b is representable, the expres-

sion (a/b)

b + (a mod b) shall equal a. If the value of the second operand is zero, the

behavior is undeﬁned and an error is thrown by NUSMV. The semantics is equivalent to the

corresponding one of C/C++ languages.

In the versions of NUSMV prior to 2.4.0 the semantics of division was different. See page

16 for more detail.

Remainder Operator mod

The result of the mod operator is the algebraic remainder of the division. If the value of the

second operand is zero, the behavior is undeﬁned and an error is thrown by NUSMV.

The signature of the remainder operator is:

mod : integer * integer → integer

: unsigned word[N] * unsigned word[N] → unsigned word[N]

: signed word[N] * signed word[N] → signed word[N]

The semantics of mod operator is equivalent to the corresponding operator % of C/C++ lan-

guages. Thus if the quotient a/b is representable, the expression (a/b)

b + (a mod b)

shall equal a.

Note: in older versions of NUSMV (priori 2.4.0) the semantics of quotient and remainder

were different. Having the division and remainder operators / and mod be of the current, i.e.

C/C++’s, semantics the older semantics of division was given by the formula:

IF (a mod b < 0) THEN (a / b − 1) ELSE (a / b)

and the semantics of remainder operator was given by the formula:

IF (a mod b < 0) THEN (a mod b + b) ELSE (a mod b)

Note that in both versions the equation (a/b)

b + (a mod b) = a holds. For example,

in the current version of NuSMV the following holds:

7/5 = 1 7 mod 5 = 2

-7/5 = -1 -7 mod 5 = -2

7/-5=-1 7 mod -5 = 2

-7/-5=1 -7 mod -5 = -2

whereas in the older versions on NuSMV the equations were

7/5 = 1 7 mod 5 = 2

-7/5 = -2 -7 mod 5 = 3

7/-5=-1 7 mod -5 = 2

-7/-5=0 -7 mod -5 = -7

When supplied, the command line option -old div op switches the semantics of division and

remainder to the old one.

Note: semantics of modulo operator can be obtained from the remainder operator by exploit-

ing the equivalence:

(n modulo M) ≡ ((n mod M) + M) mod M

Where mod is the remainder operator.

Shift Operators <<, >>

The signature of the shift operators is:

<<, >> : unsigned word[N] * integer → unsigned word[N]

: signed word[N] * integer → signed word[N]

: unsigned word[N] * unsigned word[M] → unsigned word[N]

: signed word[N] * unsigned word[M] → signed word[N]

Before checking the expression for being correctly typed, the right operand can be implicitly

converted from boolean to integer type.

Left shift << (right shift >>) operation shifts to the left (right) the bits of the left operand by

the number speciﬁed in the right operand. A shift by N bits is equivalent to N shifts by 1 bit. A

bit shifted behind the word bound is lost. During shifting a word is padded with zeros with the

exception of the right shift for signed word[•], in which case a word is padded with its highest

bit. For instance,

0ub4 0101 << 2 is equal to 0sb3 1011 >> 2 is equal to

0ub4 0100 << 1 is equal to 0sb3 1110 >> 1 is equal to

0ub4

1000 << 0 is equal to 0sb3 1111 >> 0 is equal to

0ub4 1000 and 0sb3 1111

It has to be remarked that the shifting requires the right operand to be greater or equal to zero

and less then or equal to the width of the word it is applied to. NUSMV raises an error if a shift

is attempted that does not satisfy this restriction.

Index Subscript Operator [ ]

The index subscript operator extracts one element of an array in the typical fashion. On the

left of [] there has to be an expression of array type. The index expression in the brackets

has to be an expression of integer or word[•] type with value greater or equal to lower bound

and less or equal to the upper bound of the array. The signature of the index subscript operator is:

[ ] : array N..M of subtype * word[N] → subtype

: array N..M of subtype * integer → subtype

For example, for below declarations

MODULE main

VAR a : array -1 .. 4 of array 1 .. 2 of boolean;

DEFINE d := [[12, 4], [-1,2]];

VAR r : 0..1;

expressions a[-1], a[0][r+1] and d[r][1] are valid whereas a[0], a[0][r] and

d[0][r-1] will cause out of bound error.

Bit Selection Operator [ : ]

The bit selection operator extracts consecutive bits from a unsigned word[•] or signed word[•]

expression, resulting in a new unsigned word[•] expression. This operation always decreases

the width of a word or leaves it intact. The expressions in the brackets have to be integer

constants which specify the high and low bound. The high bound must be greater than or equal

to the low bound. The bits count from 0. The result of the operations is unsigned word[•]

value consisting of the consecutive bits beginning from the high bound of the operand down

to, and including, the low bound bit. For example, 0sb7 1011001[4:1] extracts bits 1 through 4

(including 1st and 4th bits) and is equal to 0ub4 1100. 0ub3 101[0:0] extracts bit number 0 and

is equal to 0ub1 1.

The signature of the bit selection operator is:

[ : ] : unsigned word[N] * integer

* integer

→ unsigned word[integer

− integer

+ 1]

: signed word[N] * integer

* integer

→ unsigned word[integer

− integer

+ 1]

where 0 ≤ integer

≤ integer

< N

Word Concatenation Operator ::

The concatenation operator joins two words (unsigned word[•] or signed word[•] or both)

together to create a larger unsigned word[•] type. The operator itself is two colons (::), and

its signature is as follows:

:: : word[M] * word[N] → unsigned word[M+N]

See 2.3.3) for array deﬁnes and 2.3.1 for array variables.

where word[N] is unsigned word[N] or signed word[N]. The left-hand operand will make up

the upper bits of the new word, and the right-hand operand will make up the lower bits. The

result is always unsigned word[•]. For example, given the two words w1 := 0ub4 1101

and w2 := 0sb2 00, the result of w1::w2 is 0ub6 110100.

Word sizeof Operator

sizeof operator provides a very simple way for retrieving the width of a word. The behavior

of this operator can be described as follows:

let w be a word[N] : sizeof (w) returns N.

The signature of the operator is:

sizeof : unsigned word[•] → integer

: signed word[•] → integer

Extend Word Conversions

extend operator increases the width of a word by attaching additional bits on the left. If the

provided word is unsigned then zeros are added, otherwise if the word is signed the highest (sing)

bit is repeated corresponding number of times.

The signature of the operator is:

extend : unsigned word[N] * integer → unsigned word[N+integer ]

: signed word[N] * integer → signed word[N+integer ]

For example:

extend(0ub3 101, 2) = 0ub5 00101

extend(0sb3 101, 2) = 0sb5 11101

extend(0sb3 011, 2) = 0sb5 00011

Note that the right operand of extend has to be an integer constant greater or equal to zero.

Resize Word Conversions

resize operator provides a more comfortable way of changing the width of a word. The

behavior of this operator can be described as follows:

let w be a M bits unsigned word[•] and N be the required width: if M = N, w is returned

unmodiﬁed; if N is less than M, bits in the range [N-1:0] are extracted from w; if N is greater

than M, w is extended of (N - M) bits up to required width, padding with zeroes.

let w be a M bits signed word[•] and N be the required width: if M = N, w is returned

unmodiﬁed; if N is less than M, bits in the range [N-2:0] are extracted from w, while N-1-ith bit

is forced to preserve the value of the original sign bit of w (M-1-ith bit); if N is greater than M,

w is extended of (N - M) bits up to required width, extending sign bit.

The signature of the operator is:

resize : unsigned word[•] * integer → unsigned word[integer ]

: signed word[•] * integer → signed word[integer ]

Set Expressions

The set expression is an expression deﬁning a set of boolean, integer and symbolic enum

values. A set expression can be created with the union operator. For example, 1 union 0

speciﬁes the set of values 1 and 0. One or both of the operands of union can be sets. In this

case, union returns a union of these sets. For example, expression (1 union 0) union

-3 speciﬁes the set of values 1, 0 and -3.

Note that there cannot be a set of sets in NuSMV. Sets can contain only singleton values, but

not other sets.

The signature of the union operator is:

union : boolean set * boolean set → boolean set

: integer set * integer set → integer set

: symbolic set * symbolic set → symbolic set

: integers-and-symbolic set * integers-and-symbolic set

→ integers-and-symbolic set

Before checking the expression for being correctly typed, if it is possible, both operands are

converted to their counterpart set types

, which virtually means converting individual values

to singleton sets. Then both operands are implicitly converted to a minimal type that covers

both operands. If after these manipulations the operands do not satisfy the signature of union

operator, an error is raised by NUSMV.

There is also another way to write a set expression by enumerating all its values between

curly brackets. The syntactic rule for the values in curly brackets is:

set_body_expr ::

basic_expr

| set_body_expr , basic_expr

Enumerating values in curly brackets is semantically equivalent to writing them connected

by union operators. For example, expression {exp1, exp2, exp3} is equivalent to exp1

union exp2 union exp3. Note that according to the semantics of union operator, ex-

pression {{1, 2}, {3, 4}} is equivalent to {1, 2, 3, 4}, i.e. there is no actually set of

sets.

Yet another way to write a set expression is to use the binary operator .. (<TWO DOTS>).

The two operands have both to be expressions that evaluate to constants integer numbers, and

may contain names of deﬁnes and module formal parameters. For example, -1 - P1 .. 5

+ D1, where P1 refers to a module formal parameter, and D1 refers to a deﬁne. Both P1 and

D1 have to be statically evaluable to integer constants.

This is just a shorthand for a set expression containing the list of integer

numbers included between the lower and the upper bound. For example, -1..5 and

{-1,0,1,2,3,4,5} are equivalent. Note that the evaluated number on the left from the

two dots must be less than or equal to the evaluated number on the right.

Set expressions can be used only as operands of union and in operations, as the right

operand of case and as the second and the third operand of (• ? • : •) expressions and

assignments. In all other places the use of set expressions is prohibited.

Inclusion Operator in

The inclusion operator ‘in’ tests the left operand for being a subset of the right operand. If either

operand is a number or a symbolic value instead of a set, it is coerced to a singleton set.

The signature of the in operator is:

in : boolean set * boolean set → boolean

: integer set * integer set → boolean

: symbolic set * symbolic set → boolean

: integers-and-symbolic set * integers-and-symbolic set → boolean

Similar to union operation, before checking the expression for being correctly typed, if it is

See 2.1.6 for more information about the set types and their counterpart types

剩余144页未读，继续阅读

weixin_38702110

粉丝: 5
资源: 941

NuSMV2.6模型检查器用户手册与技术概述

NuSMV模型检测器

NuSMV模型检测工具安装包

关于电梯的简单NuSMV模型

nusmv的安装和使用

handbook of model checking

nusmv中如何将可达状态打印出来

pdr的python代码

SMV 模型检测

基于Matlab面板版的卡尔曼小球运动跟踪[Matlab面板版].zip

最新资源