有限状态机建模语言：NuSMV与Promela详解

1. NuSMV中的有限状态机

在NuSMV中，过渡谓词在变量更新相互高度依赖时非常有用。例如，过渡谓词：

TRANS
next(x) + 2*next(y) + 3*next(z) = (x + 2*y + 3*z) mod 7

它简洁地定义了变量x、y和z如何随时间变化以及它们之间的关系，而这在 ASSIGN 子句中无法直接表达。

在使用过渡谓词定义模块时，用户需要注意以下两点：
- 初始状态谓词至少要被一个状态满足。
- 过渡关系必须是左全的。

若不满足这两个条件，可能会导致逻辑荒谬。幸运的是，NuSMV提供了检查这些条件是否满足的选项，但用户需要记得使用该选项。

1.1 多模块组合

NuSMV模型通常有多个模块，它们之间会有交互。将模型构建为多个模块的组合可以提高模型的可维护性和可理解性，并且通常能反映现实系统中多个代理或实体的实际交互。模块可以被实例化任意次数。

每个NuSMV系统模型都应该有一个主模块。例如，要分析之前的计数器模块，需要在主模块中实例化计数器模块，并定义一种机制来定期重置计数器。

在组合模块时，可以使用模块参数将信息从一个模块传递到另一个模块。

假设有一个简单的 increase 模块，当布尔参数 flag 的值为 TRUE 时，它会将其值（模某个常量值 mx + 1 ，作为参数传递）增加。通过将上限作为参数提供，可以创建具有不同上限的 increase 模块的多个实例。

可以将 increase 模块与计数器组合，让它统计计数器达到状态2的次数。为了在模块之间传递信息，可以编写任意表达式，只要将模块 m 的变量 v 表示为 m.v 。

以下是一个主模块的定义示例，其中创建了计数器和 increase 模块的各一个实例，并设置为 increase 实例统计计数器实例达到状态2的次数，并且当 increase 实例达到值 mx 时，通知计数器实例重置计数器：

// 这里可以根据实际情况补充主模块的代码示例

模块实例之间的依赖关系在模块实例级别可能看起来是循环的，但在单个变量级别并非如此，而NuSMV实际上检查的是单个变量级别，不允许出现循环依赖。

组合建模的一个优点是可维护性。例如，如果更改计数器模块的定义，理想情况下 increase 模块不需要更改。但当前的主模块定义可能无法完全实现这一点。可以通过在计数器模块中声明一个额外的布尔变量，或者使用 DEFINE 声明来解决这个问题。

变量在 DEFINE 子句中声明的不是实际的状态变量，而是可以在每个状态中使用实际状态变量计算的表达式。这在后续的属性模型检查中也会有很大帮助。

模块是同步执行的，即每个时间点，所有模块都会同步进行过渡步骤。这意味着在这个特定的示例模型中：
- increase 模块不会错过计数器状态等于2的情况。
- 状态2不会被重复计数。

在早期版本的NuSMV中，也支持异步组合，但在当前版本中已被弃用。如果要在NuSMV中对异步系统进行建模，需要在更高层次上解决，即模型需要有明确的控制变量来编码模块何时可以改变状态，何时应该保持不变。

2. Promela中的有限状态机

Promela是另一种用于描述有限状态机的高级语言。与NuSMV不同，Promela更基于诸如C之类的命令式编程语言。为了支持并行进程系统的建模，在通常的命令式编程概念（如赋值和顺序组合）之上，添加了非确定性、并行性以及通过同步和异步通道进行通信等概念。

2.1 定义Promela进程

• 模型状态 ：与NuSMV类似，进程的状态通过变量来建模。变量可以在进程内部声明，也可以全局声明，全局声明的变量可被模型中的所有进程访问。变量必须有类型，Promela支持的原始变量类型如下表所示：

名称	声明	值
Bit	bit v	{0, 1}
Boolean	bool v	{false, true}
Byte	byte v	[0, 28 - 1]
Short	short v	[-215, 215 - 1]
Integer	int v	[-231, 231 + 1]
Unsigned integer	unsigned v: n	[0, 2n - 1]
Enumeration	mtype v	定义的mtype的值
Array of type T	T v[n]	所有n个元素的T范围

除了原始类型，用户还可以通过定义由现有类型变量组成的结构体来定义自己的新类型。例如，定义一个 car 类型：

// 定义car类型
mtype:car = {is_driving: bool, nr_occupants: byte};

可以声明该类型的实例 car c ，并通过 c.is_driving 和 c.nr_occupants 来引用其成员。

进程的状态除了由局部变量的值定义外，还由当前执行点定义。在Promela中，进程行为的定义更类似于程序代码，指令的执行有时会被暂停，因此存在当前执行点的概念，它标识了执行在当前状态下到达的进程定义位置。

以下是一个带有重置选项的模3计数器的Promela模型示例：

// 声明枚举类型
mtype = {zero, one, two};
// 声明全局布尔变量
bool reset;

proctype counter() {
    // 声明并初始化局部变量
    mtype state = zero;
    do
    :: reset -> state = zero;
    ::!reset ->
        if
        :: state == zero -> state = one;
        :: state == one -> state = two;
        :: state == two -> state = zero;
        fi;
    od;
}

