本文關(guān)鍵詞：構(gòu)件系統(tǒng)模型檢測(cè)方法研究

  更多相關(guān)文章： 構(gòu)件系統(tǒng) 模型檢測(cè) 抽象方法

【摘要】：構(gòu)件系統(tǒng)被廣泛應(yīng)用于許多工業(yè)領(lǐng)域,全面的分析其行為和正確性具有現(xiàn)實(shí)需求和意義�，F(xiàn)已有對(duì)該系統(tǒng)交互及隨機(jī)行為正確性進(jìn)行驗(yàn)證的符號(hào)化、組合和統(tǒng)計(jì)模型檢測(cè)方法。由于構(gòu)件系統(tǒng)中變量較多,容易引起驗(yàn)證的狀態(tài)空間爆炸問(wèn)題;而使用抽象技術(shù)時(shí),驗(yàn)證是不完備的。針對(duì)以上問(wèn)題,圍繞對(duì)構(gòu)件系統(tǒng)中變量的處理,本文提出了一些模型檢測(cè)方法,并將它們用于實(shí)際案例的的驗(yàn)證。本文的主要貢獻(xiàn)如下:?本文提出了基于變量劃分的符號(hào)化模型檢測(cè)方法。該方法對(duì)分離遷移表達(dá)式中的變量集合進(jìn)行劃分,將其分為值變化和值不變的兩個(gè)子集。使用該方法進(jìn)行構(gòu)件系統(tǒng)符號(hào)化模型檢測(cè)時(shí),只需要對(duì)遷移上值變化的變量進(jìn)行處理,有效地減少了時(shí)間和內(nèi)存開(kāi)銷。?本文針對(duì)組合抽象構(gòu)件系統(tǒng)不變式驗(yàn)證的不完備問(wèn)題,提出了不變式增強(qiáng)和狀態(tài)劃分兩種精化方法。不變式增強(qiáng)方法主要用于去除系統(tǒng)偽反例,并生成增強(qiáng)不變式精化原系統(tǒng)不變式;狀態(tài)劃分方法主要利用反例對(duì)抽象狀態(tài)進(jìn)行劃分,生成新?tīng)顟B(tài)對(duì)抽象系統(tǒng)進(jìn)行精化。將上述兩種精化方法融入到組合抽象方法中,本文提出了構(gòu)件系統(tǒng)抽象精化組合模型檢測(cè)算法,并證明了該算法的完備性和有效性。?為了對(duì)隨機(jī)構(gòu)件模型行為屬性進(jìn)行概率分析和檢測(cè),本文設(shè)計(jì)并實(shí)現(xiàn)了模型翻譯和基于模塊的系統(tǒng)組合方法,其保留了原模型的概率信息和構(gòu)件系統(tǒng)的組合特性。本文使用概率變量分布離散化方法對(duì)復(fù)雜模型進(jìn)行抽象,并對(duì)抽象模型的概率模型檢測(cè)和原模型的統(tǒng)計(jì)模型檢測(cè)方法進(jìn)行比較和分析。?為了分析帶權(quán)隨機(jī)構(gòu)件系統(tǒng)期望的性質(zhì),針對(duì)已有i LTL方法只能對(duì)非周期Markov模型進(jìn)行驗(yàn)證的問(wèn)題,本文提出了對(duì)周期Markov模型的概率質(zhì)量函數(shù)(pmf)序列的時(shí)序?qū)傩赃M(jìn)行基于可行解的模型檢測(cè)方法——ip LTL。上述驗(yàn)證方法使用了抽象技術(shù),將pmf作為模型狀態(tài)。當(dāng)待驗(yàn)證屬性不成立時(shí),該方法將給出反例,即模型的初始pmf。從該初始pmf出發(fā),可以對(duì)違反屬性的系統(tǒng)運(yùn)行進(jìn)行分析。
【關(guān)鍵詞】：構(gòu)件系統(tǒng) 模型檢測(cè) 抽象方法
【學(xué)位授予單位】：清華大學(xué)
【學(xué)位級(jí)別】：博士
【學(xué)位授予年份】：2015
【分類號(hào)】：O213
【目錄】：

