如何正式验证以下协议是否正确？
How does one formally verify that the following protocol is correct?
在下面的代码示例中，一个 Sender 和一个 Receiver 交换 -- 时间长度不确定-- 包数。 Sender 发送的每条消息都包含 0 或 1 和一个序列号。每当 Receiver 收到一条消息时，它都会检查它是否是新的，在这种情况下它会向 Sender 发回一个 acknowledgment。收到 ACK 后，发件人 发送一条包含新内容的消息。
在此模型中，每当发送消息时，消息可能会丢失、发送两次或正常发送。
mtype = { MESSAGE, ACK };
chan sender2receiver = [2] of { mtype, bit, int };
chan receiver2sender = [2] of { mtype, bit, int };
inline unreliable_send(channel, type, tag, seqno) {
bool loss = false;
bool duplicate = true;
if
:: channel!type(tag, seqno);
if
:: channel!type(tag, seqno);
:: duplicate = false;
fi
:: loss = true;
fi
}
active proctype Sender () {
bit in_bit, out_bit;
int seq_no;
do
:: unreliable_send(sender2receiver, MESSAGE, out_bit, seq_no) ->
receiver2sender?ACK(in_bit, 0);
if
:: in_bit == out_bit ->
out_bit = 1 - out_bit;
seq_no++;
:: else ->
skip;
fi;
od;
}
active proctype Receiver () {
bit in_bit, old_bit;
int seq_no;
do
:: sender2receiver?MESSAGE(in_bit, seq_no) ->
if
:: in_bit != old_bit ->
printf("received: %d\n", seq_no);
old_bit = in_bit;
:: else ->
skip;
fi;
unreliable_send(receiver2sender, ACK, in_bit, 0);
od;
}
在之前的模型中，数据包丢失会导致死锁。
为了解决这个问题，讲师讨论了几种方法。
其中一种方法是让 Sender 无情地发送消息，直到它有效地传递给 Receiver 及其对应的 ack 已被 发件人 正确接收。 即：
active proctype Sender () {
bit in_bit, out_bit;
int seq_no;
// solution 1: keep sending a message till an ack is received
do
:: unreliable_send(sender2receiver, MESSAGE, out_bit, seq_no);
:: receiver2sender?ACK(in_bit, 0);
if
:: in_bit == out_bit ->
out_bit = 1 - out_bit;
seq_no++;
:: else ->
skip;
fi;
od;
}
虽然在实践中这种方法似乎有效，这意味着模拟模型不再导致死锁，但讲师警告我们它仍然会失败 形式验证 因为至少存在一个不幸的执行路径，在某个时刻所有消息都丢失了，无论有多少人坚持再次发送相同的消息。
讲师邀请我们思考如何使用 Spin 找到建议方法失败的执行轨迹之一。由于我们还没有涵盖 LTL 模型检查，解决方案应该基于 assert 或 labels.
协议背后的想法是 Sender 和 Receiver 不断交换 new messages无限长的时间。
可以通过进度标签.
验证所提出的解决方案是否有效地遵守了该规范
Progress labels are used to define correctness claims. A progress
label states the requirement that the labeled global state must be
visited infinitely often in any infinite system execution. Any
violation of this requirement can be reported by the verifier as a
non-progress cycle.
在此模型中，progress-state 是我们确定消息已正确发送和确认的模型，因此我们的 progress-state 是我们意识到这一事实后立即出现的模型。
因此，我们编辑Sender代码如下，在in_bit == out_bit ->后添加一个progress:标签：
active proctype Sender () {
bit in_bit, out_bit;
int seq_no;
// solution 1: keep sending a message till an ack is received
do
:: unreliable_send(sender2receiver, MESSAGE, out_bit, seq_no);
:: receiver2sender?ACK(in_bit, 0);
if
:: in_bit == out_bit ->
progress:
out_bit = 1 - out_bit;
seq_no++;
:: else ->
skip;
fi;
od;
}
然后我们可以正式验证模型如下：
~$ spin -a -DNP test.pml
~$ gcc -DNP pan.c -o run
~$ ./run -l -bfs
或者，或者，使用以下 one-liner：
~$ spin -search -l test.pml
正如预期的那样，spin 找到一个 non-progress 循环:
pan:1: non-progress cycle (at depth 16)
pan: wrote test.pml.trail
(Spin Version 6.4.7 -- 19 August 2017)
Warning: Search not completed
+ Partial Order Reduction
Full statespace search for:
never claim + (:np_:)
assertion violations + (if within scope of claim)
non-progress cycles + (fairness disabled)
invalid end states - (disabled by never claim)
State-vector 88 byte, depth reached 41, errors: 1
21 states, stored
0 states, matched
21 transitions (= stored+matched)
0 atomic steps
hash conflicts: 0 (resolved)
Stats on memory usage (in Megabytes):
0.002 equivalent memory usage for states (stored*(State-vector + overhead))
0.287 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
pan: elapsed time 0 seconds
我们现在可以模拟 counter-example 并显示打印有问题的执行轨迹：
~$ spin -p -l -g -t test.pml
starting claim 2
spin: couldn't find claim 2 (ignored)
using statement merging
2: proc 0 (Sender:1) test.pml:8 (state 1) [loss = 0]
Sender(0):loss = 0
2: proc 0 (Sender:1) test.pml:9 (state 2) [duplicate = 1]
Sender(0):duplicate = 1
Sender(0):loss = 0
4: proc 0 (Sender:1) test.pml:10 (state 3) [sender2receiver!2,out_bit,seq_no]
queue 1 (sender2receiver): [MESSAGE,0,0]
6: proc 1 (Receiver:1) test.pml:44 (state 1) [sender2receiver?MESSAGE,in_bit,seq_no]
queue 1 (sender2receiver):
Receiver(1):seq_no = 0
Receiver(1):in_bit = 0
8: proc 1 (Receiver:1) test.pml:49 (state 5) [else]
queue 1 (sender2receiver):
10: proc 1 (Receiver:1) test.pml:50 (state 6) [(1)]
queue 1 (sender2receiver):
12: proc 1 (Receiver:1) test.pml:8 (state 9) [loss = 0]
queue 1 (sender2receiver):
Receiver(1):loss = 0
12: proc 1 (Receiver:1) test.pml:9 (state 10) [duplicate = 1]
queue 1 (sender2receiver):
Receiver(1):duplicate = 1
Receiver(1):loss = 0
14: proc 1 (Receiver:1) test.pml:10 (state 11) [receiver2sender!1,in_bit,0]
queue 1 (sender2receiver):
queue 2 (receiver2sender): [ACK,0,0]
16: proc 1 (Receiver:1) test.pml:12 (state 12) [receiver2sender!1,in_bit,0]
queue 1 (sender2receiver):
queue 2 (receiver2sender): [ACK,0,0][ACK,0,0]
<<<<<START OF CYCLE>>>>>
18: proc 0 (Sender:1) test.pml:12 (state 4) [sender2receiver!2,out_bit,seq_no]
queue 1 (sender2receiver): [MESSAGE,0,0]
queue 2 (receiver2sender): [ACK,0,0][ACK,0,0]
20: proc 1 (Receiver:1) test.pml:44 (state 1) [sender2receiver?MESSAGE,in_bit,seq_no]
queue 1 (sender2receiver):
queue 2 (receiver2sender): [ACK,0,0][ACK,0,0]
Receiver(1):seq_no = 0
Receiver(1):in_bit = 0
22: proc 1 (Receiver:1) test.pml:49 (state 5) [else]
queue 1 (sender2receiver):
queue 2 (receiver2sender): [ACK,0,0][ACK,0,0]
24: proc 1 (Receiver:1) test.pml:50 (state 6) [(1)]
queue 1 (sender2receiver):
queue 2 (receiver2sender): [ACK,0,0][ACK,0,0]
26: proc 1 (Receiver:1) test.pml:8 (state 9) [loss = 0]
queue 1 (sender2receiver):
queue 2 (receiver2sender): [ACK,0,0][ACK,0,0]
Receiver(1):loss = 0
26: proc 1 (Receiver:1) test.pml:9 (state 10) [duplicate = 1]
queue 1 (sender2receiver):
queue 2 (receiver2sender): [ACK,0,0][ACK,0,0]
Receiver(1):duplicate = 1
Receiver(1):loss = 0
28: proc 1 (Receiver:1) test.pml:15 (state 16) [loss = 1]
queue 1 (sender2receiver):
queue 2 (receiver2sender): [ACK,0,0][ACK,0,0]
Receiver(1):loss = 1
30: proc 0 (Sender:1) test.pml:8 (state 1) [loss = 0]
queue 1 (sender2receiver):
queue 2 (receiver2sender): [ACK,0,0][ACK,0,0]
Sender(0):loss = 0
30: proc 0 (Sender:1) test.pml:9 (state 2) [duplicate = 1]
queue 1 (sender2receiver):
queue 2 (receiver2sender): [ACK,0,0][ACK,0,0]
Sender(0):duplicate = 1
Sender(0):loss = 0
32: proc 0 (Sender:1) test.pml:10 (state 3) [sender2receiver!2,out_bit,seq_no]
queue 1 (sender2receiver): [MESSAGE,0,0]
queue 2 (receiver2sender): [ACK,0,0][ACK,0,0]
34: proc 1 (Receiver:1) test.pml:44 (state 1) [sender2receiver?MESSAGE,in_bit,seq_no]
queue 1 (sender2receiver):
queue 2 (receiver2sender): [ACK,0,0][ACK,0,0]
Receiver(1):seq_no = 0
Receiver(1):in_bit = 0
36: proc 1 (Receiver:1) test.pml:49 (state 5) [else]
queue 1 (sender2receiver):
queue 2 (receiver2sender): [ACK,0,0][ACK,0,0]
38: proc 1 (Receiver:1) test.pml:50 (state 6) [(1)]
queue 1 (sender2receiver):
queue 2 (receiver2sender): [ACK,0,0][ACK,0,0]
40: proc 1 (Receiver:1) test.pml:8 (state 9) [loss = 0]
queue 1 (sender2receiver):
queue 2 (receiver2sender): [ACK,0,0][ACK,0,0]
Receiver(1):loss = 0
40: proc 1 (Receiver:1) test.pml:9 (state 10) [duplicate = 1]
queue 1 (sender2receiver):
queue 2 (receiver2sender): [ACK,0,0][ACK,0,0]
Receiver(1):duplicate = 1
Receiver(1):loss = 0
42: proc 1 (Receiver:1) test.pml:15 (state 16) [loss = 1]
queue 1 (sender2receiver):
queue 2 (receiver2sender): [ACK,0,0][ACK,0,0]
Receiver(1):loss = 1
spin: trail ends after 42 steps
#processes: 2
queue 1 (sender2receiver):
queue 2 (receiver2sender): [ACK,0,0][ACK,0,0]
42: proc 1 (Receiver:1) test.pml:43 (state 20)
Receiver(1):loss = 1
42: proc 0 (Sender:1) test.pml:11 (state 6)
2 processes created
在下面的代码示例中，一个 Sender 和一个 Receiver 交换 -- 时间长度不确定-- 包数。 Sender 发送的每条消息都包含 0 或 1 和一个序列号。每当 Receiver 收到一条消息时，它都会检查它是否是新的，在这种情况下它会向 Sender 发回一个 acknowledgment。收到 ACK 后，发件人 发送一条包含新内容的消息。
在此模型中，每当发送消息时，消息可能会丢失、发送两次或正常发送。
mtype = { MESSAGE, ACK };
chan sender2receiver = [2] of { mtype, bit, int };
chan receiver2sender = [2] of { mtype, bit, int };
inline unreliable_send(channel, type, tag, seqno) {
bool loss = false;
bool duplicate = true;
if
:: channel!type(tag, seqno);
if
:: channel!type(tag, seqno);
:: duplicate = false;
fi
:: loss = true;
fi
}
active proctype Sender () {
bit in_bit, out_bit;
int seq_no;
do
:: unreliable_send(sender2receiver, MESSAGE, out_bit, seq_no) ->
receiver2sender?ACK(in_bit, 0);
if
:: in_bit == out_bit ->
out_bit = 1 - out_bit;
seq_no++;
:: else ->
skip;
fi;
od;
}
active proctype Receiver () {
bit in_bit, old_bit;
int seq_no;
do
:: sender2receiver?MESSAGE(in_bit, seq_no) ->
if
:: in_bit != old_bit ->
printf("received: %d\n", seq_no);
old_bit = in_bit;
:: else ->
skip;
fi;
unreliable_send(receiver2sender, ACK, in_bit, 0);
od;
}
在之前的模型中，数据包丢失会导致死锁。
为了解决这个问题，讲师讨论了几种方法。
其中一种方法是让 Sender 无情地发送消息，直到它有效地传递给 Receiver 及其对应的 ack 已被 发件人 正确接收。 即：
active proctype Sender () {
bit in_bit, out_bit;
int seq_no;
// solution 1: keep sending a message till an ack is received
do
:: unreliable_send(sender2receiver, MESSAGE, out_bit, seq_no);
:: receiver2sender?ACK(in_bit, 0);
if
:: in_bit == out_bit ->
out_bit = 1 - out_bit;
seq_no++;
:: else ->
skip;
fi;
od;
}
虽然在实践中这种方法似乎有效，这意味着模拟模型不再导致死锁，但讲师警告我们它仍然会失败 形式验证 因为至少存在一个不幸的执行路径，在某个时刻所有消息都丢失了，无论有多少人坚持再次发送相同的消息。
讲师邀请我们思考如何使用 Spin 找到建议方法失败的执行轨迹之一。由于我们还没有涵盖 LTL 模型检查，解决方案应该基于 assert 或 labels.
协议背后的想法是 Sender 和 Receiver 不断交换 new messages无限长的时间。
可以通过进度标签.
验证所提出的解决方案是否有效地遵守了该规范Progress labels are used to define correctness claims. A progress label states the requirement that the labeled global state must be visited infinitely often in any infinite system execution. Any violation of this requirement can be reported by the verifier as a non-progress cycle.
在此模型中，progress-state 是我们确定消息已正确发送和确认的模型，因此我们的 progress-state 是我们意识到这一事实后立即出现的模型。
因此，我们编辑Sender代码如下，在in_bit == out_bit ->后添加一个progress:标签：
active proctype Sender () {
bit in_bit, out_bit;
int seq_no;
// solution 1: keep sending a message till an ack is received
do
:: unreliable_send(sender2receiver, MESSAGE, out_bit, seq_no);
:: receiver2sender?ACK(in_bit, 0);
if
:: in_bit == out_bit ->
progress:
out_bit = 1 - out_bit;
seq_no++;
:: else ->
skip;
fi;
od;
}
然后我们可以正式验证模型如下：
~$ spin -a -DNP test.pml
~$ gcc -DNP pan.c -o run
~$ ./run -l -bfs
或者，或者，使用以下 one-liner：
~$ spin -search -l test.pml
正如预期的那样，spin 找到一个 non-progress 循环:
pan:1: non-progress cycle (at depth 16)
pan: wrote test.pml.trail
(Spin Version 6.4.7 -- 19 August 2017)
Warning: Search not completed
+ Partial Order Reduction
Full statespace search for:
never claim + (:np_:)
assertion violations + (if within scope of claim)
non-progress cycles + (fairness disabled)
invalid end states - (disabled by never claim)
State-vector 88 byte, depth reached 41, errors: 1
21 states, stored
0 states, matched
21 transitions (= stored+matched)
0 atomic steps
hash conflicts: 0 (resolved)
Stats on memory usage (in Megabytes):
0.002 equivalent memory usage for states (stored*(State-vector + overhead))
0.287 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
pan: elapsed time 0 seconds
我们现在可以模拟 counter-example 并显示打印有问题的执行轨迹：
~$ spin -p -l -g -t test.pml
starting claim 2
spin: couldn't find claim 2 (ignored)
using statement merging
2: proc 0 (Sender:1) test.pml:8 (state 1) [loss = 0]
Sender(0):loss = 0
2: proc 0 (Sender:1) test.pml:9 (state 2) [duplicate = 1]
Sender(0):duplicate = 1
Sender(0):loss = 0
4: proc 0 (Sender:1) test.pml:10 (state 3) [sender2receiver!2,out_bit,seq_no]
queue 1 (sender2receiver): [MESSAGE,0,0]
6: proc 1 (Receiver:1) test.pml:44 (state 1) [sender2receiver?MESSAGE,in_bit,seq_no]
queue 1 (sender2receiver):
Receiver(1):seq_no = 0
Receiver(1):in_bit = 0
8: proc 1 (Receiver:1) test.pml:49 (state 5) [else]
queue 1 (sender2receiver):
10: proc 1 (Receiver:1) test.pml:50 (state 6) [(1)]
queue 1 (sender2receiver):
12: proc 1 (Receiver:1) test.pml:8 (state 9) [loss = 0]
queue 1 (sender2receiver):
Receiver(1):loss = 0
12: proc 1 (Receiver:1) test.pml:9 (state 10) [duplicate = 1]
queue 1 (sender2receiver):
Receiver(1):duplicate = 1
Receiver(1):loss = 0
14: proc 1 (Receiver:1) test.pml:10 (state 11) [receiver2sender!1,in_bit,0]
queue 1 (sender2receiver):
queue 2 (receiver2sender): [ACK,0,0]
16: proc 1 (Receiver:1) test.pml:12 (state 12) [receiver2sender!1,in_bit,0]
queue 1 (sender2receiver):
queue 2 (receiver2sender): [ACK,0,0][ACK,0,0]
<<<<<START OF CYCLE>>>>>
18: proc 0 (Sender:1) test.pml:12 (state 4) [sender2receiver!2,out_bit,seq_no]
queue 1 (sender2receiver): [MESSAGE,0,0]
queue 2 (receiver2sender): [ACK,0,0][ACK,0,0]
20: proc 1 (Receiver:1) test.pml:44 (state 1) [sender2receiver?MESSAGE,in_bit,seq_no]
queue 1 (sender2receiver):
queue 2 (receiver2sender): [ACK,0,0][ACK,0,0]
Receiver(1):seq_no = 0
Receiver(1):in_bit = 0
22: proc 1 (Receiver:1) test.pml:49 (state 5) [else]
queue 1 (sender2receiver):
queue 2 (receiver2sender): [ACK,0,0][ACK,0,0]
24: proc 1 (Receiver:1) test.pml:50 (state 6) [(1)]
queue 1 (sender2receiver):
queue 2 (receiver2sender): [ACK,0,0][ACK,0,0]
26: proc 1 (Receiver:1) test.pml:8 (state 9) [loss = 0]
queue 1 (sender2receiver):
queue 2 (receiver2sender): [ACK,0,0][ACK,0,0]
Receiver(1):loss = 0
26: proc 1 (Receiver:1) test.pml:9 (state 10) [duplicate = 1]
queue 1 (sender2receiver):
queue 2 (receiver2sender): [ACK,0,0][ACK,0,0]
Receiver(1):duplicate = 1
Receiver(1):loss = 0
28: proc 1 (Receiver:1) test.pml:15 (state 16) [loss = 1]
queue 1 (sender2receiver):
queue 2 (receiver2sender): [ACK,0,0][ACK,0,0]
Receiver(1):loss = 1
30: proc 0 (Sender:1) test.pml:8 (state 1) [loss = 0]
queue 1 (sender2receiver):
queue 2 (receiver2sender): [ACK,0,0][ACK,0,0]
Sender(0):loss = 0
30: proc 0 (Sender:1) test.pml:9 (state 2) [duplicate = 1]
queue 1 (sender2receiver):
queue 2 (receiver2sender): [ACK,0,0][ACK,0,0]
Sender(0):duplicate = 1
Sender(0):loss = 0
32: proc 0 (Sender:1) test.pml:10 (state 3) [sender2receiver!2,out_bit,seq_no]
queue 1 (sender2receiver): [MESSAGE,0,0]
queue 2 (receiver2sender): [ACK,0,0][ACK,0,0]
34: proc 1 (Receiver:1) test.pml:44 (state 1) [sender2receiver?MESSAGE,in_bit,seq_no]
queue 1 (sender2receiver):
queue 2 (receiver2sender): [ACK,0,0][ACK,0,0]
Receiver(1):seq_no = 0
Receiver(1):in_bit = 0
36: proc 1 (Receiver:1) test.pml:49 (state 5) [else]
queue 1 (sender2receiver):
queue 2 (receiver2sender): [ACK,0,0][ACK,0,0]
38: proc 1 (Receiver:1) test.pml:50 (state 6) [(1)]
queue 1 (sender2receiver):
queue 2 (receiver2sender): [ACK,0,0][ACK,0,0]
40: proc 1 (Receiver:1) test.pml:8 (state 9) [loss = 0]
queue 1 (sender2receiver):
queue 2 (receiver2sender): [ACK,0,0][ACK,0,0]
Receiver(1):loss = 0
40: proc 1 (Receiver:1) test.pml:9 (state 10) [duplicate = 1]
queue 1 (sender2receiver):
queue 2 (receiver2sender): [ACK,0,0][ACK,0,0]
Receiver(1):duplicate = 1
Receiver(1):loss = 0
42: proc 1 (Receiver:1) test.pml:15 (state 16) [loss = 1]
queue 1 (sender2receiver):
queue 2 (receiver2sender): [ACK,0,0][ACK,0,0]
Receiver(1):loss = 1
spin: trail ends after 42 steps
#processes: 2
queue 1 (sender2receiver):
queue 2 (receiver2sender): [ACK,0,0][ACK,0,0]
42: proc 1 (Receiver:1) test.pml:43 (state 20)
Receiver(1):loss = 1
42: proc 0 (Sender:1) test.pml:11 (state 6)
2 processes created