模型检测方法.ppt
《模型检测方法.ppt》由会员分享,可在线阅读,更多相关《模型检测方法.ppt(24页珍藏版)》请在三一文库上搜索。
1、模型检测方法,中国科学院软件研究所 张文辉 http:/ 对一些不满足的性质可能很快知道问题 对一些满足的性质也可能很快知道结论,限界模型检测与验证,限界模型检测与验证,限界模型检测与验证,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 较小时,
2、 较快查出系统问题,自动售茶机,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 满足 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)是否满足
3、的限界模型,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;,
- 配套讲稿:
如PPT文件的首页显示word图标,表示该PPT已包含配套word讲稿。双击word图标可打开word文档。
- 特殊限制:
部分文档作品中含有的国旗、国徽等图片,仅作为作品整体效果示例展示,禁止商用。设计者仅对作品中独创性部分享有著作权。
- 关 键 词:
- 模型 检测 方法
链接地址:https://www.31doc.com/p-3205822.html