本文關(guān)鍵詞：基于自動(dòng)機(jī)理論的高效模型檢驗(yàn)算法研究，，由筆耕文化傳播整理發(fā)布。

【摘要】：模型檢驗(yàn)是一種重要的自動(dòng)化驗(yàn)證技術(shù),基于狀態(tài)遍歷的思想窮舉系統(tǒng)能夠到達(dá)的所有狀態(tài),并在系統(tǒng)不滿足指定的性質(zhì)時(shí)提供反例。本文主要關(guān)注適用于軟件系統(tǒng)的基于自動(dòng)機(jī)理論的(顯式)模型檢驗(yàn)。給定一個(gè)系統(tǒng)模型,根據(jù)待檢驗(yàn)性質(zhì)的不同,需要采用不同的模型檢驗(yàn)算法驗(yàn)證系統(tǒng)是否滿足性質(zhì),主要包括可達(dá)性算法、精化檢驗(yàn)算法和面向時(shí)序邏輯模型檢驗(yàn)的空性檢驗(yàn)算法等。其中,精化檢驗(yàn)和空性檢驗(yàn)算法中還存在不少困難和挑戰(zhàn)：(1)精化檢驗(yàn)算法依賴于自動(dòng)機(jī)的子集構(gòu)造,容易引起狀態(tài)空間爆炸問題,是制約精化檢驗(yàn)應(yīng)用范圍的一個(gè)重要原因；(2)當(dāng)前精化檢驗(yàn)主要面向并發(fā)系統(tǒng),而對于更復(fù)雜的系統(tǒng),例如帶有時(shí)間約束的實(shí)時(shí)系統(tǒng)(通常用時(shí)間自動(dòng)機(jī)表示),還沒有成熟有效的算法能夠支持其精化檢驗(yàn)；(3)有窮自動(dòng)機(jī)的空性檢驗(yàn)算法已經(jīng)發(fā)展得比較成熟,然而時(shí)間自動(dòng)機(jī)的空性檢驗(yàn)需要進(jìn)一步考慮non-Zenoness問題(即在有限時(shí)間內(nèi)不能發(fā)生無窮多事件),目前還沒有高效的算法支持。針對上述困難和挑戰(zhàn),本文重點(diǎn)研究基于反鏈的精化檢驗(yàn)算法、時(shí)間自動(dòng)機(jī)的精化檢驗(yàn)算法,以及提出了一種新的基于non-Zenoness的時(shí)間自動(dòng)機(jī)空性檢驗(yàn)算法,主要工作和貢獻(xiàn)如下：1.針對精化檢驗(yàn)算法中子集構(gòu)造引起的狀態(tài)空間爆炸問題,本文首次將反鏈的思想引入到三類當(dāng)前主要的精化檢驗(yàn)算法中,提出了基于反鏈的路徑精化檢驗(yàn)、穩(wěn)定故障精化檢驗(yàn)和故障-偏差精化檢驗(yàn)算法,展示了如何消減滿足反鏈關(guān)系的狀態(tài),并證明了這三個(gè)算法的正確性。實(shí)驗(yàn)表明,基于反鏈的精化檢驗(yàn)算法性能大大優(yōu)于不使用反鏈的精化檢驗(yàn)算法,性能提升多達(dá)幾十倍。2.本文首次提出了時(shí)間自動(dòng)機(jī)的精化檢驗(yàn)算法,即給定兩個(gè)時(shí)間自動(dòng)機(jī),一個(gè)時(shí)間自動(dòng)機(jī)的語言是否包含于另一個(gè)時(shí)間自動(dòng)機(jī)。算法采用了時(shí)鐘域抽象這種目前最有效的抽象方法,得到有窮狀態(tài)空間,使算法能夠真正應(yīng)用于實(shí)際系統(tǒng)。算法還在一定程度上克服了時(shí)間自動(dòng)機(jī)確定化的不可判定性問題,即用理論以及實(shí)驗(yàn)證明了在絕大部分實(shí)際情況下算法是可以停止的。此外,算法還利用基于反鏈和上下界模擬關(guān)系的優(yōu)化方法進(jìn)一步提高算法性能。從實(shí)驗(yàn)結(jié)果可以得出,算法在實(shí)際系統(tǒng)的驗(yàn)證中表現(xiàn)出了良好的性能。3.本文提出了一種新的基于non-Zenoness的時(shí)間自動(dòng)機(jī)空性檢驗(yàn)算法.目前已存在的其他空性檢驗(yàn)算法由于在檢驗(yàn)non-Zenoness時(shí)需要引入額外的時(shí)鐘或者狀態(tài),使得狀態(tài)空間大大增加,算法性能往往十分低下。本文定義了一類特殊的時(shí)間自動(dòng)機(jī)CUB-TA,并且為其提出了一種無需引入其他狀態(tài)或時(shí)鐘的空性檢驗(yàn)算法,因此具有較高的效率。在此基礎(chǔ)上,本文又證明了任意時(shí)間自動(dòng)機(jī)都能夠轉(zhuǎn)化為CUB-TA,并提出了快速的轉(zhuǎn)化算法。實(shí)驗(yàn)表明,大部分實(shí)際系統(tǒng)本身就是CUB-TA,或者只需要很小的代價(jià)就能轉(zhuǎn)換成CUB-TA,因此本文提出的算法非常具有實(shí)用性。此外,本文的算法性能在大部分情況下高于其他算法。4.模型檢驗(yàn)的成功很大程度上得益于驗(yàn)證工具的支持。本文在模型驗(yàn)證工具PAT框架中實(shí)現(xiàn)了上述所有算法,并結(jié)合PAT工具本身對各種形式化建模語言和語言解析的支持,使得用戶可以方便地建模實(shí)際系統(tǒng)和待檢驗(yàn)性質(zhì),并進(jìn)行有效的驗(yàn)證。
【關(guān)鍵詞】：模型檢驗(yàn) 自動(dòng)機(jī) 精化檢驗(yàn) 反鏈 時(shí)間自動(dòng)機(jī) 空性檢驗(yàn) Non-Zenoness
【學(xué)位授予單位】：浙江大學(xué)
【學(xué)位級別】：博士
【學(xué)位授予年份】：2015
【分類號】：TP301.1
【目錄】：

