2

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

ltl p0 {p X q}

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

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

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

4

1 回答 1

4

LTL公式的一般结构

如果某个语句ptrue处于状态i，那么某个语句q处于下一个状态，即状态i+1true

是以下一个：

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

该公式p -> X q通过以下方式验证

  • 任何状态S i stp在S ifalse
  • 任何状态S i stp都true在S iq中并且true在S i+1中，其中S i+1是当前正在评估的执行路径中S i的后继状态

全局运算符[]需要使模型检查器验证条件是否p -> X q适用于执行路径中的任何状态。如果您省略它，则p -> X q仅检查该属性的初始状态，这在99.99%的情况下不是您想要的。

例子

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

我们要检查的属性是，每当计数器达到给定的检查点状态并且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) }。但是，标签在具有 结构的公式的上下文中经常使用[] (p -> X g)，所以我认为在我的示例中插入一个带有一些空的借口的标签会很有用。

  • 我通常更喜欢较弱的F odd条件而不是更强的语句X X odd，除非由于要验证的属性的性质而不可能/不建议这样做。事实上，对于Spin来说，一眼就能猜出从一个语句到另一个语句发生了多少次转换，因为AFAIK模型通常会经历许多优化以相互删除/合并状态。

于 2017-08-01T08:44:15.567 回答