《模型检测方法.ppt》由会员分享，可在线阅读，更多相关《模型检测方法.ppt（24页珍藏版）》请在三一办公上搜索。
1、模型检测方法,中国科学院软件研究所张文辉http:/,(ab)(bc)(ad),2,BDD,a,b,c,d,d,0,0,0,0,c,d,d,0,1,0,0,b,c,d,d,1,1,1,1,c,d,d,1,1,0,0,(ab)(bc)(ad),3,BDD,a,b,c,d,d,0,c,d,d,b,c,d,d,1,c,d,d,(ab)(bc)(ad),4,BDD,a,b,c,d,d,0,c,d,d,b,c,d,d,1,c,d,d,(ab)(bc)(ad),5,BDD,a,b,c,d,0,c,d,b,c,d,d,1,c,d,(ab)(bc)(ad),6,BDD,a,b,c,d,0,c,d,b,c,d,
2、d,1,c,d,(ab)(bc)(ad),7,BDD,a,b,c,d,0,c,d,b,c,1,c,d,(ab)(bc)(ad),8,BDD,a,b,c,d,0,c,d,b,c,1,c,d,(ab)(bc)(ad),9,BDD,a,b,c,c,d,b,c,c,0,1,(ab)(bc)(ad),10,BDD,a,b,c,c,d,b,c,c,0,1,(ab)(bc)(ad),11,BDD,a,b,c,d,b,c,0,1,(ab)(bc)(ad),12,BDD,a,b,c,d,d,0,0,0,0,c,d,d,0,1,0,0,b,c,d,d,1,1,1,1,c,d,d,1,1,0,0,(ab)(bc)(
3、ad),13,BDD,a,b,c,d,d,0,0,0,0,c,d,d,0,1,0,0,b,c,d,d,1,1,1,1,c,d,d,1,1,0,0,(ab)(bc)(ad),14,BDD,a,b,0,c,d,0,0,1,b,1,c,1,0,(ab)(bc)(ad),15,BDD,a,b,c,d,0,1,b,c,限界模型检测与验证,从模型的局部考察一个性质是否满足对一些不满足的性质可能很快知道问题对一些满足的性质也可能很快知道结论,限界模型检测与验证,限界模型检测与验证,限界模型检测与验证,M,s|=，限界模型 M0,M1,.问题：是否存在k，Mk,s|=m?存在k,Mk,s|=m,则 M,s|=
4、系统满足性质,可靠性,K 较小时，较快验证系统性质,限界模型检测与验证,M,s|=，限界模型 M0,M1,.问题：是否存在k，Mk,s|=m?存在k,Mk,s|=m,则 M,s|=则 M,s|=系统存在问题,可靠性,K 较小时，较快查出系统问题,自动售茶机,s0,s1,s3,s5,s2,s4,p0,q0,p4,q1,p3,q2,p2,q0,p1,q0,p2,q0,E(q0 U q2)vs A(q0 R q2),P0:s0 P1:s0 s1;s0 s2;P2:s0 s1 s3;s0 s1 s5;s0 s2 s4;s0 s2 s5;,我们有M2,s0 s1 s5|=(q0 U q2)因此 M2 满
5、足 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),我们有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;s0 s2 s5;,限界模型,P4:s0 s1 s3 s4 s5;s0 s1 s3 s5 s0;s0 s1 s5 s0 s1;s0 s1 s5 s0 s2;s0 s2 s4 s5 s0;s0 s2 s5 s0 s1;s0 s2 s5 s0 s2;,P3:s0 s1 s3 s4;s0 s1 s3 s5;s0 s1 s5 s0;s0 s2 s4 s5;s0 s2 s5 s0;,P0:s0 P1:s0 s1;s0 s2;P2:s0 s1 s3;s0 s1 s5;s0 s2 s4;s0 s2 s5;,
