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

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

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