通讯
协议
离婚协议模板下载合伙人协议 下载渠道分销协议免费下载敬业协议下载授课协议下载
例子Stillwatersrundeep.流静水深,人静心深Wherethereislife,thereishope。有生命必有希望通讯协议BA通讯协议BASR通讯协议BASR通讯协议BchaASRchbchrchs通讯协议prbchaprapssprrchbchrchsobuf[]busy[]sqibuf[]recv[]mpMWQS通讯协议模型(主程序)VVMft001DEFINEQS=2QSL=1M=4ML=3W=2WL=1rr=0ss=1aa=2bb=3VARerr:0..1;INITerr=0;PROCchr:chrs();chs:chrs();cha:chab();chb:chab();pra:mpra();prb:mprb();SPECAG(err!=1);进程模块说明1(通道)MODULEchrs()VARcontents[0..QSL]:{ack,red,green,blue};seq[0..QSL]:0..ML;len:0..QS;start:0..QSL;INIT(forxxin[0..QSL]):contents[xx]=0;(forxxin[0..QSL]):seq[xx]=0;len=0;start=0;TRANSlen>0:(len,start):=(len-1,(start+1)%M);//loosychannel进程模块说明2(通道)MODULEchab()VARcontents[0..QSL]:{ack,red,green,blue};len:0..QS;start:0..QSL;INIT(forxxin[0..QSL]):contents[xx]=0;len=0;start=0;TRANSFALSE:TRUE;过程说明1PROCEDUREchget(nn,c,s)VARINITTRANSnn=rr:(c,s,chr.start,chr.len):=(chr.contents[chr.start],chr.seq[chr.start],(chr.start+1)%QS,chr.len-1)&RETURN;nn=ss:(c,s,chs.start,chs.len):=(chs.contents[chs.start],chs.seq[chs.start],(chs.start+1)%QS,chs.len-1)&RETURN;nn=aa:(c,cha.start,cha.len):=(cha.contents[cha.start],(cha.start+1)%QS,cha.len-1)&RETURN;nn=bb:(c,chb.start,chb.len):=(chb.contents[chb.start],(chb.start+1)%QS,chb.len-1)&RETURN;过程说明2PROCEDUREchput(nn,c,s)VARpc:{s0,s1};pos:0..QS;INITpc=s0;pos=0;TRANSnn=0&pc=s0:(pos,pc):=((chr.start+chr.len)%QS,s1);nn=0&pc=s1:(chr.contents[pos],chr.seq[pos],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.contents[pos],chs.seq[pos],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.contents[pos],cha.len):=(c,cha.len+1)&RETURN;nn=3&pc=s0:(pos,pc):=((chb.start+chb.len)%QS,s1);nn=3&pc=s1:(chb.contents[pos],chb.len):=(c,chb.len+1)&RETURN;进程模块说明3(pss)MODULEmpss()VARbusy[0..ML]:0..1;obuf[0..ML]:{ack,red,green,blue};q:0..ML;s:0..ML;//q=oldestunacked,s=nexttosendy:0..ML;wd:0..W;INIT(forxxin[0..ML]):busy[xx]=0;(forxxin[0..ML]):obuf[xx]=0;q=0;s=0;y=0;wd=0;TRANSwd
0&chr.len0:chget(ss,ack,y)&(busy[y]):=(0);wd>0&busy[q]=0:(wd,q):=(wd-1,(q+1)%M);chr.len0&busy[q]=1:mpsscase2(q)&(wd):=(wd);过程说明3aPROCEDUREmpsscase1(wd,s)VARpc:{s0,s1,s2,s3};tmp:{ack,red,green,blue};INITpc=s0;tmp=0;TRANSpc=s0:chget(aa,tmp,s)&(pc):=(s1);pc=s1:(wd,pss.busy[s],pss.obuf[s],pc):=(wd+1,1,tmp,s2);pc=s2:chput(rr,tmp,s)&(s):=((s+1)%M)&RETURN;过程说明3bPROCEDUREmpsscase2(q)VARpc:{s0,s1};tmp:{ack,red,green,blue};INITpc=s0;TRANSpc=s0:(tmp,pc):=(pss.obuf[q],s1);pc=s1:chput(rr,tmp,q)&RETURN;进程模块说明4(prr)MODULEmprr()VARrecv[0..ML]:0..1;ibuf[0..ML]:{ack,red,green,blue};p:0..ML;m:0..ML;//p=lastacked,m=lastreceivedINIT(forxxin[0..ML]):recv[xx]=0;(forxxin[0..ML]):ibuf[xx]=0;p=0;m=0;TRANSchr.len>0:mprrcase1(m,p)&(m):=(m);recv[p]=1&chb.lenm&p-m<=W)|(p+M>m&p+M-m<=W)):chput(ss,ack,m)&RETURN;pc=s1&prr.recv[m]=1&!((p>m&p-m<=W)|(p+M>m&p+M-m<=W)):RETURN;pc=s1&prr.recv[m]=0:(prr.ibuf[m],prr.recv[m],pc):=(tmp,1,s2);pc=s2:(prr.recv[(m+M-W)%M],pc):=(0,s2)&RETURN;过程说明4bPROCEDUREmprrcase2(p)VARpc:{s0,s1,s2,s3};tmp:{ack,red,green,blue};INITpc=s0;tmp=0;TRANSpc=s0:(tmp,pc):=(prr.ibuf[p],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)MODULEmpra()VARpc:{s0,s1,s2,s3};INITpc=s0;TRANSpc=s0&cha.len0:chget(bb,x,0)&(pc):=(s1);pc=s1&x=red:(pc):=(s2);pc=s1&x!=red:(err,pc):=(1,s1);进程模块说明(续)pc=s2&chb.len>0: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.len>0: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.len>0:chget(bb,x,0)&(pc):=(s7);pc=s7&x=blue:(pc):=(s6);pc=s7&x!=blue:(err,pc):=(1,s7);模型检测./verds-ck1ft001.vvmVERSION:verds1.43-JAN2013FILE:ft001.vvmPROPERTY:AG(errB1)bound=0time=2----------time=2bound=1time=2----------time=2bound=2time=2----------time=2..bound=102time=58706----------time=58706bound=103time=58824----------time=58824CONCLUSION:TRUE(time=58824)可达性问题通讯协议模型(主程序)VVMft001DEFINEQS=2QSL=1M=4ML=3W=2WL=1rr=0ss=1aa=2bb=3VARerr:0..1;INITerr=0;PROCchr:chrs();chs:chrs();cha:chab();chb:chab();pra:mpra();prb:mprb();SPECAG(err!=1);AG(prb.pc!=s7);模型检测./verds-Xce-ck2ft001.vvmVERSION:verds1.43-JAN2013FILE:ft001.vvmPROPERTY:AG(errB1)bound=0time=2----------time=2bound=1time=2----------time=2bound=2time=2----------time=2..bound=26time=1449----------time=1449bound=27time=1637----------time=1637CONCLUSION:FALSE(time=1986)验证过程验证问题Model建模VERDSModelCheckerPositiveConclusionhttp://lcs.ios.ac.cn/~zwh/verds/NegativeConclusionErrorTrace安全性质问题?
浙公网安备 33021202002483