1、隨著計算機(jī)通信與網(wǎng)絡(luò)技術(shù)的發(fā)展，網(wǎng)絡(luò)協(xié)議的穩(wěn)定性和安全性發(fā)揮著越來越重要的作用，所以對網(wǎng)絡(luò)協(xié)議的研究有重要意義。形式化的方法將成為分析網(wǎng)絡(luò)協(xié)議的重要方法，目前有很多研究網(wǎng)絡(luò)協(xié)議的理論和方法，比較重要的理論有BAN邏輯，定理證明和模型檢測等，而模型檢測作為形式化分析理論方法中的一種，有著自動化和提供反例等優(yōu)點，基于此，我們采用形式化方法和模型檢測工具來檢測網(wǎng)絡(luò)協(xié)議的漏洞也是很有意義的，從而達(dá)到提高網(wǎng)絡(luò)協(xié)議安全性和穩(wěn)定性的目的。
　　

2、 本文首先在介紹網(wǎng)絡(luò)協(xié)議、形式化方法和模型檢測工具及其應(yīng)用的基礎(chǔ)上，通過不同的安裝環(huán)境對SIPN工具使用做了介紹，并對形式化描述的幾種語言進(jìn)行比較；其次，介紹了OSPF路由協(xié)議的概念、特性和協(xié)議的操作及工作過程，同時采用形式化方法的FSM分析了OSPF協(xié)議；接著重點分析了OSPF網(wǎng)絡(luò)類型、報文頭部、報文處理流程和LSA處理流程；緊接著通過SPIN模型檢測工具對OSPF協(xié)議進(jìn)行抽象化建模，描述了OSPF協(xié)議的LTL性質(zhì)，并剛XSPIN模

3、型檢測工具進(jìn)行了檢測驗證，得到了運行軌跡，在此基礎(chǔ)上又采剛穩(wěn)定狀態(tài)驗證的方法從可行性和正確性等方面驗證了OSPF路由協(xié)議；最后總結(jié)本文的主要工作并對尚需完善的工作進(jìn)行展望。
　　 本文采用的主要方法和技術(shù)如下：⑴采用形式化的分析方法，對OSPF協(xié)議分析；⑵SPIN適用于并行系統(tǒng)，本文探討了在Windows、Java、Cygwin等環(huán)境下對SPIN工具的安裝和使用，并詳細(xì)介紹了SPIN的圖形界面工具XSPIN的安裝過程和功能的使用