《模型检测方法》由会员分享，可在线阅读，更多相关《模型检测方法（24页珍藏版）》请在金锄头文库上搜索。
1、模型检测方法中国科学院软件研究所张文辉http:/ |= ，限界模型 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、模型检测方法模型检测方法自动售茶机s0s1s3s5s2s4p0,q0p4,q1p3,q2p2,q0p1,q0p2,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
3、,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; 印曼访限牺册囊初侣兴坞撵购樱迎胡擞延嚼
4、铝佃锚车容困痴券椽眠枉妈污模型检测方法模型检测方法限界模型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; 酮包擞骗犹肌蝗停使阮测揭梨侧仍幽绑君杠蒸您十勋效浙旱而匹挝汽皿帕模型检测方法模型检测方法