• 摘要3-4
• Abstract4-9
• 第1章 緒論9-21
• 1.1 研究對(duì)象9-11
• 1.2 研究目標(biāo)11-13
• 1.3 相關(guān)研究工作13-18
• 1.3.1 符號(hào)化模型檢測(cè)13-14
• 1.3.2 組合模型檢測(cè)14-16
• 1.3.3 統(tǒng)計(jì)模型檢測(cè)16-17
• 1.3.4 概率模型檢測(cè)17
• 1.3.5 模型檢測(cè)工具17-18
• 1.4 研究思路18-20
• 1.5 論文貢獻(xiàn)20
• 1.6 論文結(jié)構(gòu)20-21
• 第2章 構(gòu)件系統(tǒng)21-30
• 2.1 引言21-22
• 2.2 構(gòu)件系統(tǒng)22-24
• 2.3 隨機(jī)構(gòu)件系統(tǒng)24-27
• 2.4 帶權(quán)隨機(jī)構(gòu)件系統(tǒng)27-29
• 2.5 本章小結(jié)29-30
• 第3章 構(gòu)件系統(tǒng)符號(hào)化模型檢測(cè)30-41
• 3.1 引言30-31
• 3.2 符號(hào)化模型檢測(cè)31-33
• 3.2.1 符號(hào)化模型檢測(cè)31-32
• 3.2.2 分離遷移表達(dá)式方法32
• 3.2.3 變量劃分方法32-33
• 3.3 構(gòu)件系統(tǒng)符號(hào)化模型33-34
• 3.4 構(gòu)件系統(tǒng)符號(hào)化模型檢測(cè)34-36
• 3.4.1 構(gòu)件系統(tǒng)變量劃分34-35
• 3.4.2 變量劃分符號(hào)化算法35-36
• 3.5 案例及實(shí)驗(yàn)結(jié)果分析36-40
• 3.6 本章小結(jié)40-41
• 第4章 構(gòu)件系統(tǒng)抽象精化組合模型檢測(cè)41-64
• 4.1 引言41-43
• 4.2 組合抽象構(gòu)件系統(tǒng)模型檢測(cè)43-48
• 4.2.1 組合驗(yàn)證規(guī)則43-47
• 4.2.2 組合驗(yàn)證的不完備性問(wèn)題分析47-48
• 4.3 精化方法48-52
• 4.3.1 不變式增強(qiáng)48-49
• 4.3.2 狀態(tài)劃分49-52
• 4.4 構(gòu)件系統(tǒng)驗(yàn)證框架52-56
• 4.5 案例分析56-62
• 4.5.1 車門控制系統(tǒng)56-57
• 4.5.2 溫度控制系統(tǒng)57-62
• 4.6 本章小結(jié)62-64
• 第5章 隨機(jī)構(gòu)件系統(tǒng)概率分析和檢測(cè)64-79
• 5.1 引言64-65
• 5.2 PRISM建模語(yǔ)言65-66
• 5.3 隨機(jī)構(gòu)件系統(tǒng)模型翻譯66-69
• 5.4 構(gòu)件系統(tǒng)隨機(jī)行為分析69-77
• 5.4.1 時(shí)鐘同步協(xié)議案例70-72
• 5.4.2 統(tǒng)計(jì)模型檢測(cè)72-73
• 5.4.3 模型抽象73-74
• 5.4.4 概率模型檢測(cè)74-75
• 5.4.5 MPEG2播放器案例75-77
• 5.5 本章小結(jié)77-79
• 第6章 基于可行解的隨機(jī)構(gòu)件系統(tǒng)模型檢測(cè)79-96
• 6.1 引言79-80
• 6.2 隨機(jī)構(gòu)件系統(tǒng)語(yǔ)義分析80-81
• 6.3 iLTL模型檢測(cè)81-84
• 6.4 ipLTL模型檢測(cè)84-93
• 6.4.1 (k, d)-Markov模型及其收斂性分析84-88
• 6.4.2 ip LTL的語(yǔ)法和語(yǔ)義88-89
• 6.4.3 ip LTL模型檢測(cè)89-93
• 6.5 案例分析93-94
• 6.6 本章小結(jié)94-96
• 第7章 結(jié)束語(yǔ)96-98
• 7.1 工作總結(jié)96-97
• 7.2 研究展望97-98
• 參考文獻(xiàn)98-105
• 致謝105-107
• 個(gè)人簡(jiǎn)歷、在學(xué)期間發(fā)表的學(xué)術(shù)論文與研究成果107

【相似文獻(xiàn)】

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

1 黎云祥，劉玉成，，鐘章成;植物種群生態(tài)學(xué)中的構(gòu)件理論[J];生態(tài)學(xué)雜志;1995年06期

中國(guó)重要報(bào)紙全文數(shù)據(jù)庫(kù) 前1條

1 盧捍華 劉建星;NGOSS：運(yùn)營(yíng)支撐系統(tǒng)的新框架[N];通信產(chǎn)業(yè)報(bào);2003年

中國(guó)博士學(xué)位論文全文數(shù)據(jù)庫(kù) 前2條

1 張連怡;構(gòu)件系統(tǒng)模型檢測(cè)方法研究[D];清華大學(xué);2015年

2 黃杰;分布構(gòu)件系統(tǒng)故障診斷技術(shù)研究[D];國(guó)防科學(xué)技術(shù)大學(xué);2005年

中國(guó)碩士學(xué)位論文全文數(shù)據(jù)庫(kù) 前6條

1 蘇萍;面向動(dòng)態(tài)更新的構(gòu)件依賴自動(dòng)管理技術(shù)研究[D];南京大學(xué);2014年

2 陳昀林;艦載分布式構(gòu)件系統(tǒng)的容錯(cuò)技術(shù)研究[D];中國(guó)艦船研究院;2011年

3 解凱;構(gòu)件系統(tǒng)回歸測(cè)試模型與技術(shù)研究[D];東南大學(xué);2006年

4 劉偉乾;古文字構(gòu)件朝向研究[D];華東師范大學(xué);2011年

5 夏輝;基于EJB構(gòu)件系統(tǒng)的集成測(cè)試方法研究[D];西安理工大學(xué);2006年

6 郄曉淼;河北明代長(zhǎng)城碑刻文字研究[D];河北師范大學(xué);2015年

本文編號(hào)：1043500