IPv6鄰居發(fā)現協(xié)議的形式化驗證.pdf

1、隨著網絡和通信技術的高速發(fā)展,大量新的協(xié)議不斷被提出.但是,到目前為止,Internet的協(xié)議標準RFC仍然使用自然語言描述,Internet的協(xié)議實現也主要是采用人工編制完成,這種協(xié)議軟件開發(fā)是隨意的,并逐步擴大的.隨著網絡服務要求的提高,網絡系統(tǒng)的復雜性在協(xié)議方面體現出空間分布性、并發(fā)性、異步性、不穩(wěn)定性和多樣性,網絡協(xié)議再也不可能用工程直覺方法設計出高質量的協(xié)議,協(xié)議的完整性、正確性、安全性、可移植性和標準化都難以得到保證,而且協(xié)

2、議實現后糾正協(xié)議描述錯誤的代價是十分可觀的.錯誤或不完全的協(xié)議可能導致整個網絡的癱瘓,以及服務可靠性的降低.這就要求我們必須在協(xié)議投入實際應用之前,進行協(xié)議驗證,來保證協(xié)議設計的正確性和完整性.也就是說,為了更好地研究和實現協(xié)議,應該采用協(xié)議工程的方法,通過適當的技術和計算機輔助工具,來設計和維護網絡協(xié)議.協(xié)議形式化理論是協(xié)議工程學的核心.形式化驗證技術在協(xié)議的驗證工作中,具有良好的發(fā)展前途,并且近幾年來受到了廣泛的重視.形式化說明語言