本文關(guān)鍵詞：面向復(fù)雜隨機(jī)系統(tǒng)的貝葉斯統(tǒng)計(jì)模型檢測方法，由筆耕文化傳播整理發(fā)布。

【摘要】：隨著網(wǎng)絡(luò)技術(shù)的成熟,加速了各類網(wǎng)絡(luò)設(shè)施、應(yīng)用和服務(wù)的發(fā)展,如移動互聯(lián)網(wǎng)、云計(jì)算等。它們滲透進(jìn)了人們生活的方方面面。越來越多的設(shè)施與應(yīng)用會建立在網(wǎng)絡(luò)之上。研究如何保證它們的正確性和可靠性就變成一個有意義的課題。不同于其他軟硬件系統(tǒng),網(wǎng)絡(luò)系統(tǒng)往往包含隨機(jī)性。雖然業(yè)界目前主要采用測試來保證軟硬件系統(tǒng)的正確性和可靠性。但是它也存在一些不足,如沒有把握保證檢測出系統(tǒng)所有的錯誤和其效果與測試者的經(jīng)驗(yàn)有較大關(guān)聯(lián)等。為更好地保證復(fù)雜隨機(jī)系統(tǒng)的正確性和可靠性,我們提出了一種基于預(yù)測的貝葉斯統(tǒng)計(jì)模型檢測方法(prediction-based Bayesian model checking)。從模型的初始狀態(tài)開始,隨機(jī)從模型中選擇一條有限路徑,并多次重復(fù)這個過程。由于有限路徑是相互獨(dú)立的,因此就能將所有的有限路徑看作為樣本,并通過貝葉斯推斷(Bayesian Inference)來推斷模型滿足性質(zhì)的概率。另外,我們利用貝葉斯統(tǒng)計(jì)學(xué)中先驗(yàn)分布與后驗(yàn)分布的共軛關(guān)系,在驗(yàn)證前預(yù)測所需樣本的數(shù)量上限。并且保證一旦抽樣數(shù)量達(dá)到該上限時,當(dāng)前的結(jié)果已經(jīng)達(dá)到了可信度與精度的要求,可立即返回。其次,根據(jù)之前所預(yù)測的上限,我們會在每次統(tǒng)計(jì)數(shù)據(jù)更新后,再次利用共軛關(guān)系來預(yù)測所有可能的推斷結(jié)果。當(dāng)所有可能的結(jié)果都與當(dāng)前結(jié)果一致時,便直接返回結(jié)果。為提高對一部分復(fù)雜系統(tǒng)的驗(yàn)證效率(運(yùn)行周期較長的隨機(jī)系統(tǒng)),我們另外提出了一種啟發(fā)式的抽樣與驗(yàn)證算法。它將路徑抽樣與路徑驗(yàn)證分開成兩個階段：在對路徑進(jìn)行驗(yàn)證時,嘗試?yán)盟惴▉矶ㄎ灰粋�“可判前綴”,而這個“可判前綴”能夠直接用來判定該路徑是否滿足性質(zhì)。而在后續(xù)的抽樣中,根據(jù)之前所收集的“可判前綴”信息,便可以直接判斷路徑是否滿足性質(zhì)。從而避免耗時的路徑驗(yàn)證。并且,它還可以與基于預(yù)測的貝葉斯統(tǒng)計(jì)模型檢測算法相結(jié)合。SPAC(Statistical Probabilistic Approximate model Checker)是基于上述算法所實(shí)現(xiàn)的統(tǒng)計(jì)模型檢測工具。通過SPAC對調(diào)度算法、分布式算法等案例進(jìn)行研究后,發(fā)現(xiàn)在一些場景下,該算法相對于其他統(tǒng)計(jì)模型檢測算法效率更高。并且對于運(yùn)行周期較長的系統(tǒng),啟發(fā)式算法也可以進(jìn)一步提高驗(yàn)證效率。
【關(guān)鍵詞】：統(tǒng)計(jì)模型檢測 復(fù)雜隨機(jī)系統(tǒng) 貝葉斯推斷 啟發(fā)式算法 預(yù)測 SPAC
【學(xué)位授予單位】：華東師范大學(xué)
【學(xué)位級別】：碩士
【學(xué)位授予年份】：2016
【分類號】：O212.8
【目錄】：

