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

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

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

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

【相似文獻】

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

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

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

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

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

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

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

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

8 王扣武;張s，

本文編號：662384