本文關(guān)鍵詞：并發(fā)系統(tǒng)中基于偏序規(guī)約的狀態(tài)空間約簡(jiǎn)與應(yīng)用

  更多相關(guān)文章： 模型檢測(cè) 偏序規(guī)約 頑固集 領(lǐng)導(dǎo)選舉

【摘要】：隨著人們對(duì)軟硬件系統(tǒng)功能需求的日益增加,導(dǎo)致系統(tǒng)的規(guī)模越來越復(fù)雜,其安全性和可靠性也越來越難以得到保證。在一些關(guān)鍵領(lǐng)域,例如航空航天、銀行、證券等,軟件可靠性問題顯得尤為重要,已經(jīng)日益成為當(dāng)今研究的重要課題。在過去的三十幾年間,針對(duì)并發(fā)系統(tǒng)運(yùn)行的不確定性,各國(guó)研究人員為解決可靠性問題做出了許多工作,其中,模型檢測(cè)驗(yàn)證技術(shù)就是該領(lǐng)域中的熱點(diǎn)之一。模型檢測(cè)是一種形式化自動(dòng)驗(yàn)證技術(shù),它可以為許多軟件設(shè)計(jì)中的相關(guān)問題提出解決辦法。一般給定一個(gè)系統(tǒng)的形式化數(shù)學(xué)模型以及形式化的規(guī)約屬性,就可以使用模型檢測(cè)技術(shù)驗(yàn)證該系統(tǒng)是否滿足屬性。自動(dòng)檢測(cè)器的檢測(cè)結(jié)果要不證明該系統(tǒng)滿足該屬性,要不提供一個(gè)反例路徑。然而,對(duì)于許多類型的系統(tǒng)來說,隨著建模系統(tǒng)規(guī)模和進(jìn)程數(shù)目的擴(kuò)大,運(yùn)行過程中可能產(chǎn)生的狀態(tài)數(shù)將呈指數(shù)級(jí)增長(zhǎng),這就引起了狀態(tài)爆炸問題。偏序規(guī)約技術(shù)就是為了緩解異步并發(fā)系統(tǒng)的狀態(tài)爆炸問題而產(chǎn)生的,該技術(shù)主要是構(gòu)建一個(gè)更小的狀態(tài)空間子集,而搜索時(shí)僅探測(cè)該狀態(tài)空間子集,并不是探測(cè)所有的并發(fā)交錯(cuò)運(yùn)行。本文中,我們對(duì)模型檢測(cè)技術(shù)和偏序規(guī)約技術(shù)進(jìn)行深入的研究,主要工作如下:1、詳述了并發(fā)系統(tǒng)的形式化描述方法及模型檢測(cè)的一些基本原則,并研究如何使用TLA+語言對(duì)現(xiàn)實(shí)問題進(jìn)行規(guī)約。2、研究了偏序規(guī)約的相關(guān)理論,同時(shí)對(duì)幾種約簡(jiǎn)狀態(tài)空間的偏序規(guī)約算法進(jìn)行深入研究,包括充足集(ample)、持久集(persistent)、條件頑固集(conditional stubborn)。3、基于條件頑固集和持久集的計(jì)算算法,通過集合理論證明了在相同條件下,有條件頑固集算法比持久集算法更加有效。4、結(jié)合使用頑固集和對(duì)稱性約簡(jiǎn)技術(shù),在Petri網(wǎng)的建模工具基礎(chǔ)上,分析了讀寫互斥算法的約簡(jiǎn)過程,通過工具LoLA進(jìn)行實(shí)驗(yàn)對(duì)比驗(yàn)證。5、研究了偏序規(guī)約的實(shí)驗(yàn)效果評(píng)估,并提出了基于Promela語言的領(lǐng)導(dǎo)選舉算法的建模方法,同時(shí)利用SPIN工具進(jìn)行偏序規(guī)約。
【關(guān)鍵詞】：模型檢測(cè) 偏序規(guī)約 頑固集 領(lǐng)導(dǎo)選舉
【學(xué)位授予單位】：貴州大學(xué)
【學(xué)位級(jí)別】：碩士
【學(xué)位授予年份】：2015
【分類號(hào)】：TP302.7
【目錄】：

