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

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

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

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



本文編號：2930874