發(fā)布時間：2017-05-19 16:08

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

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

• 摘要4-6
• Abstract6-14
• 第1章 緒論14-25
• 1.1 形式化方法和模型檢驗14-16
• 1.2 基于自動機理論的模型檢驗算法16-22
• 1.2.1 可達(dá)性算法17-18
• 1.2.2 精化檢驗算法18-20
• 1.2.3 空性檢驗算法20-22
• 1.3 本文工作22-25
• 1.3.1 研究點和創(chuàng)新點22-24
• 1.3.2 組織架構(gòu)24-25
• 第2章 模型檢驗研究基礎(chǔ)與現(xiàn)狀25-45
• 2.1 模型檢驗概述25-28
• 2.1.1 模型檢驗概念26-27
• 2.1.2 模型檢驗的本質(zhì)27-28
• 2.2 模型檢驗中的建模方法研究現(xiàn)狀28-30
• 2.2.1 系統(tǒng)建模28-29
• 2.2.2 性質(zhì)建模29-30
• 2.3 模型檢驗算法研究現(xiàn)狀30-37
• 2.3.1 符號化模型檢驗算法30-31
• 2.3.2 基于自動機理論的模型檢驗算法31-37
• 2.4 模型檢驗算法優(yōu)化方法研究現(xiàn)狀37-41
• 2.5 模型檢驗工具研究現(xiàn)狀41-43
• 2.6 本章小結(jié)43-45
• 第3章 基于反鏈的精化檢驗算法45-63
• 3.1 引言45-46
• 3.2 相關(guān)工作46-47
• 3.3 基本定義47-48
• 3.3.1 精化檢驗基本定義47-48
• 3.4 基于反鏈的精化檢驗48-59
• 3.4.1 基于反鏈的路徑精化檢驗48-51
• 3.4.2 基于反鏈的穩(wěn)定故障精化檢驗51-55
• 3.4.3 基于反鏈的故障-偏差精化檢驗55-59
• 3.5 實驗及結(jié)果分析59-60
• 3.6 本章小結(jié)60-63
• 第4章 時間自動機的精化檢驗算法63-87
• 4.1 引言63-65
• 4.2 相關(guān)工作65-66
• 4.3 基本定義66-68
• 4.4 時間系統(tǒng)的路徑精化檢驗68-72
• 4.4.1 時間自動機的路徑精化檢驗方法69-70
• 4.4.2 基于反鏈的時間自動機路徑精化檢驗算法70-72
• 4.5 時間自動機的精化檢驗72-79
• 4.5.1 性質(zhì)模型展開72-74
• 4.5.2 精化檢驗中的時鐘域抽象74-77
• 4.5.3 基于模擬關(guān)系的狀態(tài)空間消減77-79
• 4.6 時間自動機的精化檢驗算法79-81
• 4.7 實驗及結(jié)果分析81-86
• 4.7.1 時間自動機路徑精化檢驗實驗結(jié)果81-82
• 4.7.2 時間自動機間的精化檢驗實驗結(jié)果82-86
• 4.8 本章小結(jié)86-87
• 第5章 基于non-Zenoness的時間自動機空性檢驗算法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 時間自動機CUB-TA94-97
• 5.4 基于non-Zenoness的空性檢驗算法97-102
• 5.4.1 CUB-TA的空性檢驗算法97-98
• 5.4.2 將任意時間自動機轉(zhuǎn)化為CUB-TA98-102
• 5.5 實驗及結(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];航空計算技術(shù);2003年03期

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

本文編號：379140