本文關鍵詞：基于矩陣半張量積模型檢測算法的研究與實現(xiàn)，由筆耕文化傳播整理發(fā)布。

【摘要】：在計算機科學迅猛發(fā)展的今天,云計算、物聯(lián)網(wǎng)、移動互聯(lián)網(wǎng)成了時代的標志,這些軟件技術的高速發(fā)展對自身驗證的可靠性和硬件性能提出了挑戰(zhàn),對于硬件的性能要求最終落到了硬件集成電路的可靠性上面。然而,在硬件發(fā)展的歷程中,驗證集成芯片的正確性和可靠性一直是一個瓶頸。在驗證領域使用最多的是基于模擬的驗證方式,這種檢驗方式存在其不可彌補的缺點,即它只能證明系統(tǒng)有錯,而不能證明系統(tǒng)設計的正確性。而在軟件方面,對于可靠性的驗證還處于沒有形成特定規(guī)范的階段。所以無論是針對軟件還是硬件,對其可靠性的驗證都是有實質(zhì)意義的。本文主要以半張量積為數(shù)學理論,研究一種基于半張量積的模型檢測算法。算法主要分為三個部分:被驗證系統(tǒng)的數(shù)學建模、被驗證系統(tǒng)需要滿足的屬性描述和模型檢測算法。針對被驗證系統(tǒng)數(shù)學建模,首先根據(jù)被驗證系統(tǒng)的原子集合,固定原子公式順序,考查原子公式的取值,確定原子公式在系統(tǒng)狀態(tài)的取值情況,定義系統(tǒng)狀態(tài)的布爾編碼表示。然后使用矩陣半張量積的邏輯抽象方法對系統(tǒng)狀態(tài)向量化,得到系統(tǒng)的狀態(tài)向量。根據(jù)規(guī)定系統(tǒng)狀態(tài)的順序,利用圖論的鄰接矩陣定義被驗證系統(tǒng)的結構矩陣。最后使用向量乘法描述系統(tǒng)運行狀態(tài),并給出模型檢測算法的正確性和有窮性的數(shù)學證明。本算法對被檢測的屬性的描述采用分支時態(tài)邏輯的計算樹邏輯,因此分析了計算樹邏輯(Computation Tree Logic,CTL)的適當集,選取相應的適當集對任意CTL公式進行標準化描述。針對CTL的適當集的原子語義EX、EG和EU分別給出了驗證算法描述,再被驗證系統(tǒng)需要滿足的屬性描述對任意CTL公式表示進行屬性的復合語義驗證算法設計方案。論文最后給出了基于半張量積的模型檢測算法的應用實例分析,實現(xiàn)了從屬性分析、模型建立到最后的驗證,并完成了實例的驗證工作。從應用實例表明,本算法不僅可以應用于軟件系統(tǒng)和硬件系統(tǒng)的驗證,還可以拓展到布爾網(wǎng)絡分析等其他研究領域。
【關鍵詞】：形式化驗證 Kripke結構 模型檢驗 驗證算法
【學位授予單位】：電子科技大學
【學位級別】：碩士
【學位授予年份】：2015
【分類號】：TP302.7
【目錄】：

