《通讯协议例子》PPT课件.ppt

《《通讯协议例子》PPT课件.ppt》由会员分享，可在线阅读，更多相关《《通讯协议例子》PPT课件.ppt（26页珍藏版）》请在淘文阁 - 分享文档赚钱的网站上搜索。

1、通讯协议(例子)通讯协议BA通讯协议BASR通讯协议BASR通讯协议BchaASRchbchrchs通讯协议prbchaprapssprrchbchrchs obuf busy s q ibuf recv m pMWQS通讯协议模型(主程序)VVM ft001 DEFINE QS=2 QSL=1 M=4 ML=3 W=2 WL=1 rr=0 ss=1 aa=2 bb=3VAR err:0.1;INIT err=0;PROC chr:chrs();chs:chrs();cha:chab();chb:chab();pra:mpra();prb:mprb();SPEC AG(err!=1);进程模块

2、说明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;star

3、t:0.QSL;INIT (for xx in 0.QSL):contentsxx=0;len=0;start=0;TRANS FALSE:TRUE;过程说明1PROCEDURE 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)&RETURN;nn=ss:(c,s,chs.start,chs.len):=(chs.contentschs.start,chs.seqchs.start,(chs.st

4、art+1)%QS,chs.len-1)&RETURN;nn=aa:(c,cha.start,cha.len):=(cha.contentscha.start,(cha.start+1)%QS,cha.len-1)&RETURN;nn=bb:(c,chb.start,chb.len):=(chb.contentschb.start,(chb.start+1)%QS,chb.len-1)&RETURN;过程说明2PROCEDURE chput(nn,c,s)VAR pc:s0,s1;pos:0.QS;INIT pc=s0;pos=0;TRANS nn=0&pc=s0:(pos,pc):=(chr

5、.start+chr.len)%QS,s1);nn=0&pc=s1:(chr.contentspos,chr.seqpos,chr.len):=(c,s,chr.len+1)&RETURN;nn=1&pc=s0:(pos,pc):=(chs.start+chs.len)%QS,s1);nn=1&pc=s1:(chs.contentspos,chs.seqpos,chs.len):=(c,s,chs.len+1)&RETURN;nn=2&pc=s0:(pos,pc):=(cha.start+cha.len)%QS,s1);nn=2&pc=s1:(cha.contentspos,cha.len):

6、=(c,cha.len+1)&RETURN;nn=3&pc=s0:(pos,pc):=(chb.start+chb.len)%QS,s1);nn=3&pc=s1:(chb.contentspos,chb.len):=(c,chb.len+1)&RETURN;进程模块说明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 i

7、n 0.ML):obufxx=0;q=0;s=0;y=0;wd=0;TRANS wd0&chr.len0:chget(ss,ack,y)&(busyy):=(0);wd0&busyq=0:(wd,q):=(wd-1,(q+1)%M);chr.len0&busyq=1:mpsscase2(q)&(wd):=(wd);过程说明3aPROCEDURE 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)&(pc):=(s1);pc=s1:(wd,pss

8、.busys,pss.obufs,pc):=(wd+1,1,tmp,s2);pc=s2:chput(rr,tmp,s)&(s):=(s+1)%M)&RETURN;过程说明3bPROCEDURE 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)&RETURN;进程模块说明4(prr)MODULE mprr()VAR recv0.ML:0.1;ibuf0.ML:ack,red,green,blue;p:0.ML;m

9、: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)&(m):=(m);recvp=1&chb.lenQS&chs.lenm&p-mm&p+M-mm&p-mm&p+M-m=W):RETURN;pc=s1&prr.recvm=0:(prr.ibufm,prr.recvm,pc):=(tmp,1,s2);pc=s2:(prr.recv(m+M-W)%M,pc):=(0,s2)&RETURN;过程

10、说明4bPROCEDURE 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)&(pc):=(s2);pc=s2:chput(ss,ack,p)&(p,pc):=(p+1)%M,s3);pc=s3:RETURN;进程模块说明(测试进程pra)MODULE mpra()VAR pc:s0,s1,s2,s3;INIT pc=s0;TRANS pc=s0&cha.lenQS:chput(aa,r

11、ed,0)&(pc):=(s1);pc=s1&cha.lenQS:chput(aa,red,0)&(pc):=(s1);pc=s1&cha.lenQS:chput(aa,green,0)&(pc):=(s2);pc=s2&cha.lenQS:chput(aa,green,0)&(pc):=(s2);pc=s2&cha.lenQS:chput(aa,blue,0)&(pc):=(s3);pc=s3&cha.len0:chget(bb,x,0)&(pc):=(s1);pc=s1&x=red:(pc):=(s2);pc=s1&x!=red:(err,pc):=(1,s1);进程模块说明(续)pc=s

12、2&chb.len0:chget(bb,x,0)&(pc):=(s3);pc=s3&x=red:(pc):=(s2);pc=s3&x=green:(pc):=(s4);pc=s3&x!=red&x!=green:(err,pc):=(1,s3);pc=s4&chb.len0:chget(bb,x,0)&(pc):=(s5);pc=s5&x=green:(pc):=(s4);pc=s5&x=blue:(pc):=(s6);pc=s5&x!=green&x!=blue:(err,pc):=(1,s5);pc=s6&chb.len0:chget(bb,x,0)&(pc):=(s7);pc=s7&x=

13、blue:(pc):=(s6);pc=s7&x!=blue:(err,pc):=(1,s7);模型检测./verds-ck 1 ft001.vvm./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(t

14、ime=58824)可达性问题通讯协议模型(主程序)VVM ft001 DEFINE QS=2 QSL=1 M=4 ML=3 W=2 WL=1 rr=0 ss=1 aa=2 bb=3VAR 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.vvm./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 CheckerPositive Conclusionhttp:/ ConclusionError Trace安全性质问题?