發(fā)布時(shí)間：2017-08-12 15:38

  本文關(guān)鍵詞：基于抽象和學(xué)習(xí)的統(tǒng)計(jì)模型檢測(cè)研究

  更多相關(guān)文章： 信息物理融合系統(tǒng) 隨機(jī)混成自動(dòng)機(jī) 主成分分析 統(tǒng)計(jì)抽象 統(tǒng)計(jì)模型檢測(cè)

【摘要】：信息物理融合系統(tǒng)(Cyber Physical Systems, CPS)是一種更關(guān)注計(jì)算機(jī)與物理環(huán)境交互和協(xié)作的高級(jí)嵌入式系統(tǒng),自2006年此概念被提出以來(lái),已受到了學(xué)術(shù)界與工業(yè)界的高度關(guān)注。第一,CPS應(yīng)用大都安全攸關(guān)或功耗要求嚴(yán)苛,在保證功能的前提下,仍必須滿足一定的非功能屬性,如吞吐量、能耗等,因此需要驗(yàn)證分析以保證其可信性；第二,CPS大都是異構(gòu)的混成系統(tǒng),融合了連續(xù)的物理過(guò)程和離散的系統(tǒng)行為,且處于高度不確定的開(kāi)放環(huán)境中,因此使用傳統(tǒng)的方法(如模型檢測(cè)和定理證明)難以完成驗(yàn)證分析。為緩解此問(wèn)題,人們開(kāi)始嘗試使用統(tǒng)計(jì)算法對(duì)系統(tǒng)模型的仿真Trace進(jìn)行分析,求得近似結(jié)果,并給出結(jié)果的誤差范圍，這種方法被稱為統(tǒng)計(jì)模型檢測(cè)(Statistical Model Checking, SMC)。SMC無(wú)需遍歷狀態(tài)空間,但當(dāng)結(jié)果精度要求較高時(shí)需要產(chǎn)生大量Trace(多數(shù)仿真軟件的Trace生成比較耗時(shí)),性能因此大大降低,本文即針對(duì)SMC的性能問(wèn)題展開(kāi)深入研究。首先,對(duì)已有SMC算法的原理進(jìn)行了剖析,實(shí)現(xiàn)了4種SMC算法,通過(guò)大量實(shí)驗(yàn)給出了詳細(xì)的性能評(píng)估。基于實(shí)驗(yàn)結(jié)論,提出了一個(gè)自適應(yīng)的SMC算法框架,以根據(jù)不同屬性的預(yù)估概率,動(dòng)態(tài)地選擇合適的SMC算法。其次,為改進(jìn)自適應(yīng)的SMC中貝葉斯區(qū)間估計(jì)算法的不足,提出了基于抽象和學(xué)習(xí)的SMC方法,旨在減少統(tǒng)計(jì)分析所需的Trace數(shù)量以提高SMC的效率。其中結(jié)合已有的抽象和學(xué)習(xí)理論(如主成分分析、隨機(jī)文法推斷),對(duì)隨機(jī)混成自動(dòng)機(jī)的仿真Trace進(jìn)行了概率等價(jià)抽象和簡(jiǎn)化；并基于抽象Trace學(xué)習(xí)出概率等價(jià)的系統(tǒng)行為模型-—前綴頻率樹(shù),同時(shí)提出了樹(shù)的兩階段約減算法,以有效控制樹(shù)的規(guī)模,為更高效的SMC驗(yàn)證分析提供了良好的抽象模型。最后,介紹了我們實(shí)現(xiàn)的CPS建模分析平臺(tái)-—Modana,基于此平臺(tái)實(shí)現(xiàn)了本文提出的SMC改進(jìn)算法,基于Modana平臺(tái)建模分析了典型的CPS系統(tǒng)-—智能溫控系統(tǒng)；并結(jié)合3個(gè)基準(zhǔn)測(cè)試案例,對(duì)SMC算法改進(jìn)前后的性能和準(zhǔn)確度進(jìn)行了實(shí)驗(yàn)性評(píng)估。結(jié)果證明,本文提出的SMC改進(jìn)方法正確并且有效。
【關(guān)鍵詞】：信息物理融合系統(tǒng) 隨機(jī)混成自動(dòng)機(jī) 主成分分析 統(tǒng)計(jì)抽象 統(tǒng)計(jì)模型檢測(cè)
【學(xué)位授予單位】：華東師范大學(xué)
【學(xué)位級(jí)別】：碩士
【學(xué)位授予年份】：2016
【分類號(hào)】：O212.1;TP273
【目錄】：

