模型检测方法 中国科学院软件研究所 张文辉 http://lcs.ios.ac.cn/~zwh/pv
BDD (ab)(bc)(ad) a b b c c c c d d d d d d d d 1 1 1 1 1 1 1 2
BDD (ab)(bc)(ad) a b b c c c c d d d d d d d d 1 3
BDD (ab)(bc)(ad) a b b c c c c d d d d d d d d 1 4
BDD (ab)(bc)(ad) a b b c c c c d d d d d 1 5
BDD (ab)(bc)(ad) a b b c c c c d d d d d 1 6
BDD (ab)(bc)(ad) a b b c c c c d d d 1 7
BDD (ab)(bc)(ad) a b b c c c c d d d 1 8
BDD (ab)(bc)(ad) a b b c c c c d 1 9
BDD (ab)(bc)(ad) a b b c c c c d 1 10
BDD (ab)(bc)(ad) a b b c c d 1 11
BDD (ab)(bc)(ad) a b b c c c c d d d d d d d d 1 1 1 1 1 1 1 12
BDD (ab)(bc)(ad) a b b c c c c d d d d d d d d 1 1 1 1 1 1 1 13
BDD (ab)(bc)(ad) a b b c 1 c d 1 1 14
BDD (ab)(bc)(ad) a b b c c d 1 15
限界模型检测与验证 从模型的局部考察一个性质是否满足 对一些不满足的性质可能很快知道问题 对一些满足的性质也可能很快知道结论
限界模型检测与验证
限界模型检测与验证
限界模型检测与验证 M,s |= ,限界模型 M0, M1, …. 问题:是否存在k ,Mk,s |=m ? 存在k, Mk,s |=m , 则 M,s |= ==> 系统满足性质 可靠性 K 较小时, 较快验证系统性质
限界模型检测与验证 M,s |= ,限界模型 M0, M1, …. 问题:是否存在k ,Mk,s |=m ? 存在k, Mk,s |=m , 则 M,s |= 则 M,s |= ==> 系统存在问题 可靠性 K 较小时, 较快查出系统问题
自动售茶机 {p0,q0} s0 {p1,q0} {p2,q0} s1 s2 {p4,q1} s3 s4 {p2,q0} s5
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)是否满足的限界模型
AG(q0q2) vs EF(q0q2) P0: s0 P1: s0 s1; s0 s2; P2: s0 s1 s3; 我们有 M2, s0 s2 s4 |= F(q0q2) 因此 M2 满足 EF(q0q2) M 不满足 AG(q0q2) M0 |=EF(q0q2), M1 |=EF(q0q2) M2=(S,P2,s0,L)是最小 可确定AG(q0q2)是否满足的限界模型
限界模型 P0: s0 P1: s0 s1; s0 s2; P2: s0 s1 s3; s0 s1 s5; s0 s2 s4;