在 SPIN ltl 公式中使用 ne(X)t 运算符

Question

我正在尝试定义一个在 SPIN 中使用 ne(X)t 运算符的 ltl 公式。我的问题与 this 问题非常相似。我有一个状态机，我想验证如果某些语句 p 在 state0 中为真，那么某些语句 q 在下一个状态中为真, 状态 1。 ltl 公式如下所示：

ltl p0 {p X q}

当我尝试使用 spin -a test.pml 生成验证器时，出现以下错误：

spin: test.pml:20, Error: syntax error saw 'X'

我使用 -DNXT 标志编译了 SPIN（如 this 建议的那样）。我知道 ne(X)t 运算符无法在启用偏序减少的情况下进行测试。我发现禁用偏序减少的唯一方法是在编译验证程序时使用 -DNOREDUCE 标志。但是，我什至无法首先生成验证器 (pan.c)。

Answer 1

LTL 公式的一般结构

if some statement p is true in state_i, then some statement q is true in the next state, state_i+1

是下面这个：

ltl p0 { [] (p -> X q) }

公式p -> X q由

验证

任何状态 S_i s.t。 p 是 false 在 S_i
任何状态 S_i s.t。 p 是 S_i 中的 true 并且 q 是 [=63 中的 true =]S_i+1，其中S_i+1为后继当前正在评估的执行路径中的 S_i

需要 globally 运算符 [] 才能使 Model Checker 验证条件 p -> X q 是否成立对于执行路径中的任何状态。如果你省略它，那么属性 p -> X q 只会被检查初始状态，这在 99.99% 的情况下不是你想要的。

示例

在以下模型中，如果 cc 是偶数，则进程 counter 将其加一，否则进程终止或将 cc 减一以不确定的方式。

我们要检查的属性是，每当 counter 达到给定的 checkpoint 状态并且 cc 是偶数，正好经过 2 次转换后 cc 是奇数。

byte cc = 0;

active proctype counter()
{
checkpoint:
    do
        :: cc % 2 == 0 -> cc++;
        :: else ->
            if
                :: cc--;
                :: break;
            fi;
    od;
}

#define even ( cc % 2 == 0 )
#define odd  ( cc % 2 == 1 )

ltl p0 { [] ( (counter[0]@checkpoint & even) -> X X odd) }

ltl 属性 p0 已验证：

~$ spin -a test.pml
~$ gcc -DNXT -DNOREDUCE -o run pan.c
~$ ./run -a

(Spin Version 6.4.3 -- 16 December 2014)

Full statespace search for:
    never claim             + (p0)
    assertion violations    + (if within scope of claim)
    acceptance   cycles     + (fairness disabled)
    invalid end states  - (disabled by never claim)

State-vector 28 byte, depth reached 11, errors: 0
        8 states, stored (10 visited)
        2 states, matched
       12 transitions (= visited+matched)
        0 atomic steps
hash conflicts:         0 (resolved)

Stats on memory usage (in Megabytes):
    0.000   equivalent memory usage for states (stored*(State-vector + overhead))
    0.289   actual memory usage for states
  128.000   memory used for hash table (-w24)
    0.534   memory used for DFS stack (-m10000)
  128.730   total actual memory usage


unreached in proctype counter
    (0 of 11 states)
unreached in claim p0
    _spin_nvr.tmp:16, state 20, "-end-"
    (1 of 20 states)

pan: elapsed time 0 seconds

注意事项：

在此示例中，标签 checkpoint: 的使用完全是可选的。使用 ltl 公式 { [] ( even -> X X odd) } 可以获得相同的结果。然而，labels 在具有结构 [] (p -> X g) 的公式的上下文中使用得非常频繁，因此我认为在我的示例中使用一些空的借口推一个是有用的。
我通常更喜欢较弱的 F odd 条件而不是更强的语句 X X odd，除非由于 [= 的性质，那不是 possible/advisable 133=] 正在验证中。事实上，使用 Spin 很难一眼就猜出从一个语句到另一个语句发生了多少次转换，因为 AFAIK 模型通常会经过多次优化以达到 remove/merge 状态。

在 SPIN ltl 公式中使用 ne(X)t 运算符

Using the ne(X)t operator in a SPIN ltl formula

model-checking

spin

promela