本文關(guān)鍵詞：基于μ-演算的局部模型檢測算法設(shè)計，，由筆耕文化傳播整理發(fā)布。

【摘要】：隨著計算機軟件系統(tǒng)、硬件系統(tǒng)的發(fā)展,系統(tǒng)也變得越來越復(fù)雜,因此設(shè)法保證系統(tǒng)的正確性和可靠性變得越來越重要。為此,許多學(xué)者投入到該問題的研究中,并提出了很多理論與方法,模型檢測因高度自動化而引起了學(xué)者的關(guān)注。模型檢測是一種形式化驗證技術(shù)。其過程就是通過對系統(tǒng)建立模型,然后驗證該模型是否滿足給定的性質(zhì)。在模型檢測常用的邏輯中,命題μ-演算吸引了很多學(xué)者的興趣,它是由Kozen提出的,是個表達能力很強的邏輯語言,其較強的表達能力主要來自于最大不動點算子和最小不動點算子的交替嵌套。由于命題μ-演算有著較強的表達能力,因此其它一些邏輯驗證都可以轉(zhuǎn)換為命題μ-演算來驗證,而且驗證效率也較高。模型檢測需要對系統(tǒng)狀態(tài)空間進行窮舉搜索,驗證并發(fā)系統(tǒng)時,其狀態(tài)數(shù)是呈指數(shù)增長的。目前已經(jīng)有許多關(guān)于命題μ-演算的模型檢測算法,這些算法可以分為全局模型檢測算法和局部模型檢測算法。對于命題μ-演算,目前已知的最好的局部模型檢測算法的時間復(fù)雜度與交替嵌套深度d呈指數(shù)關(guān)系,其復(fù)雜度較高,本文將對其不動點交替嵌套迭代過程進行分析,提出時間復(fù)雜度較低的局部模型檢測算法。本文從命題μ-演算出發(fā),研究不動點交替嵌套迭代的中間結(jié)果之間的偏序關(guān)系,設(shè)計高效的局部模型檢測算法,并對算法的復(fù)雜度進行研究分析。本文主要分為三個部分:第一部分主要分析基于命題μ-演算的局部模型檢測算法,對其不動點交替嵌套迭代過程進行分析,然后從三支決策的角度改進算法。第二部分主要分析不動點交替嵌套迭代過程的中間結(jié)果之間的一組偏序關(guān)系,并根據(jù)該關(guān)系設(shè)計了一個局部模型檢測算法。第三部分主要開發(fā)設(shè)計了模型檢測器MuFPAL-MC的詞法語法分析器模塊,并闡述了模型檢測器MuFPAL-MC的研究框架。
【關(guān)鍵詞】：局部模型檢測 命題μ-演算 復(fù)雜度 不動點
【學(xué)位授予單位】：閩南師范大學(xué)
【學(xué)位級別】：碩士
【學(xué)位授予年份】：2016
【分類號】：O141.1
【目錄】：

• 摘要5-6
• Abstract6-10
• 第1章 緒論10-18
• 1.1 研究背景及意義10-13
• 1.2 國內(nèi)外研究現(xiàn)狀13-15
• 1.3 主要工作和結(jié)構(gòu)安排15-18
• 1.3.1 主要工作16
• 1.3.2 結(jié)構(gòu)安排16-18
• 第2章 基礎(chǔ)知識18-26
• 2.1 命題 μ-演算18-20
• 2.2 分區(qū)依賴圖20-21
• 2.3 界程演算21-23
• 2.4 界程邏輯23-25
• 2.5 三支決策25-26
• 第3章 三支決策視角的局部模型檢測26-36
• 3.1 m -演算局部模型檢測過程分析26-30
• 3.2 三支決策視角的模型檢測算法30-32
• 3.3 算法的對比分析32-34
• 3.4 本章小結(jié)34-36
• 第4章 基于一組偏序關(guān)系的局部模型檢測36-50
• 4.1 算法分析36-43
• 4.2 算法設(shè)計43-45
• 4.3 復(fù)雜度分析45-49
• 4.3.1 時間復(fù)雜度45-48
• 4.3.2 空間復(fù)雜度48
• 4.3.3 復(fù)雜度對比48-49
• 4.4 本章小結(jié)49-50
• 第5章 模型檢測器MuFPAL-MC的詞法語法分析器的開發(fā)設(shè)計50-66
• 5.1 MuFPAL-MC模型檢測器概述50-58
• 5.1.1 需求分析50-53
• 5.1.2 總體結(jié)構(gòu)53-54
• 5.1.3 界程演算的描述方式54-55
• 5.1.4 界程邏輯公式的描述方式55-57
• 5.1.5 系統(tǒng)內(nèi)部模塊57-58
• 5.2 詞法分析器58-60
• 5.3 語法分析器60-62
• 5.4 簡單實例測試62-63
• 5.5 本章小結(jié)63-66
• 第6章 總結(jié)和展望66-68
• 6.1 總結(jié)66
• 6.2 展望66-68
• 參考文獻68-78
• 致謝78-80
• 第I條 攻讀學(xué)位期間取得的科研成果80

【相似文獻】

中國期刊全文數(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

本文編號：487032