通訊協(xié)議例子(參考版)
2025-07-20 14:08本頁面
【正文】 模型檢測 ./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)證過程 驗(yàn)證問題 Model 建模 VERDS Model Checker Positive Conclusion Negative Conclusion Error Trace 安全性質(zhì) 問題 ? 。 SPEC AG(err!=1)。 pra: mpra()。 cha: chab()。 PROC chr: chrs()。 模型檢測 ./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á)性問題 通訊協(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。 pc=s7amp。 pc=s7amp。0: chget(bb,x,0)amp。x!=blue: (err,pc):=(1,s5)。 pc=s5amp。 pc=s5amp。 pc=s5amp。0: chget(bb,x,0)amp。x!=green: (err,pc):=(1,s3)。 pc=s3amp。 pc=s3amp。 pc=s3amp。0: chget(bb,x,0)amp。x!=red: (err,pc):=(1,s1)。x=red: (pc):=(
研究報(bào)告相關(guān)推薦
鄂ICP備17016276號-1