基于概率模型檢測(cè)的動(dòng)態(tài)系統(tǒng)領(lǐng)導(dǎo)者選舉協(xié)議分析與驗(yàn)證.pdf

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

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

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