基于概率模型檢測的動態(tài)系統(tǒng)領導者選舉協(xié)議分析與驗證.pdf

1、領導者選舉協(xié)議是分布式計算中的重要協(xié)議。它能夠保證分布式系統(tǒng)選舉出唯一的領導者，使之協(xié)同系統(tǒng)中其余進程的工作，以此提高整個系統(tǒng)的工作效率。隨著動態(tài)系統(tǒng)逐漸成為分布式計算的研究熱點，在該系統(tǒng)中的領導者選舉協(xié)議的設計和驗證獲得較多的關注。對于該協(xié)議的驗證，必須立足于動態(tài)系統(tǒng)。
　　由于動態(tài)系統(tǒng)中包含了很多不確定的因素，這給傳統(tǒng)的基于模型檢測的協(xié)議驗證方法帶來了很大的挑戰(zhàn)。本文采用概率模型檢測技術，對這種廣泛存在的不確定性進行建模，圍繞

2、著動態(tài)系統(tǒng)中的領導者選舉協(xié)議進行了較為系統(tǒng)的分析，并應用主流開源概率模型檢測工具PRISM對最近提出的層次式領導者選舉協(xié)議進行建模與驗證。
　?。?）在模型分析的過程中，針對模型檢測領域常見的“狀態(tài)爆炸”問題，本文通過簡化協(xié)議的內部操作，刪除多余步驟，來減少模型的狀態(tài)數(shù)。對其中不確定的行為，通過為其設定概率系數(shù)，取代原先復雜的條件判定操作，從而緩解了模型狀態(tài)爆炸問題的產生。
　?。?）在模型構建的過程中，引入了“假設-保證”

3、的組合式驗證思想，將層次式協(xié)議進行分別處理，建立了一個具有雙層結構的領導者選舉協(xié)議模型，并通過實驗，給出了具體驗證結果，顯示了該模型的有效性。
　?。?）在整個實驗的過程中，針對模型中含有大量相似的內容造成代碼重復書寫的問題，本文提出了一種自動生成PRISM代碼的方法，在很大程度上提高了代碼的編寫效率。并且借助于C語言，完成了簡易的PRISM代碼自動生成的腳本程序。
　　本文的研究意義在于對近期提出的層次式領導者選舉協(xié)議進行