《通讯协议例子》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,M W QS,通讯协议模型(主程序),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: 01; INIT err=0; PROC chr: chrs(); chs: chrs(); cha: chab(); chb: chab(); pra: mpra(); prb: mprb(); SPEC AG(err!=1);,进程模块说明1(通道),MODULE chrs() VAR contents0QSL: ack,red,green,blue; seq0QSL: 0ML; len: 0QS; start: 0QSL; INIT (for xx in 0QSL): contentsxx=0; (for xx in 0QSL): seqxx=0; len=0; start=0; TRANS len0: (len,start):=(len-1,(start+1)%M); /loosy channel,进程模块说明2(通道),MODULE chab() VAR contents0QSL: ack,red,green,blue; len: 0QS; start: 0QSL; INIT (for xx in 0QSL): contentsxx=0; len=0; start=0; TRANS FALSE: TRUE;,过程说明1,PROCEDURE chget(nn,c,s) VAR INIT TRANS 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: 0QS; INIT pc=s0; pos=0; TRANS nn=0,进程模块说明3(pss),MODULE mpss() VAR busy0ML: 01; obuf0ML: ack,red,green,blue; q: 0ML; s: 0ML; /q=oldest unacked,s=next to send y: 0ML; wd: 0W; INIT (for xx in 0ML): busyxx=0; (for xx in 0ML): 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 recv0ML: 01; ibuf0ML: ack,red,green,blue; p: 0ML; m: 0ML; /p=last acked, m=last received INIT (for xx in 0ML): recvxx=0; (for xx in 0ML): 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.vvm VERSION: verds 1.43 - JAN 2013 FILE: ft001.vvm PROPERTY: A G (err B 1 ) bound = 0 time = 2 - time = 2 bound = 1 time = 2 - time = 2 bound = 2 time = 2 - time = 2 . . bound =102 time = 58706 - time = 58706 bound =103 time = 58824 - time = 58824 CONCLUSION: 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: 01; 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 VERSION: verds 1.43 - JAN 2013 FILE: ft001.vvm PROPERTY: A G (err B 1 ) bound = 0 time = 2 - time = 2 bound = 1 time = 2 - time = 2 bound = 2 time = 2 - time = 2 . . bound = 26 time = 1449 - time = 1449 bound = 27 time = 1637 - time = 1637 CONC