随着信息和通信技术的广泛应用，软件的正确性检查变得非常重要。系统的可靠性取决于硬件和软件。

模式检查的优势：

• 快速
• 无需严格证明
• 逻辑可以很容易地表达许多并发属性

SPIN系统

SPIN（Simple Promela INterpreter）是一种验证并发系统正确性的工具，是最先进的模型检查器之一。它使用Promela语言表示并发系统

Promela语言

ProMeLa（Protocol/Process Meta Language）允许以动态方式创建流程，通过消息通道实现同步/异步通信。该语言的语法与C相似。

数据类型

数组：

1

byte[12], bit[100]

结构体：

1
2
3
4

typedef MyStruct {
    short Field1;
    short Field2;
};

过程

要定义流程，我们需要指定：流程名称、形式参数、局部变量声明和语句。

1
2
3
4
5
6

proctype you_run(byte x) {
    printf("Pid = %d, x = %d\n", _pid, x);
}

// 请注意，局部变量_pid是一个预定义的变量
// 它记录了当前流程的实例化编号，通常为非负整数

实例化一个过程：

1
2
3
4

init {
    run you_run(0);
    run you_run(1)
}

特别地，活动进程是自动创建的实例化的进程。在活动进程中，不能使用任何参数：

1
2
3

active [2] proctype you_run() {
    printf("my Pid is: %d\n", _pid)
}

如果要创建的活动进程数量为1，则可以略去[]

消息通道

定义

1

chan cname = ['const' ] of { typename, typename, ..., typename}

例如：chan ch = [16] of {short, byte, bit}

const用于指定通道的大小，上限为255。特别地，对于const=0的情况，通道实现的通信为同步通信

发送和接收消息

1
2
3

// 发送消息
// 参数的类型必须与声明中的类型相同
cname ! msg1, msg1, msg3

如果通道未满，则该语句可执行（在这种情况下，消息将附加到通道上）；否则，该语句将被阻塞。

1
2
3

// 接收消息
// 参数的类型必须与声明中的类型相同
cname ? e1, e2, e3

如果通道不为空，则该语句可执行（在这种情况下，消息将从通道中删除）；否则，该语句将被阻塞（等待正确的消息）。如果 $e_i$ 是一个变量，则消息中的值将被分配给 $e_i$。

原子语句

在实例化流程中，执行序列stat1; stat2; ...，执行状态可能会被打破。为了避免这种情况，我们可以使用原子语句序列：

1

atomic{stat1; stat2; ...; statk}

上述序列将作为一个不可分割的步骤执行，除非序列中的某些语句被阻塞。一旦被阻止的语句变得可执行，序列中的其余语句将继续执行。

选择语句

1
2
3
4
5
6

if
    :: guard_1 -> option_1
    :: guard_2 -> option_2
    ...
    :: guard_n -> option_n
fi

上面的每个guard_i都被称为option_i的卫式。

1. 如果没有可满足的卫式，则阻塞选择语句，直到某些卫式可用。
2. 如果同时有多个可满足的卫式，则将随机选择一个选项执行。
3. 如果guard_i是重言式，我们将忽略guarded_i ->

循环语句

1
2
3
4
5
6

do
    :: guard_1 -> option_1
    :: guard_2 -> option_2
    ...
    :: guard_n -> option_n
od

重复语句类似于选择语句，但它会重复执行，直到执行break语句或goto-jump将控制权转移到循环之外。

模式检查

给定一个结构 $M$ 和一个公式 $\varphi$，如果 $M \vDash \varphi$ 成立，则称 $M$ 是 $\varphi$ 的模型。

证明 $M \vDash \varphi$ 的过程就称作模式检查。

许多问题都可以用模式检查描述，例如：

基本时态

记符号 $p$ 为一个原子命题，例如DeviceEnabled，则有：

它具有如下性质：

• 否定律：$\lnot \text{X} \varphi \equiv \text{X} \lnot \varphi$，$\lnot \text{G} \varphi \equiv \text{F} \lnot \varphi$，$\lnot \text{F} \varphi \equiv \text{G} \lnot \varphi$
• 分配律：$\text{G}(\varphi \land \psi) \equiv \text{G} \varphi \land \text{G} \psi$，$\text{F}(\varphi \lor \psi) \equiv \text{F} \varphi \lor \text{F} \psi$
• 互定义：$\text{F} \varphi \equiv \lnot \text{G} \lnot \varphi$，$\text{G} \varphi \equiv \lnot \text{F} \lnot \varphi$，$\text{F} \varphi \equiv (p \lor \lnot p) \text{U} \varphi$
• 幂等律：$\text{F} \text{F} \varphi \equiv \text{F} \varphi$，$\text{G} \text{G} \varphi \equiv \text{G} \varphi$
• $\text{G} \text{F} \text{G} \varphi \equiv \text{F} \text{G} \varphi$，$\text{F} \text{G} \text{F} \varphi \equiv \text{G} \text{F} \varphi$，$\text{G}(\text{F} \varphi \lor \text{F} \psi) \equiv \text{G} \text{F} \varphi \lor \text{G} \text{F} \psi$

