發(fā)布時(shí)間：2017-08-03 02:24

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

  更多相關(guān)文章： 形式化驗(yàn)證 概率模型檢測(cè) 領(lǐng)導(dǎo)者選舉協(xié)議 動(dòng)態(tài)系統(tǒng)

【摘要】：領(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)行建模,圍繞著動(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)證。(1)在模型分析的過程中,針對(duì)模型檢測(cè)領(lǐng)域常見的“狀態(tài)爆炸”問題,本文通過簡(jiǎn)化協(xié)議的內(nèi)部操作,刪除多余步驟,來減少模型的狀態(tài)數(shù)。對(duì)其中不確定的行為,通過為其設(shè)定概率系數(shù),取代原先復(fù)雜的條件判定操作,從而緩解了模型狀態(tài)爆炸問題的產(chǎn)生。(2)在模型構(gòu)建的過程中,引入了“假設(shè)-保證”的組合式驗(yàn)證思想,將層次式協(xié)議進(jìn)行分別處理,建立了一個(gè)具有雙層結(jié)構(gòu)的領(lǐng)導(dǎo)者選舉協(xié)議模型,并通過實(shí)驗(yàn),給出了具體驗(yàn)證結(jié)果,顯示了該模型的有效性。(3)在整個(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)行了分層建模與驗(yàn)證,驗(yàn)證模型的規(guī)模和效率比傳統(tǒng)的整體式驗(yàn)證都有了很大的提升,為動(dòng)態(tài)系統(tǒng)中領(lǐng)導(dǎo)者的確定,提供了一種比較合理的方法,增強(qiáng)了動(dòng)態(tài)系統(tǒng)的工作效率。
【關(guān)鍵詞】：形式化驗(yàn)證 概率模型檢測(cè) 領(lǐng)導(dǎo)者選舉協(xié)議 動(dòng)態(tài)系統(tǒng)
【學(xué)位授予單位】：南京航空航天大學(xué)
【學(xué)位級(jí)別】：碩士
【學(xué)位授予年份】：2016
【分類號(hào)】：TP338.8
【目錄】：

• 摘要4-5
• ABSTRACT5-10
• 注釋表10-11
• 縮略詞11-12
• 第一章 緒論12-17
• 1.1 研究背景和意義12-13
• 1.2 研究現(xiàn)狀13-15
• 1.3 主要研究內(nèi)容15-16
• 1.4 文章的組織結(jié)構(gòu)16-17
• 第二章 相關(guān)概念和工具介紹17-21
• 2.1 相關(guān)概念17-19
• 2.1.1 概率模型檢測(cè)17-18
• 2.1.2 動(dòng)態(tài)系統(tǒng)18
• 2.1.3 領(lǐng)導(dǎo)者選舉協(xié)議18-19
• 2.2 PRISM簡(jiǎn)介19
• 2.3 本章小結(jié)19-21
• 第三章 動(dòng)態(tài)系統(tǒng)層次式領(lǐng)導(dǎo)者選舉協(xié)議的介紹21-36
• 3.1 系統(tǒng)模型與假設(shè)21-24
• 3.1.1 進(jìn)程與簇21-22
• 3.1.2 異步性與穩(wěn)定性22-23
• 3.1.3“詢問-回復(fù)”操作與相關(guān)假設(shè)23-24
• 3.2 動(dòng)態(tài)系統(tǒng)領(lǐng)導(dǎo)者選舉協(xié)議介紹24-35
• 3.2.1 下層領(lǐng)導(dǎo)者選舉協(xié)議24-31
• 3.2.2 上層領(lǐng)導(dǎo)者選舉協(xié)議31-35
• 3.3 本章小結(jié)35-36
• 第四章 構(gòu)建PRISM概率模型36-49
• 4.1 相關(guān)理論支持36-37
• 4.1.1 假設(shè)-保證驗(yàn)證36
• 4.1.2 布爾型變量法實(shí)現(xiàn)集合交、并操作36-37
• 4.2 下層領(lǐng)導(dǎo)者選舉模型的構(gòu)建和屬性驗(yàn)證37-42
• 4.2.1 流程狀態(tài)分析38
• 4.2.2 協(xié)議-模型轉(zhuǎn)化38-42
• 4.3 上層領(lǐng)導(dǎo)者選舉模型的構(gòu)建和屬性驗(yàn)證42-45
• 4.3.1 流程狀態(tài)分析43
• 4.3.2 協(xié)議-模型轉(zhuǎn)化43-45
• 4.4 基于C語言的自動(dòng)生成建模腳本語言45-48
• 4.4.1 參數(shù)化分析46-47
• 4.4.2 區(qū)域化實(shí)現(xiàn)47-48
• 4.5 本章小結(jié)48-49
• 第五章 關(guān)于協(xié)議可靠性的PRISM模型驗(yàn)證49-62
• 5.1 基于假設(shè)-保證的分層建�？煽啃则�(yàn)證49-55
• 5.1.1 下層模型屬性驗(yàn)證49-52
• 5.1.2 上層模型屬性驗(yàn)證52-55
• 5.2 模型分層與整體驗(yàn)證開銷對(duì)比55-58
• 5.2.1 模型分層驗(yàn)證的開銷55-56
• 5.2.2 模型整體驗(yàn)證的開銷56-58
• 5.3 不穩(wěn)定環(huán)境下領(lǐng)導(dǎo)者選舉協(xié)議的可靠性分析58-60
• 5.3.1 下層環(huán)境不穩(wěn)定對(duì)協(xié)議可靠性的影響58-59
• 5.3.2 上層環(huán)境不穩(wěn)定對(duì)協(xié)議可靠性的影響59-60
• 5.4 本章小結(jié)60-62
• 第六章 總結(jié)與展望62-63
• 參考文獻(xiàn)63-67
• 致謝67-68
• 在學(xué)期間的研究成果及發(fā)表的學(xué)術(shù)論文68

