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

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

【摘要】：隨著人們對軟硬件系統(tǒng)功能需求的日益增加,導(dǎo)致系統(tǒng)的規(guī)模越來越復(fù)雜,其安全性和可靠性也越來越難以得到保證。在一些關(guān)鍵領(lǐng)域,例如航空航天、銀行、證券等,軟件可靠性問題顯得尤為重要,已經(jīng)日益成為當(dāng)今研究的重要課題。在過去的三十幾年間,針對并發(fā)系統(tǒng)運行的不確定性,各國研究人員為解決可靠性問題做出了許多工作,其中,模型檢測驗證技術(shù)就是該領(lǐng)域中的熱點之一。模型檢測是一種形式化自動驗證技術(shù),它可以為許多軟件設(shè)計中的相關(guān)問題提出解決辦法。一般給定一個系統(tǒng)的形式化數(shù)學(xué)模型以及形式化的規(guī)約屬性,就可以使用模型檢測技術(shù)驗證該系統(tǒng)是否滿足屬性。自動檢測器的檢測結(jié)果要不證明該系統(tǒng)滿足該屬性,要不提供一個反例路徑。然而,對于許多類型的系統(tǒng)來說,隨著建模系統(tǒng)規(guī)模和進程數(shù)目的擴大,運行過程中可能產(chǎn)生的狀態(tài)數(shù)將呈指數(shù)級增長,這就引起了狀態(tài)爆炸問題。偏序規(guī)約技術(shù)就是為了緩解異步并發(fā)系統(tǒng)的狀態(tài)爆炸問題而產(chǎn)生的,該技術(shù)主要是構(gòu)建一個更小的狀態(tài)空間子集,而搜索時僅探測該狀態(tài)空間子集,并不是探測所有的并發(fā)交錯運行。本文中,我們對模型檢測技術(shù)和偏序規(guī)約技術(shù)進行深入的研究,主要工作如下:1、詳述了并發(fā)系統(tǒng)的形式化描述方法及模型檢測的一些基本原則,并研究如何使用TLA+語言對現(xiàn)實問題進行規(guī)約。2、研究了偏序規(guī)約的相關(guān)理論,同時對幾種約簡狀態(tài)空間的偏序規(guī)約算法進行深入研究,包括充足集(ample)、持久集(persistent)、條件頑固集(conditional stubborn)。3、基于條件頑固集和持久集的計算算法,通過集合理論證明了在相同條件下,有條件頑固集算法比持久集算法更加有效。4、結(jié)合使用頑固集和對稱性約簡技術(shù),在Petri網(wǎng)的建模工具基礎(chǔ)上,分析了讀寫互斥算法的約簡過程,通過工具LoLA進行實驗對比驗證。5、研究了偏序規(guī)約的實驗效果評估,并提出了基于Promela語言的領(lǐng)導(dǎo)選舉算法的建模方法,同時利用SPIN工具進行偏序規(guī)約。
【關(guān)鍵詞】：模型檢測 偏序規(guī)約 頑固集 領(lǐng)導(dǎo)選舉
【學(xué)位授予單位】：貴州大學(xué)
【學(xué)位級別】：碩士
【學(xué)位授予年份】：2015
【分類號】：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ī)約及模型檢測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 模型檢測20-24
• 2.3.1 自動機20-22
• 2.3.2 模型檢測過程22-23
• 2.3.3 模型檢測的優(yōu)缺點23-24
• 2.4 基于TLA+數(shù)學(xué)實例的形式化規(guī)約24-27
• 2.4.1 TLA和TLA+24-25
• 2.4.2 使用TLA+的數(shù)學(xué)實例規(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 獨立變遷與跡理論32-34
• 3.3 選擇性搜索與并發(fā)系統(tǒng)中的獨立性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章 基于頑固集和對稱約簡技術(shù)的Petri網(wǎng)模型檢測方法46-55
• 4.1 Petri網(wǎng)46-47
• 4.2 對稱約簡技術(shù)47-48
• 4.3 結(jié)合對稱性和頑固集進行狀態(tài)空間約簡48-54
• 4.3.1 工具LoLA簡介48-49
• 4.3.2 基于讀寫互斥算法的檢測及結(jié)果分析49-54
• 4.4 本章小結(jié)54-55
• 第5章 基于偏序規(guī)約的SPIN模型檢測及應(yīng)用實例55-63
• 5.1 偏序方法的評估及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 對領(lǐng)導(dǎo)選舉算法進行建模規(guī)約與檢測58-61
• 5.3 本章小結(jié)61-63
• 第6章 總結(jié)與展望63-65
• 6.1 本文工作總結(jié)63
• 6.2 展望63-65
• 致謝65-66
• 參考文獻66-69
• 附錄 A：作者在攻讀碩士學(xué)位期間的學(xué)術(shù)論文及參與的科研項目69-70

【參考文獻】

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

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

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

，

本文編號：1015994