• 摘要4-6
• Abstract6-14
• 第1章 緒論14-25
• 1.1 形式化方法和模型檢驗(yàn)14-16
• 1.2 基于自動(dòng)機(jī)理論的模型檢驗(yàn)算法16-22
• 1.2.1 可達(dá)性算法17-18
• 1.2.2 精化檢驗(yàn)算法18-20
• 1.2.3 空性檢驗(yàn)算法20-22
• 1.3 本文工作22-25
• 1.3.1 研究點(diǎn)和創(chuàng)新點(diǎn)22-24
• 1.3.2 組織架構(gòu)24-25
• 第2章 模型檢驗(yàn)研究基礎(chǔ)與現(xiàn)狀25-45
• 2.1 模型檢驗(yàn)概述25-28
• 2.1.1 模型檢驗(yàn)概念26-27
• 2.1.2 模型檢驗(yàn)的本質(zhì)27-28
• 2.2 模型檢驗(yàn)中的建模方法研究現(xiàn)狀28-30
• 2.2.1 系統(tǒng)建模28-29
• 2.2.2 性質(zhì)建模29-30
• 2.3 模型檢驗(yàn)算法研究現(xiàn)狀30-37
• 2.3.1 符號化模型檢驗(yàn)算法30-31
• 2.3.2 基于自動(dòng)機(jī)理論的模型檢驗(yàn)算法31-37
• 2.4 模型檢驗(yàn)算法優(yōu)化方法研究現(xiàn)狀37-41
• 2.5 模型檢驗(yàn)工具研究現(xiàn)狀41-43
• 2.6 本章小結(jié)43-45
• 第3章 基于反鏈的精化檢驗(yàn)算法45-63
• 3.1 引言45-46
• 3.2 相關(guān)工作46-47
• 3.3 基本定義47-48
• 3.3.1 精化檢驗(yàn)基本定義47-48
• 3.4 基于反鏈的精化檢驗(yàn)48-59
• 3.4.1 基于反鏈的路徑精化檢驗(yàn)48-51
• 3.4.2 基于反鏈的穩(wěn)定故障精化檢驗(yàn)51-55
• 3.4.3 基于反鏈的故障-偏差精化檢驗(yàn)55-59
• 3.5 實(shí)驗(yàn)及結(jié)果分析59-60
• 3.6 本章小結(jié)60-63
• 第4章 時(shí)間自動(dòng)機(jī)的精化檢驗(yàn)算法63-87
• 4.1 引言63-65
• 4.2 相關(guān)工作65-66
• 4.3 基本定義66-68
• 4.4 時(shí)間系統(tǒng)的路徑精化檢驗(yàn)68-72
• 4.4.1 時(shí)間自動(dòng)機(jī)的路徑精化檢驗(yàn)方法69-70
• 4.4.2 基于反鏈的時(shí)間自動(dòng)機(jī)路徑精化檢驗(yàn)算法70-72
• 4.5 時(shí)間自動(dòng)機(jī)的精化檢驗(yàn)72-79
• 4.5.1 性質(zhì)模型展開72-74
• 4.5.2 精化檢驗(yàn)中的時(shí)鐘域抽象74-77
• 4.5.3 基于模擬關(guān)系的狀態(tài)空間消減77-79
• 4.6 時(shí)間自動(dòng)機(jī)的精化檢驗(yàn)算法79-81
• 4.7 實(shí)驗(yàn)及結(jié)果分析81-86
• 4.7.1 時(shí)間自動(dòng)機(jī)路徑精化檢驗(yàn)實(shí)驗(yàn)結(jié)果81-82
• 4.7.2 時(shí)間自動(dòng)機(jī)間的精化檢驗(yàn)實(shí)驗(yàn)結(jié)果82-86
• 4.8 本章小結(jié)86-87
• 第5章 基于non-Zenoness的時(shí)間自動(dòng)機(jī)空性檢驗(yàn)算法87-108
• 5.1 引言87-89
• 5.2 理論基礎(chǔ)和相關(guān)工作89-94
• 5.2.1 理論基礎(chǔ)89-90
• 5.2.2 SNZ(Strongly non-Zeno)方法90-91
• 5.2.3 GZG(Guessing Zone Graph)方法91-93
• 5.2.4 其他方法93-94
• 5.3 時(shí)間自動(dòng)機(jī)CUB-TA94-97
• 5.4 基于non-Zenoness的空性檢驗(yàn)算法97-102
• 5.4.1 CUB-TA的空性檢驗(yàn)算法97-98
• 5.4.2 將任意時(shí)間自動(dòng)機(jī)轉(zhuǎn)化為CUB-TA98-102
• 5.5 實(shí)驗(yàn)及結(jié)果分析102-107
• 5.6 本章小結(jié)107-108
• 第6章 總結(jié)與展望108-110
• 6.1 本文工作總結(jié)108-109
• 6.2 未來工作展望109-110
• 參考文獻(xiàn)110-119
• 攻讀博士學(xué)位期間主要科研成果119-120
• 致謝120-121
• 作者簡歷121

【參考文獻(xiàn)】

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

1 高曉寧;計(jì)算機(jī)軟件可靠性分析及抗不可靠性方法[J];航空計(jì)算技術(shù);2003年03期

  本文關(guān)鍵詞：基于自動(dòng)機(jī)理論的高效模型檢驗(yàn)算法研究，由筆耕文化傳播整理發(fā)布。

本文編號：379140