【參考文獻(xiàn)】

中國期刊全文數(shù)據(jù)庫 前10條

1 馬銀雪;陳哲;黃志球;黃吳丹;;使用模型檢驗(yàn)自動(dòng)化驗(yàn)證路由協(xié)議[J];小型微型計(jì)算機(jī)系統(tǒng);2015年11期

2 周筱羽;顧斌;趙建華;楊孟飛;李宣東;;中斷驅(qū)動(dòng)系統(tǒng)模型檢驗(yàn)?[J];軟件學(xué)報(bào);2015年09期

3 張偉偉;宋曉琳;張三林;吳訓(xùn)成;;基于軟硬件協(xié)同設(shè)計(jì)的車道線實(shí)時(shí)識(shí)別方法[J];中國機(jī)械工程;2015年10期

4 夏春蕊;王瑞;李曉娟;關(guān)永;;概率模型檢測(cè)技術(shù)在機(jī)器人路徑規(guī)劃中的應(yīng)用[J];計(jì)算機(jī)仿真;2015年03期

5 劉來;駱翔宇;;一個(gè)分布式K互斥算法的概率模型檢測(cè)[J];計(jì)算機(jī)應(yīng)用研究;2015年04期

6 支志兵;;容斥原理在漢密爾頓問題中的應(yīng)用[J];數(shù)學(xué)理論與應(yīng)用;2014年02期

7 莊t-;沈昌祥;蔡勉;;基于行為的可信動(dòng)態(tài)度量的狀態(tài)空間約簡(jiǎn)研究[J];計(jì)算機(jī)學(xué)報(bào);2014年05期

8 賈寧;楊春;佟冬;王克義;;動(dòng)態(tài)翻譯系統(tǒng)中的間接轉(zhuǎn)移關(guān)聯(lián)軟件預(yù)測(cè)算法[J];計(jì)算機(jī)研究與發(fā)展;2014年03期

9 周東華;史建濤;何瀟;;動(dòng)態(tài)系統(tǒng)間歇故障診斷技術(shù)綜述[J];自動(dòng)化學(xué)報(bào);2014年02期

10 田浪軍;陳衛(wèi)衛(wèi);陳衛(wèi)東;李濤;;云存儲(chǔ)系統(tǒng)中動(dòng)態(tài)負(fù)載均衡算法研究[J];計(jì)算機(jī)工程;2013年10期

中國博士學(xué)位論文全文數(shù)據(jù)庫 前1條

1 劉志鋒;模型檢測(cè)中關(guān)鍵技術(shù)的研究及其應(yīng)用[D];南京大學(xué);2011年

中國碩士學(xué)位論文全文數(shù)據(jù)庫 前2條

1 陳道喜;基于Promela的組合抽象Spin模型檢測(cè)及應(yīng)用[D];蘇州大學(xué);2009年

2 王敏飛;模型檢測(cè)在安全協(xié)議驗(yàn)證中的研究與應(yīng)用[D];南京航空航天大學(xué);2009年

，

本文編號(hào)：612284