2

这是我在 Stack Exchange 上的第一个问题，所以如果有任何违反准则的内容，请告诉我。

我有一个用 Promela 为大学操作系统和并发系统课程编写的程序。有两个进程正在运行，它们增加了一个变量 n。我们的任务是编写流程，然后使用 Spin 中的验证工具来证明 n 可以取值 4。我已经阅读了所有命令行参数并搞砸了，但没有任何结果对我来说，“插入这个修饰符后跟一个变量名来检查所有可能的值”。

byte n;

proctype p()
{
    byte countp = 0;
    byte temp;
    do
    :: countp != 2 -> temp = n; temp = temp + 1; n = temp; countp = countp + 1;
    :: countp >= 2 -> break;
    od
}

proctype q()
{

    byte countq = 0;

    do
    :: countq != 2 -> n = n + 1; countq = countq + 1;
    :: countq >= 2 -> break;
    od
}

init
{
    run p();
    run q();
}
4

1 回答 1

2

有几种方法可以做到这一点，但作为一名教师，我更喜欢基于ltl的方法，因为至少它表明你了解如何使用它。

监控进程。

从概念上讲，这是迄今为止最简单的：您只需添加一个n != 4随时断言该断言的进程，然后检查该断言是否最终失败。

byte n;

active proctype p()
{
    byte countp = 0;
    byte temp;
    do
    :: countp != 2 -> temp = n; temp = temp + 1; n = temp; countp = countp + 1;
    :: countp >= 2 -> break;
    od
}

active proctype q()
{

    byte countq = 0;

    do
    :: countq != 2 -> n = n + 1; countq = countq + 1;
    :: countq >= 2 -> break;
    od
}

active proctype monitor()
{
    do
        :: true -> assert(n != 4);
    od;
}

注意：monitor 过程中的循环是完全没有必要的，但它使初学者更清楚其目的。

您可以使用以下一行来验证此程序：

~$ spin -search -bfs buggy_01.pml

Spin在零时间内找到了一个反例：

Depth=10 States=56 Transitions=84 Memory=128.195    
pan:1: assertion violated (n!=4) (at depth 19)
pan: wrote buggy_01.pml.trail

(Spin Version 6.4.3 -- 16 December 2014)
Warning: Search not completed
    + Breadth-First Search
    + Partial Order Reduction

Full statespace search for:
    never claim             - (none specified)
    assertion violations    +
    cycle checks            - (disabled by -DSAFETY)
    invalid end states      +

State-vector 28 byte, depth reached 19, errors: 1
      215 states, stored
             215 nominal states (stored-atomic)
      181 states, matched
      396 transitions (= stored+matched)
        0 atomic steps
hash conflicts:         0 (resolved)

Stats on memory usage (in Megabytes):
    0.011       equivalent memory usage for states (stored*(State-vector + overhead))
    0.290       actual memory usage for states
  128.000       memory used for hash table (-w24)
  128.195       total actual memory usage

pan: elapsed time 0 seconds

您实际上可以使用以下命令检查违反断言的执行跟踪：

~$ spin -t -p -g -l buggy_01.pml

这些选项具有以下含义：

  • -t: 重播.trailspin 生成的反例
  • -p: 打印所有语句
  • -g: 打印所有全局变量
  • -l: 打印所有局部变量

这是输出：

using statement merging
  1:    proc  2 (monitor:1) buggy_01.pml:27 (state 1)   [(1)]
  2:    proc  1 (q:1) buggy_01.pml:19 (state 1) [((countq!=2))]
  3:    proc  0 (p:1) buggy_01.pml:8 (state 1)  [((countp!=2))]
  4:    proc  1 (q:1) buggy_01.pml:19 (state 2) [n = (n+1)]
        n = 1
  5:    proc  1 (q:1) buggy_01.pml:19 (state 3) [countq = (countq+1)]
        q(1):countq = 1
  6:    proc  1 (q:1) buggy_01.pml:19 (state 1) [((countq!=2))]
  7:    proc  1 (q:1) buggy_01.pml:19 (state 2) [n = (n+1)]
        n = 2
  8:    proc  1 (q:1) buggy_01.pml:19 (state 3) [countq = (countq+1)]
        q(1):countq = 2
  9:    proc  1 (q:1) buggy_01.pml:20 (state 4) [((countq>=2))]
 10:    proc  0 (p:1) buggy_01.pml:8 (state 2)  [temp = n]
        p(0):temp = 2
 11:    proc  0 (p:1) buggy_01.pml:8 (state 3)  [temp = (temp+1)]
        p(0):temp = 3
 12:    proc  0 (p:1) buggy_01.pml:8 (state 4)  [n = temp]
        n = 3
 13:    proc  0 (p:1) buggy_01.pml:8 (state 5)  [countp = (countp+1)]
        p(0):countp = 1
 14:    proc  0 (p:1) buggy_01.pml:8 (state 1)  [((countp!=2))]
 15:    proc  0 (p:1) buggy_01.pml:8 (state 2)  [temp = n]
        p(0):temp = 3
 16:    proc  0 (p:1) buggy_01.pml:8 (state 3)  [temp = (temp+1)]
        p(0):temp = 4
 17:    proc  0 (p:1) buggy_01.pml:8 (state 4)  [n = temp]
        n = 4
 18:    proc  0 (p:1) buggy_01.pml:8 (state 5)  [countp = (countp+1)]
        p(0):countp = 2
 19:    proc  0 (p:1) buggy_01.pml:9 (state 6)  [((countp>=2))]
spin: buggy_01.pml:27, Error: assertion violated
spin: text of failed assertion: assert((n!=4))
 20:    proc  2 (monitor:1) buggy_01.pml:27 (state 2)   [assert((n!=4))]
spin: trail ends after 20 steps
#processes: 3
        n = 4
 20:    proc  2 (monitor:1) buggy_01.pml:26 (state 3)
 20:    proc  1 (q:1) buggy_01.pml:22 (state 9) <valid end state>
 20:    proc  0 (p:1) buggy_01.pml:11 (state 11) <valid end state>
3 processes created

如您所见，它报告（一个）导致断言违规的可能执行跟踪。

零担。

可以想到几个ltl 属性，它们可以帮助验证n最终是否等于4. 其中一个属性是[] (n != 4)，其内容如下：

从初始状态开始，在所有输出路径上的每个可达状态中，它true总是n不同于4.

新模型如下所示：

byte n;

active proctype p()
{
    byte countp = 0;
    byte temp;
    do
    :: countp != 2 -> temp = n; temp = temp + 1; n = temp; countp = countp + 1;
    :: countp >= 2 -> break;
    od
}

active proctype q()
{

    byte countq = 0;

    do
    :: countq != 2 -> n = n + 1; countq = countq + 1;
    :: countq >= 2 -> break;
    od
}

ltl p0 { [] (n != 4) }

您验证此属性的方式与使用断言的方式几乎相同。为了使这个答案简短，我不会在此处复制并粘贴整个输出，而仅列出使用的命令：

~$ spin -search -bfs buggy_02.pml
ltl p0: [] ((n!=4))
Depth=10 States=40 Transitions=40 Memory=128.195    
pan:1: assertion violated  !( !((n!=4))) (at depth 15)
pan: wrote buggy_02.pml.trail

...

Full statespace search for:
    never claim             + (p0)
    ...
State-vector 28 byte, depth reached 15, errors: 1
...

~$ spin -t -p -g -l buggy_02.pml
...

如果您想保证n最终总是等于4，那么您应该研究一些互斥方法来保护您的关键部分，或者，检查.d_step {}

于 2017-03-09T10:29:40.133 回答