基于模型檢驗(yàn)的路由協(xié)議驗(yàn)證方法研究.pdf

1、計(jì)算機(jī)網(wǎng)絡(luò)多樣化的發(fā)展催生出大量新的路由協(xié)議，這些路由協(xié)議的安全性和正確性問題亟待解決。目前，基于形式化的方法、技術(shù)、工具已大量應(yīng)用在路由協(xié)議研究上，幫助實(shí)現(xiàn)協(xié)議的設(shè)計(jì)和實(shí)施。但現(xiàn)實(shí)問題是，一方面路由協(xié)議的發(fā)展變得多樣化，協(xié)議應(yīng)用的網(wǎng)絡(luò)規(guī)模從少節(jié)點(diǎn)到多節(jié)點(diǎn)不等；分層路由和人為規(guī)定的選路策略也使得概念簡(jiǎn)單清晰、性能優(yōu)良的算法變得復(fù)雜；通信鏈路和節(jié)點(diǎn)的不可靠使網(wǎng)絡(luò)拓?fù)涑蕜?dòng)態(tài)變化。另一方面，形式化方法的理論較深，規(guī)約、建模語言多樣，模型檢驗(yàn)、

2、定理證明技術(shù)多樣，支持形式化驗(yàn)證的工具多樣。相比理論上的可行性，形式化方法的工具仍然較弱。因此，網(wǎng)絡(luò)協(xié)議研究人員如果想掌握全部知識(shí)似乎不可行，選擇合適的形式化驗(yàn)證方法、技術(shù)、工具應(yīng)用在路由協(xié)議設(shè)計(jì)和實(shí)現(xiàn)上，也需要花費(fèi)大量時(shí)間和精力。
　　本文提出一種基于模型檢驗(yàn)的路由協(xié)議正確性和安全性的驗(yàn)證方法，該方法通過對(duì)協(xié)議的假設(shè)和簡(jiǎn)化抽取出模型，并通過基于反例的抽象精化技術(shù)實(shí)行驗(yàn)證和模型精化。將該方法應(yīng)用在三個(gè)路由協(xié)議的建模和驗(yàn)證上，使用有