通訊協(xié)議例子-資料下載頁(yè)
2025-07-17 14:08本頁(yè)面
【正文】 amp。x=blue: (pc):=(s6)。 pc=s5amp。x!=greenamp。x!=blue: (err,pc):=(1,s5)。 pc=s6amp。0: chget(bb,x,0)amp。(pc):=(s7)。 pc=s7amp。x=blue: (pc):=(s6)。 pc=s7amp。x!=blue: (err,pc):=(1,s7)。 模型檢測(cè) ./verds ck 1 VERSION: verds JAN 2022 FILE: 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) 可達(dá)性問(wèn)題 通訊協(xié)議模型 (主程序 ) 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()。 prb: mprb()。 SPEC AG(err!=1)。 AG(!=s7)。 模型檢測(cè) ./verds Xce ck 2 VERSION: verds JAN 2022 FILE: 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) 驗(yàn)證過(guò)程 驗(yàn)證問(wèn)題 Model 建模 VERDS Model Checker Positive Conclusion Negative Conclusion Error Trace 安全性質(zhì) 問(wèn)題 ?
研究報(bào)告相關(guān)推薦
鄂ICP備17016276號(hào)-1