基于有色Petri網的SPIN協(xié)議驗證.pdf

1、無線傳感器網絡作為一種新興的技術，已成為當前國際上備受關注的研究熱點，被認為是對21世紀產生巨大影響力的技術之一。路由協(xié)議的研究是無線傳感器網絡的一個重要研究領域，其中對現(xiàn)有協(xié)議進行分析和驗證，確定各種現(xiàn)有協(xié)議對無線傳感器網絡的可用性是很重要的一個方向。SPIN是無線傳感器網絡中第一個基于數據的路由協(xié)議，它采用協(xié)商機制和資源自適應機制解決了傳統(tǒng)協(xié)議所存在的問題，大大節(jié)省了能量，延長了網絡壽命。SPIN包括兩個協(xié)議：SPIN-1和SPIN

2、-2。 目前對SPIN協(xié)議的研究主要是通過NS平臺進行仿真，進而分析協(xié)議的性能。本文從另一角度出發(fā)采用形式化的方法對協(xié)議進行驗證。文章首先使用形式化建模工具有色Petri網分別對SPIN-1協(xié)議和SPIN-2協(xié)議進行了形式化分析，并給出了它們的有色Petri網模型，然后利用自動化分析工具CPN Tools分別對這兩個模型進行模擬運行，得到模型的可達圖和相關分析報告，依此對協(xié)議的特性進行分析，證明協(xié)議具有活性、可達性、有界性等特性

3、。 SPIN是針對理想無損網絡設計的，沒有考慮到現(xiàn)實網絡中數據包丟失的現(xiàn)象。針對這個問題，本文提出了SPIN-E協(xié)議，它在SPIN的基礎上增加了重傳機制，使其能夠適用于有損網絡。然后文章使用有色Petri網對SPIN-E協(xié)議進行建模，通過CPN Tools對模型進行分析，證明了協(xié)議不存在死鎖，具有可達性和有界性。驗證了使用SPIN-E協(xié)議在網絡傳輸有損的情況下，節(jié)點仍能得到它所期望的數據。 本文對無線傳感器網絡的路由協(xié)議