隨著信息技術的高速發(fā)展,計算機系統(tǒng)已經被廣泛的應用于日常生活中的各個方面,比如電話通訊系統(tǒng)、銀行系統(tǒng)等。這些系統(tǒng)大部分都需要后臺運行的分布式算法來完成一些基本目標,比如分布式一致性和錯誤避免。這些算法的正確性和有效性對系統(tǒng)而言是至關重要的。然而,由于分布式算法所運行的環(huán)境復雜,算法的設計很容易出錯。應用恰當?shù)臄?shù)學理論和分析方法可以增強系統(tǒng)的正確性和可靠性�；谀Ｐ蜋z測的形式化方法就是這樣一種技術,并已成功地在實踐中應用于對復雜的時序線路設計和通信協(xié)議的正確性驗證。 模型檢測通過遍歷系統(tǒng)所有可達的狀態(tài)空間來驗證系統(tǒng)是否滿足特定的安全屬性。當被驗證的系統(tǒng)的狀態(tài)空間非常大,甚至是無限的時候,就會導致模型檢測中的狀態(tài)空間爆炸問題：即在有限的時間和存儲空間條件下,無法遍歷系統(tǒng)的整個狀態(tài)空間,進而無法對系統(tǒng)的正確性進行驗證。在分布式計算領域中,存在著許多分布式算法用來解決分布式計算中的基本問題,比如領袖選舉問題和一致性問題。由于這些問題沒有確定性的解決方案,這些算法往往通過引入輪數(shù)來確保其能夠以一定的概率完成目標,但這卻導致了輪數(shù)的無界性,從而導致在應用模型檢測對算法進行形式化驗證時的空間爆炸問題...

【文章頁數(shù)】：73 頁

【學位級別】：碩士

【部分圖文】：

圖5.1輪數(shù)之間的距離可能會無限增加

以無限增加，從而使得算法的狀態(tài)空間是無限的。為了模型檢測該算法，就需要有一個對輪數(shù)的有限表示。然而，不同于Itai一Rodeh領袖選舉算法，本文沒有發(fā)現(xiàn)該算法中正確進程的輪數(shù)之間的存在一個距離的上界。下圖5.1給出了該算法中輪數(shù)之間的距離無限增加的一個可能的執(zhí)行。r二2…V=1-....

圖5.2輪數(shù)之間的距離可能會無限增加

就需要有對輪數(shù)進行有限表示。類似于第5，1節(jié)中的BT一致性算法，本文同樣沒有找到該算法輪數(shù)之間的有界距離，正確進程的輪數(shù)之間的距離可以無限增加(見圖5.2)。在圖5.2中，進程p，停留在輪數(shù)r一1中，而其它所有進程則無限的增加輪數(shù):在第r=1輪中，協(xié)調者pZ根據(jù)收到的消息得到這一....

本文編號：4004296