《《通讯协议例子》PPT课件》由会员分享，可在线阅读，更多相关《《通讯协议例子》PPT课件（26页珍藏版）》请在装配图网上搜索。
1、通 讯 协 议 (例 子 ) 通 讯 协 议 BA 通 讯 协 议 BA S R 通 讯 协 议 BA S R 通 讯 协 议 BchaA S Rchbchrchs 通 讯 协 议 prbchapra pss prrchbchrchs obuf busy s q ibuf recv m pMWQS 通 讯 协 议 模 型 (主 程 序 )VVM ft0 0 1 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:
2、 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-
3、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; 过 程 说 明 1PROCEDURE chget(nn,c,s)VARINITTRANS nn=rr: (c,s,chr.start,chr.len):=( chr.contentsc
4、hr.start,chr.seqchr.start, (chr.start+1 )%QS,chr.len-1 ) nn=ss: (c,s,chs.start,chs.len):=( chs.contentschs.start,chs.seqchs.start, (chs.start+1 )%QS,chs.len-1 ) nn=aa: (c,cha.start,cha.len):=( cha.contentscha.start,(cha.start+1 )%QS,cha.len-1 ) nn=bb: (c,chb.start,chb.len):=( chb.contentschb.start,(
5、chb.start+1 )%QS,chb.len-1 ) 过 程 说 明 2PROCEDURE chput(nn,c,s)VAR pc: s0 ,s1 ; pos: 0 .QS;INIT pc=s0 ; pos=0 ;TRANS nn=0 nn=0 nn=1 nn=1 nn=2 nn=2 nn=3 nn=3 进 程 模 块 说 明 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 .M
6、L; 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 wd0 chr.len0 过 程 说 明 3 aPROCEDURE 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 : (wd,pss.busys,pss.obufs,pc):=(w
7、d+1 ,1 ,tmp,s2 ); pc=s2 : chput(rr,tmp,s) 过 程 说 明 3 bPROCEDURE 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; /
8、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) recvp=1 pc=s1 pc=s2 : (prr.recv(m+M-W)%M,pc):=(0 ,s2 ) 过 程 说 明 4 bPROCEDURE mprrcase2 (p)VAR pc: s0 ,s1 ,s2 ,s3 ; tmp: ack,red,green,blue;INIT pc=s0 ; tmp=0 ;TRAN
9、S pc=s0 : (tmp,pc):=(prr.ibufp,s1 ); pc=s1 : chput(bb,tmp,0 ) pc=s2 : chput(ss,ack,p) pc=s3 : RETURN; 进 程 模 块 说 明 (测 试 进 程 pra)MODULE mpra()VAR pc: s0 ,s1 ,s2 ,s3 ;INIT pc=s0 ;TRANS pc=s0 pc=s1 pc=s1 pc=s2 pc=s2 pc=s3 pc=s1 pc=s1 进 程 模 块 说 明 (续 ) pc=s2 pc=s3 pc=s3 pc=s3 pc=s4 pc=s5 pc=s5 pc=s5 pc=s6
10、 pc=s7 pc=s7 模 型 检 测./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
11、) 可 达 性 问 题 通 讯 协 议 模 型 (主 程 序 )VVM ft0 0 1 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 -
12、 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:/ Negative ConclusionError Trace 安 全 性 质 问 题 ?
《通讯协议例子》PPT课件