• 下一状态函数 ：在Promela进程的主体中，描述了进程如何改变状态。声明的变量可以立即被赋予初始值。虽然不像NuSMV那样有专门的部分来进行初始化，但建议在声明变量时赋予初始值，以避免不必要的状态。如果没有为变量提供初始值，它将被赋予默认初始值，整数类型变量为0，布尔类型变量为 false 。

Promela进程的结构和控制流定义比NuSMV模块更灵活。与NuSMV的 case 段概念最接近的是Promela中的重复构造（ do 构造），但在进程中使用它不是必需的。

重复构造中列出了有限数量的执行选项，每个选项由一系列语句组成。以下是重复构造的一般结构：

do
:: st-i-0; st-i-1;...; st-i-k;
:: st-j-0; st-j-1;...; st-j-l;
...
od;

语句可以是赋值、表达式或条件语句、特殊的 skip 语句（空语句）或 printf 语句。表达式可能引用进程局部和全局变量。

一般来说，语句并不总是可执行的。赋值、 skip 语句和 printf 语句总是可执行的，但表达式只有在计算结果为 true 时才是可执行的。

重复构造中的一个 do 选项只有在其序列中的第一个语句可执行时才是可执行的。如果选择了一个可执行的选项进行执行，但执行到达该选项序列中的另一个不可执行的语句，则执行将在该语句处阻塞，直到该语句变为可执行。

例如，以下是一个在执行过程中会阻塞的Promela进程示例：

proctype blocked() {
    int x = 0;
    int y;
    do
    :: y = 1;
    :: x == y -> printf("This will never be printed\n");
    od;
}

重复构造只有在至少有一个选项可执行时才是可执行的。Promela的重复构造与NuSMV的 case 段的一个重要区别是，前者中选项的顺序无关紧要。但 else 条件语句是个例外，当所有其他选项都不可执行时，以 else 开头的选项将被执行，并且在一个重复构造中最多只能有一个这样的选项。

在Promela中，可以使用 break 关键字跳出重复构造。例如，以下是一个创建循环的示例：

int i = 0;
bool b[5];
do
:: i < 5 -> b[i] = true; i = i + 1;
:: else -> break;
od;

与NuSMV不同，Spin不会将值溢出解释为错误。在分析过程中发生溢出时，会打印警告消息，但分析不会终止，由用户决定是否应避免溢出。此外，Spin不检查过渡关系是否完整，但会检查是否存在死锁，即执行过程中没有更多可执行过渡的系统状态。而NuSMV模型由于过渡关系的左全性要求，定义上是无死锁的。

可以使用不同的方式对模3计数器进行建模，例如使用整数变量：

// 声明全局布尔变量
bool reset;
// 声明局部变量
unsigned val: 2;

proctype counter() {
    val = 0;
    do
    :: reset -> val = 0;
    ::!reset -> val = (val + 1) % 3;
    od;
}

Promela还支持非确定性。例如，在重复或选择构造中，如果多个选项都可执行，将非确定性地选择其中一个进行执行。可以利用这一点来非确定性地为变量赋值，例如：

byte v;
do
:: v = 1;
:: v = 2;
:: v = 3;
od;

可以将模3计数器扩展为支持非确定性重置。

综上所述，NuSMV和Promela在有限状态机建模方面各有特点。NuSMV更侧重于模块的组合和过渡关系的定义，而Promela则更基于命令式编程，支持并行进程和非确定性。在实际应用中，可以根据具体需求选择合适的建模语言。

3. NuSMV与Promela的对比分析

NuSMV和Promela作为两种不同的有限状态机建模语言，在多个方面存在显著差异，下面将从几个关键维度进行对比分析。

3.1 语言基础与风格

• NuSMV ：基于声明式的逻辑描述风格，更强调通过谓词来定义系统的状态和状态之间的转换关系。例如使用 INIT 和 TRANS 子句来明确初始状态和状态转移规则，这种方式使得模型的逻辑结构清晰，易于从数学逻辑的角度进行理解和分析。
• Promela ：基于命令式编程语言，类似于C语言。它通过程序代码的方式来描述进程的行为，包含赋值、条件判断、循环等常见的编程结构，更符合程序员的编程习惯，对于熟悉命令式编程的人来说更容易上手。

3.2 变量与状态表示

• NuSMV ：变量类型相对较为基础，在定义变量时需要明确其类型和取值范围。在多模块组合时，变量的使用和传递需要遵循一定的规则，以确保模块之间的交互逻辑正确。
• Promela ：除了支持常见的基本类型外，还允许用户自定义类型，如结构体。变量可以在进程内部或全局声明，并且可以通过不同的方式进行初始化。进程的状态不仅由变量的值决定，还与当前的执行点相关，这种表示方式更加灵活，但也增加了一定的复杂度。

3.3 状态转移与控制流

