《通讯协议例子》PPT课件.ppt
通讯协议(例子),通讯协议,B,A,通讯协议,B,A,S,R,通讯协议,B,A,S,R,通讯协议,B,cha,A,S,R,chb,chr,chs,通讯协议,prb,cha,pra,pss,prr,chb,chr,chs,obuf busy s q,ibuf recv m p,MWQS,通讯协议模型(主程序),VVM ft001 DEFINE QS=2 QSL=1 M=4 ML=3 W=2 WL=1 rr=0 ss=1 aa=2 bb=3,VAR err:0.1;INIT err=0;PROC chr:chrs();chs:chrs();cha:chab();chb:chab();pra:mpra();prb:mprb();SPEC AG(err!=1);,进程模块说明1(通道),MODULE chrs()VAR contents0.QSL:ack,red,green,blue;seq0.QSL:0.ML;len:0.QS;start:0.QSL;INIT(for xx in 0.QSL):contentsxx=0;(for xx in 0.QSL):seqxx=0;len=0;start=0;TRANS len0:(len,start):=(len-1,(start+1)%M);/loosy channel,进程模块说明2(通道),MODULE chab()VAR contents0.QSL:ack,red,green,blue;len:0.QS;start:0.QSL;INIT(for xx in 0.QSL):contentsxx=0;len=0;start=0;TRANS FALSE:TRUE;,过程说明1,PROCEDURE chget(nn,c,s)VARINITTRANS nn=rr:(c,s,chr.start,chr.len):=(chr.contentschr.start,chr.seqchr.start,(chr.start+1)%QS,chr.len-1),过程说明2,PROCEDURE chput(nn,c,s)VAR pc:s0,s1;pos:0.QS;INIT pc=s0;pos=0;TRANS nn=0,进程模块说明3(pss),MODULE mpss()VAR busy0.ML:0.1;obuf0.ML:ack,red,green,blue;q:0.ML;s:0.ML;/q=oldest unacked,s=next to send y:0.ML;wd:0.W;INIT(for xx in 0.ML):busyxx=0;(for xx in 0.ML):obufxx=0;q=0;s=0;y=0;wd=0;TRANS wd0,过程说明3a,PROCEDURE mpsscase1(wd,s)VAR pc:s0,s1,s2,s3;tmp:ack,red,green,blue;INIT pc=s0;tmp=0;TRANS pc=s0:chget(aa,tmp,s),过程说明3b,PROCEDURE mpsscase2(q)VAR pc:s0,s1;tmp:ack,red,green,blue;INIT pc=s0;TRANS pc=s0:(tmp,pc):=(pss.obufq,s1);pc=s1:chput(rr,tmp,q),进程模块说明4(prr),MODULE mprr()VAR recv0.ML:0.1;ibuf0.ML:ack,red,green,blue;p:0.ML;m:0.ML;/p=last acked,m=last receivedINIT(for xx in 0.ML):recvxx=0;(for xx in 0.ML):ibufxx=0;p=0;m=0;TRANS chr.len0:mprrcase1(m,p),过程说明4a,PROCEDURE mprrcase1(m,p)VAR pc:s0,s1,s2;tmp:ack,red,green,blue;INIT pc=s0;tmp=0;TRANS pc=s0:chget(rr,tmp,m),过程说明4b,PROCEDURE mprrcase2(p)VAR pc:s0,s1,s2,s3;tmp:ack,red,green,blue;INIT pc=s0;tmp=0;TRANS pc=s0:(tmp,pc):=(prr.ibufp,s1);pc=s1:chput(bb,tmp,0),进程模块说明(测试进程pra),MODULE mpra()VAR pc:s0,s1,s2,s3;INIT pc=s0;TRANS pc=s0,进程模块说明(测试进程prb),MODULE mprb()VAR x:ack,red,green,blue;pc:s0,s1,s2,s3,s4,s5,s6,s7;INIT x=0;pc=s0;TRANS pc=s0,进程模块说明(续),pc=s2,模型检测,./verds-ck 1 ft001.vvmVERSION:verds 1.43-JAN 2013FILE:ft001.vvmPROPERTY:A G(err B 1)bound=0 time=2-time=2bound=1 time=2-time=2bound=2 time=2-time=2.bound=102 time=58706-time=58706bound=103 time=58824-time=58824CONCLUSION:TRUE(time=58824),可达性问题,通讯协议模型(主程序),VVM ft001 DEFINE QS=2 QSL=1 M=4 ML=3 W=2 WL=1 rr=0 ss=1 aa=2 bb=3,VAR err:0.1;INIT err=0;PROC chr:chrs();chs:chrs();cha:chab();chb:chab();pra:mpra();prb:mprb();SPEC AG(err!=1);AG(prb.pc!=s7);,模型检测,./verds-Xce-ck 2 ft001.vvmVERSION:verds 1.43-JAN 2013FILE:ft001.vvmPROPERTY:A G(err B 1)bound=0 time=2-time=2bound=1 time=2-time=2bound=2 time=2-time=2.bound=26 time=1449-time=1449bound=27 time=1637-time=1637CONCLUSION:FALSE(time=1986),验证过程,验证问题,Model,建模,VERDSModel Checker,Positive Conclusion,http:/,Negative Conclusion,Error Trace,安全性质,问题?,
