模型檢測是協(xié)議驗(yàn)證的技術(shù)之一。在CSMA/CD協(xié)議的驗(yàn)證過程中對該協(xié)議進(jìn)行了簡化,忽略了通道時(shí)延、退避算法等細(xì)節(jié),運(yùn)用Promela語言進(jìn)行建模實(shí)現(xiàn)。最后,使用模型檢測工具SPIN對協(xié)議實(shí)現(xiàn)的正確性、狀態(tài)可達(dá)性以及可能存在的不可推進(jìn)循環(huán)進(jìn)行了分析和檢驗(yàn),并從結(jié)果的有效性和正確性方面得出了相應(yīng)驗(yàn)證輸出圖。 

【文章來源】：計(jì)算機(jī)應(yīng)用. 2013年S2期 北大核心

【文章頁數(shù)】：4 頁

【文章目錄】：
1 CSMA/CD協(xié)議
2協(xié)議形式化描述
    2.1消息通道的描述
    2.2進(jìn)程的描述
        2.2.1 Medium進(jìn)程
        2.2.2 Node進(jìn)程
        2.2.3 User進(jìn)程
        2.2.4 init進(jìn)程
3協(xié)議驗(yàn)證
4結(jié)語



本文編號：2930874