《通讯协议 （例子）》由会员分享，可在线阅读，更多相关《通讯协议 （例子）（26页珍藏版）》请在金锄头文库上搜索。
1、通讯协议 (例子),通讯协议,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: 0.1; INIT err=0; PROC chr: chrs(); chs: chrs(); cha: chab(); chb: c
2、hab(); 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,进
3、程模块说明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) VAR INIT TRANS nn=rr: (c,s,chr.start,chr.len):=( chr.contentschr.start,chr.seqchr.start, (chr.start+1)%QS,ch
4、r.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;
5、 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,
6、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 received INIT (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,b
7、lue; 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)
8、,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 - ti
9、me = 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: 0.1; INIT err=0; PROC chr: chrs(); chs: chrs(); cha: chab(); chb: chab(); pra: mpra(); p
10、rb: 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 CONCLUSION: FALSE (time=1986),验证过程,验证问题,Model,建模,VERDS Model Checker,Positive Conclusion,Negative Conclusion,Error Trace,安全性质,问题?,