• 摘要5-6
• Abstract6-9
• 第一章 緒論9-14
• 1.1 研究目的和意義9-10
• 1.2 國內(nèi)外相關研究現(xiàn)狀10-12
• 1.3 主要研究內(nèi)容12-13
• 1.4 章節(jié)安排13-14
• 第二章 相關知識背景14-28
• 2.1 集成電路的設計與驗證14-22
• 2.1.1 集成電路的設計層次14-17
• 2.1.2 模擬驗證和形式化驗證17-22
• 2.2 時態(tài)邏輯分類22-23
• 2.2.1 線性時態(tài)邏輯的表示方法22
• 2.2.2 計算樹邏輯的表示和意義22-23
• 2.3 矩陣的半張量積23-27
• 2.3.1 矩陣半張量積的定義23-26
• 2.3.2 半張量積的偽交換性26-27
• 2.4 本章小節(jié)27-28
• 第三章 系統(tǒng)建模與結構矩陣求解28-39
• 3.1 系統(tǒng)建模28-33
• 3.1.1 Kripke結構模型28-29
• 3.1.2 布爾邏輯的矩陣表示29-31
• 3.1.3 系統(tǒng)模型的矩陣化31-33
• 3.2 系統(tǒng)結構矩陣定義與求解33-38
• 3.2.1 Kripke狀態(tài)向量求解方法33-34
• 3.2.2 Kripke結構矩陣快速求解34-38
• 3.3 本章小結38-39
• 第四章 模型檢測算法實現(xiàn)39-54
• 4.1 符號模型檢測算法39-41
• 4.1.1 符號模型檢測標記算法39-40
• 4.1.2 二叉判斷圖的算法40-41
• 4.2 屬性的描述及分析41-44
• 4.2.1 屬性描述方法的選取41
• 4.2.2 使用時態(tài)邏輯描述規(guī)范41-43
• 4.2.3 時態(tài)邏輯等價性與規(guī)范化43-44
• 4.3 模型檢測算法的數(shù)學論證44-48
• 4.3.1 模型狀態(tài)轉(zhuǎn)移的實現(xiàn)44-46
• 4.3.2 n步轉(zhuǎn)移關系的表示46-48
• 4.3.3 Kripke結構網(wǎng)絡直徑和意義48
• 4.4 基于半張量積的驗證算法48-53
• 4.4.1 EX的設計與實現(xiàn)48-50
• 4.4.2 EG的設計與實現(xiàn)50-51
• 4.4.3 EU的設計與實現(xiàn)51-52
• 4.4.4 屬性的復合驗證設計與實現(xiàn)52-53
• 4.5 本章小結53-54
• 第五章 模型檢測算法應用實例分析54-71
• 5.1 系統(tǒng)的驗證實例分析54-60
• 5.1.1 例子分析54
• 5.1.2 屬性的分析和描述54-56
• 5.1.3 建立模型與求解56-58
• 5.1.4 驗證過程實現(xiàn)58-59
• 5.1.5 試驗環(huán)境與數(shù)據(jù)結果59-60
• 5.2 模型檢測算法的擴展應用分析60-69
• 5.2.1 布爾網(wǎng)絡傳統(tǒng)的矩陣形式60-63
• 5.2.2 布爾網(wǎng)絡結構矩陣的新求法63-65
• 5.2.3 布爾網(wǎng)絡與kripke的關系65-67
• 5.2.4 用新方法求解布爾網(wǎng)絡拓撲問題67-69
• 5.3 本章小結69-71
• 第六章 總結與展望71-73
• 6.1 全文總結71
• 6.2 下一步工作及展望71-73
• 致謝73-74
• 參考文獻74-77
• 攻讀碩士學位期間取得的成果77-78

【相似文獻】

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

1 戎玫;張廣泉;;模型檢測新技術研究[J];計算機科學;2003年05期

2 肖健宇;張德運;鄭衛(wèi)斌;;過程提取用于改善程序模型檢測的可伸縮性[J];西安交通大學學報;2006年06期

3 袁志斌;徐正權;王能超;;軟件模型檢測中的抽象[J];計算機科學;2006年07期

4 劉吉鋒;孫吉貴;;基于抽象-驗證-細化范例的軟件模型檢測[J];計算機科學;2006年12期

5 化志章;吳傳孫;揭安全;薛錦云;;軟件模型檢測新技術研究[J];微計算機信息;2007年36期

6 王飛明;胡元闖;董榮勝;;模型檢測研究進展[J];廣西科學院學報;2008年04期

7 鄺宏斌;羅貴明;;并行軟件模型檢測[J];計算機工程;2008年19期

8 何愷鐸;顧明;宋曉宇;李力;李江;;面向源代碼的軟件模型檢測及其實現(xiàn)[J];計算機科學;2009年01期