线性时序逻辑

设Atom为命题变量集。为方便起见，设 $p, q, r, \cdots$（可能带有下标）表示命题变量。LTL则可以用如下的形式表示：

其中 $p$ 的范围为命题变量，$\varphi$ 的范围为LTL公式。

迁移系统

迁移系统定义为一个元组 $M = (S, \rightarrow, L)$，其中：

• $S$ 是一个非空集，由一组状态组成。
• $\rightarrow \subseteq S \times S$ 是一个转换关系。
• $L: S \rightarrow P$ 是一个赋值函数。

例如，在如下的弹簧系统中，有

• $S = \{s_1, s_2, s_3\}$
• $\rightarrow = \{(s_1, s_2), (s_2, s_1), (s_2, s_3), (s_3, s_3)\}$
• $L(s_1) = \oslash$，$L(s_2) = {\text{extended}}$，$L(s_3) = \{\text{extended}, \text{malfunction}\}$

路径

设 $M = (S, \rightarrow, L)$ 是一个迁移系统，则 $M$ 的一条路径是一个无限的序列 $\pi = (s_1, s_2, s_3, \cdots)$，其中

在上述的弹簧示例中，有如下路径：

满足关系

设 $M = (S, \rightarrow, L)$ 是一个迁移系统，$M$ 的一条路径为 $\pi$，则如果 $\pi \vDash^i \varphi$，则称LTL公式 $\varphi$ 在第 $i$ 阶段由 $\pi$（在 $M$ 下）满足。

常见的满足关系如下：

• $\pi \vDash^i p$ 当且仅当 $p \in L(\pi[i])$
• $\pi \vDash^i \varphi \land \psi$ 当且仅当 $\pi \vDash^i \varphi \land \pi \vDash^i \psi$
• $\pi \vDash^i \varphi \lor \psi$ 当且仅当 $\pi \vDash^i \varphi \lor \pi \vDash^i \psi$
• $\pi \vDash^i \varphi \Rightarrow \psi$ 当且仅当 $\pi \vDash^i \varphi \Rightarrow \pi \vDash^i \psi$
• $\pi \vDash^i \lnot \varphi$ 当且仅当 $\pi \nvDash^i \varphi$
• $\pi \vDash^i \text{X} \varphi$ 当且仅当 $\pi \vDash^{i+1} \varphi$
• $\pi \vDash^i \text{F} \varphi$ 当且仅当 $\exist\ j \geqslant i$，使得 $\pi \vDash^j \varphi$
• $\pi \vDash^i \text{G} \varphi$ 当且仅当 $\forall\ j \geqslant i$，都有 $\pi \vDash^j \varphi$
• $\pi \vDash^i \varphi \text{U} \psi$ 当且仅当 $\exist\ j \geqslant i$，使得 $\pi \vDash^j \psi$ 并且 $\forall\ k \in \{i,i+1,\cdots,j-1\}$，都有 $\pi \vDash^k \varphi$

特别的，

• 如果 $\pi \vDash^1 \varphi$，则可记为 $\pi \vDash \varphi$。
• 设 $s \in S$，若 $M$ 的所有路径均满足 $\pi[1] = s$，则可记为 $M,s \vDash \varphi$
• 若 $M$ 的所有路径均满足 $\pi \vDash \varphi$，则可记为 $M \vDash \varphi$。此时称 $M$ 为 $\varphi$ 的一个模式。

对于两个LTL公式 $\varphi$ 和 $\psi$，若它们在同一个迁移系统 $M$ 下的所有路径 $\pi$ 的所有阶段 $i$ 均有

则可记作 $\varphi \equiv \psi$

对于上述的弹簧系统，则有：

• $\pi_1 \vDash^1 \text{X} \text{extended}$，即在路径1的条件下第1个迁移后的第2个状态 $s_2$ 为 $\text{extended}$
• $\pi_1 \vDash^1 \text{F} \text{malfunction}$，即在路径1的条件下第1个迁移后的未来某个时刻为 $\text{malfunction}$
• $\pi_2 \vDash^1 \lnot \text{F} \text{malfunction}$，即在路径2的条件下第1个迁移后未来的所有时刻都不会出现 $\text{malfunction}$，等价于 $\pi_2 \vDash^1 \text{G} \lnot \text{malfunction}$