• NuSMV ：使用过渡谓词来定义状态转移，强调状态之间的逻辑关系。在多模块组合时，模块之间的交互通过参数传递和逻辑表达式来实现，并且要求过渡关系是左全的，以确保模型的正确性和完整性。
• Promela ：通过重复构造（ do 构造）和选择构造（ if-fi ）来描述状态转移和控制流。选项的执行是非确定性的，当多个选项都可执行时，会随机选择一个执行。这种非确定性的设计使得Promela能够更好地模拟并发系统中的不确定性。

3.4 模型检查与错误处理

• NuSMV ：会检查初始状态谓词是否被满足以及过渡关系的左全性，确保模型在定义上是无死锁的。如果不满足这些条件，可能会导致逻辑错误，但NuSMV提供了检查选项，帮助用户发现和解决问题。
• Promela ：Spin模型检查器不检查过渡关系的完整性，但会检查死锁情况。对于值溢出，Spin只会打印警告信息，不会终止分析，由用户自行决定是否需要处理。这种处理方式更加灵活，能够适应不同的应用场景。

以下是一个对比两者特点的表格：
| 对比维度 | NuSMV | Promela |
| ---- | ---- | ---- |
| 语言基础 | 声明式逻辑描述 | 命令式编程 |
| 变量类型 | 基础类型 | 支持自定义类型 |
| 状态转移 | 过渡谓词 | 重复和选择构造 |
| 模型检查 | 检查初始状态和过渡关系 | 检查死锁，处理值溢出 |

4. 实际应用场景与选择建议

在实际应用中，选择NuSMV还是Promela取决于具体的需求和场景。下面通过几个典型的应用场景来分析如何选择合适的建模语言。

4.1 同步系统建模

如果要建模的系统是同步执行的，各个模块之间的交互是确定性的，并且对模型的逻辑正确性和完整性要求较高，那么NuSMV是一个不错的选择。例如，对于一些硬件电路的建模，需要精确地定义初始状态和状态转移规则，以确保电路的功能正确。

以下是一个简单的同步系统建模流程：
1. 定义系统的模块结构，明确各个模块的功能和交互关系。
2. 使用 INIT 和 TRANS 子句定义每个模块的初始状态和过渡关系。
3. 在主模块中实例化各个子模块，并设置模块之间的参数传递和交互逻辑。
4. 使用NuSMV的检查选项确保模型的正确性。

// 示例代码：简单同步系统建模
MODULE main
VAR
    // 定义模块实例
    counter: counter_module;
    increase: increase_module;
ASSIGN
    // 设置模块之间的交互
    init(counter.reset) := false;
    init(increase.flag) := false;
    next(counter.reset) := increase.value == increase.mx;
    next(increase.flag) := counter.state == 2;

4.2 并发系统建模

对于并发系统，存在多个进程同时执行，并且进程之间的交互具有不确定性，Promela更适合这种场景。例如，对于通信协议的建模，需要考虑到消息的异步传递和进程的并发执行，Promela的非确定性和并发支持能够很好地模拟这些情况。

以下是一个并发系统建模的流程：
1. 定义各个进程的行为，包括变量的声明、初始值的设置和状态转移规则。
2. 使用重复构造和选择构造来描述进程的控制流和状态转移。
3. 考虑进程之间的通信方式，如同步和异步通道。
4. 使用Spin模型检查器进行死锁检查和属性验证。

// 示例代码：并发系统建模
bool reset;
proctype counter() {
    unsigned val: 2;
    val = 0;
    do
    :: reset -> val = 0;
    ::!reset -> val = (val + 1) % 3;
    od;
}

proctype monitor() {
    do
    :: counter.val == 2 -> // 处理计数器达到2的情况
    od;
}

4.3 模型的可维护性和扩展性

如果模型需要频繁修改和扩展，那么在选择建模语言时需要考虑其可维护性。NuSMV的模块组合方式使得模型的逻辑结构清晰，在修改某个模块时，只要保证模块之间的接口不变，对其他模块的影响较小。而Promela的命令式编程风格使得代码的可读性和可维护性在一定程度上依赖于程序员的编程习惯，但它的灵活性也使得模型的扩展更加方便。

以下是一个根据可维护性和扩展性选择建模语言的决策流程图：

graph TD;
    A[是否需要频繁修改模型?] -->|是| B[考虑语言的可维护性和扩展性];
    B --> C{更注重逻辑结构清晰?};
    C -->|是| D[选择NuSMV];
    C -->|否| E{更注重编程灵活性?};
    E -->|是| F[选择Promela];
    E -->|否| G[重新评估需求];
    A -->|否| H[根据其他需求选择语言];

5. 总结

NuSMV和Promela是两种强大的有限状态机建模语言，它们各自具有独特的特点和优势。NuSMV适用于对逻辑正确性和完整性要求较高的同步系统建模，通过声明式的方式定义系统的状态和转移关系；Promela则更适合并发系统建模，基于命令式编程风格，支持非确定性和并发执行。在实际应用中，需要根据具体的需求和场景来选择合适的建模语言，以确保模型能够准确地描述系统的行为，并方便进行后续的分析和验证。同时，了解两种语言的差异和特点，有助于在建模过程中充分发挥它们的优势，提高建模的效率和质量。