verification - 永远不要声称在 promela 模型中不起作用

Question

考虑这个简单的 PROMELA 模型：

#define p (x!=4)

int x = 0;

init {
    do
    :: x < 10 ->
        x++;
    od
}

我想用这个简单的声明来验证这个模型，它是使用 spin -f 生成的：

never {    /* []p */
accept_init:
T0_init:
    do
    :: ((p)) -> goto T0_init
    od;
}

但是，使用验证

spin -a model.pml
cc -o pan pan.c
./pan

没有结果。尝试 -a 选项也不会产生结果。任何随机模拟都表明，在某些时候显然 p 是错误的，那么尽管我用自旋生成了它，为什么 never 声明不起作用？

我错过了一些基本的东西吗？

score 1 · Accepted Answer

将声明放入源代码（例如 check.pml）

int x = 0;

init {
    do
    :: x < 10 ->
        x++;
    od
}

ltl  { [] (x != 4) }

然后

spin -a check.pml
cc     pan.c   -o pan
./pan -a

这给了

pan:1: assertion violated  !( !((x!=4))) (at depth 16)
pan: wrote check.pml.trail

你可以用

./pan -r -v

恕我直言，使用额外的工具从索赔中构建自动机非常不方便并且经常令人困惑。

score 1 · Accepted Answer

如果您想检查[]p，您将需要never为![]p.

要将 LTL 公式转换为从不声明，我们必须首先考虑该公式是否表达了积极或消极的属性。正属性表示我们希望系统具有的良好行为。负属性表示我们声称系统没有的不良行为。从不声明通常仅用于形式化负面属性（不应该发生的行为），这意味着在将正面属性转换为声明之前必须对其进行否定。

2 回答 2