9 林璇;;模型檢測方法在入侵檢測中的應用研究[J];現(xiàn)代計算機(專業(yè)版);2009年02期

10 顧濱兵;;一種軟件模型檢測方法及其原型系統(tǒng)[J];微計算機應用;2010年11期

中國重要會議論文全文數(shù)據(jù)庫 前5條

1 高靜;曹子寧;;基于空間邏輯和計算樹邏輯的模型檢測[A];2009年中國高校通信類院系學術研討會論文集[C];2009年

2 許梅;曹子寧;;基于謂詞μ演算和空間邏輯的模型檢測算法研究[A];2009年中國高校通信類院系學術研討會論文集[C];2009年

3 何青;駱翔宇;蘇開樂;;對弈必勝策略的符號化模型檢測[A];2006年全國理論計算機科學學術年會論文集[C];2006年

4 王飛明;胡元闖;董榮勝;;模型檢測中狀態(tài)爆炸及其優(yōu)化策略研究[A];廣西計算機學會2008年年會論文集[C];2008年

5 陳道喜;張廣泉;陳冬火;;NSPK協(xié)議的Spin模型檢測[A];2008年全國開放式分布與并行計算機學術會議論文集(下冊)[C];2008年

中國博士學位論文全文數(shù)據(jù)庫 前10條

1 江華;界程演算模型檢測[D];貴州大學;2008年

2 林榮德;移動界程演算及模型檢測應用的關鍵問題研究[D];華南理工大學;2010年

3 劉劍;傳值進程與移動進程的模型檢測方法[D];中國科學院研究生院（軟件研究所）;2005年

4 劉志鋒;模型檢測中關鍵技術的研究及其應用[D];南京大學;2011年

5 朱維軍;時間區(qū)間時序邏輯模型檢測：理論、算法及應用[D];西安電子科技大學;2011年

6 尹良澤;基于SAT的組合遷移系統(tǒng)模型檢測技術研究[D];清華大學;2014年

7 陳冬火;超協(xié)調(diào)時序邏輯及其模型檢測方法[D];中國科學院研究生院（成都計算機應用研究所）;2006年

8 田聰;命題投影時序邏輯的判定性、復雜性、表達性及模型檢測[D];西安電子科技大學;2010年

9 黃宏濤;基于懶惰切片的模型檢測技術研究[D];哈爾濱工程大學;2012年

10 劉金卓;基于符號化模型檢測的軟件演化過程模型驗證[D];云南大學;2013年

中國碩士學位論文全文數(shù)據(jù)庫 前10條

1 李永亮;基于DNA計算的CTL模型檢測方法研究[D];鄭州大學;2015年

2 楊樹峰;基于統(tǒng)計模型檢測的無線傳感器網(wǎng)絡協(xié)議建模與分析[D];鄭州大學;2015年

3 張興興;基于廣義可能性測度的互模擬及CTL不動點語義[D];陜西師范大學;2015年

4 王彬;基于多值模型檢測的SaaS應用測試及其自動化研究[D];陜西師范大學;2015年

5 王凱;基于模型檢測多反例對軟件進行調(diào)試[D];電子科技大學;2015年

6 鄧楠軼;基于廣義可能性測度的模型檢測器GPoCheck的設計與實現(xiàn)[D];陜西師范大學;2015年

7 張恒;多值模型檢測器的研究與實現(xiàn)[D];陜西師范大學;2015年

8 高毅;不同模型檢測下信號并串轉(zhuǎn)換模塊功能建模的研究[D];電子科技大學;2014年

9 崔曉爽;基于GSTE模型檢測的信號并串轉(zhuǎn)換模塊功能驗證的研究[D];電子科技大學;2014年

10 許落汀;基于BDDs的離散實時時態(tài)邏輯RTCTL*的符號化模型檢測及證據(jù)生成[D];華僑大學;2015年

  本文關鍵詞：基于矩陣半張量積模型檢測算法的研究與實現(xiàn)，由筆耕文化傳播整理發(fā)布。

，

本文編號：402565