模型检测方法 中国科学院软件研究所 张文辉 http://lcs.ios.ac.cn/~zwh/pv.

Presentation on theme: "模型检测方法 中国科学院软件研究所 张文辉 http://lcs.ios.ac.cn/~zwh/pv."— Presentation transcript:

1 模型检测方法 中国科学院软件研究所 张文辉

2 BDD (ab)(bc)(ad) a b b c c c c d d d d d d d d 1 1 1 1 1 1 1 2

3 BDD (ab)(bc)(ad) a b b c c c c d d d d d d d d 1 3

4 BDD (ab)(bc)(ad) a b b c c c c d d d d d d d d 1 4

5 BDD (ab)(bc)(ad) a b b c c c c d d d d d 1 5

6 BDD (ab)(bc)(ad) a b b c c c c d d d d d 1 6

7 BDD (ab)(bc)(ad) a b b c c c c d d d 1 7

8 BDD (ab)(bc)(ad) a b b c c c c d d d 1 8

9 BDD (ab)(bc)(ad) a b b c c c c d 1 9

10 BDD (ab)(bc)(ad) a b b c c c c d 1 10

11 BDD (ab)(bc)(ad) a b b c c d 1 11

12 BDD (ab)(bc)(ad) a b b c c c c d d d d d d d d 1 1 1 1 1 1 1 12

13 BDD (ab)(bc)(ad) a b b c c c c d d d d d d d d 1 1 1 1 1 1 1 13

14 BDD (ab)(bc)(ad) a b b c 1 c d 1 1 14

15 BDD (ab)(bc)(ad) a b b c c d 1 15

16 限界模型检测与验证 从模型的局部考察一个性质是否满足 对一些不满足的性质可能很快知道问题 对一些满足的性质也可能很快知道结论

17 限界模型检测与验证

18 限界模型检测与验证

19 限界模型检测与验证 M,s |=  ，限界模型 M0, M1, …. 问题：是否存在k ，Mk,s |=m  ?
存在k, Mk,s |=m , 则 M,s |=  ==> 系统满足性质 可靠性 K 较小时， 较快验证系统性质

20 限界模型检测与验证 M,s |=  ，限界模型 M0, M1, …. 问题：是否存在k ，Mk,s |=m  ?
存在k, Mk,s |=m , 则 M,s |=  则 M,s |=  ==> 系统存在问题 可靠性 K 较小时， 较快查出系统问题

21 自动售茶机 {p0,q0} s0 {p1,q0} {p2,q0} s1 s2 {p4,q1} s3 s4 {p2,q0} s5

22 E(q0 U q2) vs A(q0 R q2) P0: s0 P1: s0 s1; s0 s2; P2: s0 s1 s3;
我们有 M2, s0 s1 s5 |= (q0 U q2) 因此 M2 满足 E(q0 U q2) M 满足 E(q0 U q2) M0 |= E(q0 U q2), M1 |= E(q0 U q2) M2=(S,P2,s0,L)是最小 可确定E(q0 U q2)是否满足的限界模型

23 AG(q0q2) vs EF(q0q2) P0: s0 P1: s0 s1; s0 s2; P2: s0 s1 s3;
我们有 M2, s0 s2 s4 |= F(q0q2) 因此 M2 满足 EF(q0q2) M 不满足 AG(q0q2) M0 |=EF(q0q2), M1 |=EF(q0q2) M2=(S,P2,s0,L)是最小 可确定AG(q0q2)是否满足的限界模型

24 限界模型 P0: s0 P1: s0 s1; s0 s2; P2: s0 s1 s3; s0 s1 s5; s0 s2 s4;