• 摘要6-8
• ABSTRACT8-15
• 第一章 緒論15-23
• 1.1 研究背景15-18
• 1.2 研究動機(jī)18-20
• 1.3 相關(guān)工作20-21
• 1.4 文章結(jié)構(gòu)21-23
• 第二章 背景知識23-28
• 2.1 模型定義與性質(zhì)描述23-25
• 2.1.1 離散時間馬爾可夫鏈與概率遷移系統(tǒng)23
• 2.1.2 事件的測度23-24
• 2.1.3 概率計(jì)算樹邏輯PCTL24-25
• 2.2 貝葉斯推斷25-27
• 2.2.1 貝葉斯推斷與先驗(yàn)信息25-26
• 2.2.2 貝葉斯推斷過程26-27
• 2.2.3 共軛先驗(yàn)分布定理27
• 2.3 本章小結(jié)27-28
• 第三章 基于預(yù)測的貝葉斯統(tǒng)計(jì)模型檢測方法28-57
• 3.1 基本介紹28-29
• 3.2 面向定性性質(zhì)的驗(yàn)證算法29-38
• 3.2.1 方法框架29-31
• 3.2.2 抽樣數(shù)量上限預(yù)測方法31-33
• 3.2.3 面向定性性質(zhì)的統(tǒng)計(jì)結(jié)果預(yù)測方法33-35
• 3.2.4 結(jié)果可信度計(jì)算方法35-36
• 3.2.5 算法描述36-38
• 3.3 面向定量性質(zhì)的檢測算法38-42
• 3.3.1 方法框架38
• 3.3.2 面向定量性質(zhì)的統(tǒng)計(jì)結(jié)果預(yù)測方法38-40
• 3.3.3 算法描述40-42
• 3.4 啟發(fā)式抽樣與驗(yàn)證算法42-54
• 3.4.1 方法框架42-43
• 3.4.2 一個基本觀察43-44
• 3.4.3 最短可判前綴44-49
• 3.4.4 啟發(fā)式抽樣與驗(yàn)證算法49-54
• 3.5 完整算法驗(yàn)證過程54-56
• 3.6 本章小結(jié)56-57
• 第四章 統(tǒng)計(jì)模型檢測工具SPAC57-63
• 4.1 工具介紹57-58
• 4.2 工具實(shí)現(xiàn)58-61
• 4.2.1 界面與配置模塊59
• 4.2.2 參數(shù)檢查模塊59
• 4.2.3 DTMC模型構(gòu)建模塊59-60
• 4.2.4 PCTL語法解析模塊60
• 4.2.5 統(tǒng)計(jì)模型檢測算法模塊60-61
• 4.2.6 有限路徑驗(yàn)證模塊61
• 4.3 本章小結(jié)61-63
• 第五章 案例研究63-83
• 5.1 基本介紹63
• 5.2 簡單隨機(jī)調(diào)度算法63-70
• 5.2.1 簡單隨機(jī)調(diào)度算法介紹64-65
• 5.2.2 算法正確性評估65-66
• 5.2.3 不同運(yùn)行周期下的驗(yàn)證效率評估66-67
• 5.2.4 指定不同先驗(yàn)分布時的驗(yàn)證效率評估67-69
• 5.2.5 不同概率閾值下的驗(yàn)證效率評估69-70
• 5.3 同步的領(lǐng)導(dǎo)者選舉協(xié)議70-76
• 5.3.1 同步的領(lǐng)導(dǎo)者選舉協(xié)議介紹70
• 5.3.2 面向定量性質(zhì)的驗(yàn)證效率評估70-72
• 5.3.3 指定不同先驗(yàn)分布時的驗(yàn)證效率評估72-73
• 5.3.4 不同概率閾值下的驗(yàn)證效率評估73-74
• 5.3.5 不同問題規(guī)模下的驗(yàn)證效率評估74-76
• 5.4 Herman分布式算法76-81
• 5.4.1 Herman分布式算法介紹76-78
• 5.4.2 面向定量性質(zhì)的驗(yàn)證效率評估78-79
• 5.4.3 不同運(yùn)行周期下的驗(yàn)證效率評估79-81
• 5.4.4 復(fù)雜問題的驗(yàn)證效率81
• 5.5 本章小結(jié)81-83
• 第六章 總結(jié)與展望83-85
• 6.1 總結(jié)83-84
• 6.2 展望84-85
• 附錄A 啟發(fā)式驗(yàn)證算法中的關(guān)鍵狀態(tài)定位算法85-88
• 附錄B 簡單隨機(jī)調(diào)度算法在PRISM中的模型定義88-90
• 附錄C 抽樣上限預(yù)測算法90-92
• 附錄D 同步領(lǐng)導(dǎo)者選舉協(xié)議在PRISM中的模型定義92-96
• 附錄E 讀碩士學(xué)會期間發(fā)表論文和科研情況96
• 附錄F 參與科研項(xiàng)目情況96-97
• 參考文獻(xiàn)97-102
• 致謝102

【相似文獻(xiàn)】

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

1 陳清亮;朱可宜;;多智能體協(xié)同的認(rèn)知規(guī)范模型檢測算法[J];中山大學(xué)學(xué)報(bào)(自然科學(xué)版);2009年01期

2 周從華;邢支虎;劉志鋒;王昌達(dá);;馬爾可夫決策過程的限界模型檢測[J];計(jì)算機(jī)學(xué)報(bào);2013年12期

3 吉猛;胡克瑾;;基于模型檢測的電子商務(wù)鑒證技術(shù)[J];陜西師范大學(xué)學(xué)報(bào)(自然科學(xué)版);2006年04期

4 寧正元;胡山立;賴賢偉;;交互時態(tài)信念邏輯及其模型檢測[J];南京大學(xué)學(xué)報(bào)(自然科學(xué)版);2008年02期

5 王曦;徐中偉;梅萌;;基于模型檢測的軟件安全性驗(yàn)證方法[J];武漢大學(xué)學(xué)報(bào)(理學(xué)版);2010年02期

6 王晶;張廣泉;;基于概率時間自動機(jī)的模型檢測反例表示研究[J];蘇州大學(xué)學(xué)報(bào)(自然科學(xué)版);2011年02期

7 高妍妍;李曦;周學(xué)海;;L4進(jìn)程間通信機(jī)制的模型檢測方法[J];中國科學(xué)院研究生院學(xué)報(bào);2011年06期

8 王扣武;張s，

本文編號：294656