• 摘要4-6
• Abstract6-8
• 第1章 緒論8-13
• 1.1 研究背景8-9
• 1.2 研究現(xiàn)狀9-10
• 1.3 研究目的及意義10-11
• 1.4 本人工作11
• 1.5 論文結(jié)構(gòu)安排11-13
• 第2章 并發(fā)系統(tǒng)的形式化規(guī)約及模型檢測(cè)13-31
• 2.1 軟件系統(tǒng)建模13-18
• 2.1.1 并發(fā)系統(tǒng)13-14
• 2.1.2 狀態(tài)和狀態(tài)空間14-16
• 2.1.3 變遷系統(tǒng)與粒度16-18
• 2.2 形式化分析18-20
• 2.2.1 形式化方法18-19
• 2.2.2 并發(fā)系統(tǒng)的形式化描述19-20
• 2.3 模型檢測(cè)20-24
• 2.3.1 自動(dòng)機(jī)20-22
• 2.3.2 模型檢測(cè)過程22-23
• 2.3.3 模型檢測(cè)的優(yōu)缺點(diǎn)23-24
• 2.4 基于TLA+數(shù)學(xué)實(shí)例的形式化規(guī)約24-27
• 2.4.1 TLA和TLA+24-25
• 2.4.2 使用TLA+的數(shù)學(xué)實(shí)例規(guī)約25-27
• 2.5 狀態(tài)爆炸問題27-30
• 2.6 本章小結(jié)30-31
• 第3章 利用偏序規(guī)約解決狀態(tài)爆炸問題31-46
• 3.1 偏序規(guī)約31-32
• 3.2 獨(dú)立變遷與跡理論32-34
• 3.3 選擇性搜索與并發(fā)系統(tǒng)中的獨(dú)立性34-36
• 3.4 相關(guān)偏序算法36-43
• 3.4.1 充足集36-37
• 3.4.2 持久集（算法a）37-39
• 3.4.3 條件頑固集（算法b）39-43
• 3.5 持久集和頑固集的算法比較和證明43-44
• 3.6 本章小結(jié)44-46
• 第4章 基于頑固集和對(duì)稱約簡(jiǎn)技術(shù)的Petri網(wǎng)模型檢測(cè)方法46-55
• 4.1 Petri網(wǎng)46-47
• 4.2 對(duì)稱約簡(jiǎn)技術(shù)47-48
• 4.3 結(jié)合對(duì)稱性和頑固集進(jìn)行狀態(tài)空間約簡(jiǎn)48-54
• 4.3.1 工具LoLA簡(jiǎn)介48-49
• 4.3.2 基于讀寫互斥算法的檢測(cè)及結(jié)果分析49-54
• 4.4 本章小結(jié)54-55
• 第5章 基于偏序規(guī)約的SPIN模型檢測(cè)及應(yīng)用實(shí)例55-63
• 5.1 偏序方法的評(píng)估及SPIN的使用55-57
• 5.2 基于領(lǐng)導(dǎo)選舉協(xié)議的偏序規(guī)約57-61
• 5.2.1 領(lǐng)導(dǎo)選舉算法介紹57-58
• 5.2.2 對(duì)領(lǐng)導(dǎo)選舉算法進(jìn)行建模規(guī)約與檢測(cè)58-61
• 5.3 本章小結(jié)61-63
• 第6章 總結(jié)與展望63-65
• 6.1 本文工作總結(jié)63
• 6.2 展望63-65
• 致謝65-66
• 參考文獻(xiàn)66-69
• 附錄 A：作者在攻讀碩士學(xué)位期間的學(xué)術(shù)論文及參與的科研項(xiàng)目69-70

【參考文獻(xiàn)】

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

1 楊琛;房鼎益;陳曉江;;一種有效的分布式構(gòu)件交互性質(zhì)驗(yàn)證方法[J];西北大學(xué)學(xué)報(bào)(自然科學(xué)版);2007年03期

2 馮登國(guó),范紅;安全協(xié)議形式化分析理論與方法研究綜述[J];中國(guó)科學(xué)院研究生院學(xué)報(bào);2003年04期

，

本文編號(hào)：1015994