• 摘要6-7
• ABSTRACT7-12
• 第一章 緒論12-21
• 1.1 研究背景及意義12-14
• 1.2 國(guó)內(nèi)外研究現(xiàn)狀14-18
• 1.2.1 CPS的形式化建模14-15
• 1.2.2 統(tǒng)計(jì)模型檢測(cè)15-17
• 1.2.3 基于學(xué)習(xí)的統(tǒng)計(jì)模型檢測(cè)17-18
• 1.3 本文研究?jī)?nèi)容18-19
• 1.4 本文組織結(jié)構(gòu)19-20
• 1.5 本章小結(jié)20-21
• 第二章 預(yù)備知識(shí)與概念21-26
• 2.1 隨機(jī)行為21-22
• 2.2 隨機(jī)混成自動(dòng)機(jī)22-24
• 2.3 概率有界線性時(shí)態(tài)邏輯24-25
• 2.4 本章小結(jié)25-26
• 第三章 統(tǒng)計(jì)模型檢測(cè)算法的分析與集成26-43
• 3.1 統(tǒng)計(jì)模型檢測(cè)算法的原理剖析27-33
• 3.1.1 定性類SMC算法28-31
• 3.1.2 定量類SMC算法31-33
• 3.2 統(tǒng)計(jì)模型檢測(cè)算法的性能評(píng)估33-39
• 3.2.1 關(guān)于SMC算法性能的討論33-34
• 3.2.2 定性類SMC算法34-36
• 3.2.3 定量類SMC算法36-39
• 3.3 自適應(yīng)的統(tǒng)計(jì)模型檢測(cè)框架39-42
• 3.4 本章小結(jié)42-43
• 第四章 基于抽象和學(xué)習(xí)的統(tǒng)計(jì)模型檢測(cè)43-64
• 4.1 抽象階段Ⅰ：基于屬性的投影45-48
• 4.2 學(xué)習(xí)及抽象階段Ⅱ：基于主成分分析的特征降維48-50
• 4.3 抽象階段Ⅲ：關(guān)鍵點(diǎn)抽取50-52
• 4.3.1 啟發(fā)式優(yōu)化過(guò)程(可選)52
• 4.4 學(xué)習(xí)階段Ⅳ：前綴頻率樹(shù)的構(gòu)建與約簡(jiǎn)52-59
• 4.4.1 進(jìn)一步構(gòu)建概率有限自動(dòng)機(jī)(可選)55-59
• 4.5 最終概率的統(tǒng)計(jì)分析59-61
• 4.6 算法正確性與復(fù)雜度分析61-62
• 4.7 本章小結(jié)62-64
• 第五章 基于Modana平臺(tái)的SMC實(shí)現(xiàn)64-71
• 5.1 Modana平臺(tái)概述64-65
• 5.2 AL-SMC算法實(shí)現(xiàn)65-69
• 5.2.1 類與函數(shù)65-68
• 5.2.2 執(zhí)行流程與界面展示68-69
• 5.3 本章小結(jié)69-71
• 第六章 案例分析與實(shí)驗(yàn)評(píng)估71-81
• 6.1 智能溫控系統(tǒng)的建模與分析71-76
• 6.1.1 系統(tǒng)模型的建立73-75
• 6.1.2 不舒適度與能耗分析75-76
• 6.2 AL-SMC的性能和準(zhǔn)確度評(píng)估76-79
• 6.3 本章小結(jié)79-81
• 第七章 總結(jié)與展望81-83
• 參考文獻(xiàn)83-90
• 致謝90-91
• 發(fā)表論文和科研情況91

【相似文獻(xiàn)】

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

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

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

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

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

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

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

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

8 王扣武;張s，

本文編號(hào)：662384