基于模型檢查的網(wǎng)絡(luò)協(xié)議分析與驗(yàn)證.pdf

1、網(wǎng)絡(luò)協(xié)議具有空間分布性、并發(fā)性和異步性，這些特性導(dǎo)致一些并發(fā)錯(cuò)誤難以重現(xiàn)，傳統(tǒng)測試手段很難發(fā)現(xiàn)這些潛在問題。模型檢查作為一種形式化驗(yàn)證方法，能夠自動(dòng)驗(yàn)證一個(gè)系統(tǒng)是否滿足設(shè)計(jì)規(guī)范，具有高度自動(dòng)化和提供反例等諸多優(yōu)點(diǎn)，近年來被廣泛應(yīng)用于軟硬件驗(yàn)證中。通過模型檢查技術(shù)驗(yàn)證協(xié)議設(shè)計(jì)規(guī)范，可以有效減少協(xié)議設(shè)計(jì)錯(cuò)誤，更好的保證協(xié)議設(shè)計(jì)和實(shí)現(xiàn)的正確性和完整性。 本文基于模型檢查工具SPIN對網(wǎng)絡(luò)協(xié)議進(jìn)行形式化分析與驗(yàn)證。分別針對TCP連接管理

2、協(xié)議和無線局域網(wǎng)協(xié)議(802.11i)的雙向認(rèn)證過程進(jìn)行了建模與驗(yàn)證。通過分析協(xié)議設(shè)計(jì)規(guī)范，提取出協(xié)議行為的有限狀態(tài)自動(dòng)機(jī)作為過渡模型，并轉(zhuǎn)化為PROMELA模型作為SPIN工具的輸入，隨后采用線性時(shí)序邏輯(Linear-time Temporal Logic，LTL)公式描述系統(tǒng)期望滿足的屬性，根據(jù)SPIN的模擬結(jié)果對模型進(jìn)行修改和完善，最終形成與設(shè)計(jì)高度一致的模型。利用SPIN工具檢測PROMELA模型是否能滿足期望的屬性，如果不滿