基于自動機理論的高效模型檢驗算法研究.pdf

1、模型檢驗是一種重要的自動化驗證技術，基于狀態(tài)遍歷的思想窮舉系統(tǒng)能夠到達的所有狀態(tài)，并在系統(tǒng)不滿足指定的性質時提供反例。本文主要關注適用于軟件系統(tǒng)的基于自動機理論的（顯式）模型檢驗。給定一個系統(tǒng)模型，根據(jù)待檢驗性質的不同，需要采用不同的模型檢驗算法驗證系統(tǒng)是否滿足性質，主要包括可達性算法、精化檢驗算法和面向時序邏輯模型檢驗的空性檢驗算法等。其中，精化檢驗和空性檢驗算法中還存在不少困難和挑戰(zhàn):(1)精化檢驗算法依賴于自動機的子集構造，容易引

2、起狀態(tài)空間爆炸問題，是制約精化檢驗應用范圍的一個重要原因;(2)當前精化檢驗主要面向并發(fā)系統(tǒng)，而對于更復雜的系統(tǒng)，例如帶有時間約束的實時系統(tǒng)（通常用時間自動機表示），還沒有成熟有效的算法能夠支持其精化檢驗;(3)有窮自動機的空性檢驗算法已經發(fā)展得比較成熟，然而時間自動機的空性檢驗需要進一步考慮non-Zenoness問題（即在有限時間內不能發(fā)生無窮多事件），目前還沒有高效的算法支持。
　　針對上述困難和挑戰(zhàn)，本文重點研究基于反鏈的

3、精化檢驗算法、時間自動機的精化檢驗算法，以及提出了一種新的基于non-Zenoness的時間自動機空性檢驗算法，主要工作和貢獻如下:
　　1.針對精化檢驗算法中子集構造引起的狀態(tài)空間爆炸問題，本文首次將反鏈的思想引入到三類當前主要的精化檢驗算法中，提出了基于反鏈的路徑精化檢驗、穩(wěn)定故障精化檢驗和故障-偏差精化檢驗算法，展示了如何消減滿足反鏈關系的狀態(tài)，并證明了這三個算法的正確性。實驗表明，基于反鏈的精化檢驗算法性能大大優(yōu)于不使用反

4、鏈的精化檢驗算法，性能提升多達幾十倍。
　　2.本文首次提出了時間自動機的精化檢驗算法，即給定兩個時間自動機，一個時間自動機的語言是否包含于另一個時間自動機。算法采用了時鐘域抽象這種目前最有效的抽象方法，得到有窮狀態(tài)空間，使算法能夠真正應用于實際系統(tǒng)。算法還在一定程度上克服了時間自動機確定化的不可判定性問題，即用理論以及實驗證明了在絕大部分實際情況下算法是可以停止的。此外，算法還利用基于反鏈和上下界模擬關系的優(yōu)化方法進一步提高算法

5、性能。從實驗結果可以得出，算法在實際系統(tǒng)的驗證中表現(xiàn)出了良好的性能。
　　3.本文提出了一種新的基于non-Zenoness的時間自動機空性檢驗算法。目前已存在的其他空性檢驗算法由于在檢驗non-Zenoness時需要引入額外的時鐘或者狀態(tài)，使得狀態(tài)空間大大增加，算法性能往往十分低下。本文定義了一類特殊的時間自動機CUB-TA，并且為其提出了一種無需引入其他狀態(tài)或時鐘的空性檢驗算法，因此具有較高的效率。在此基礎上，本文又證明了任意

6、時間自動機都能夠轉化為CUB-TA，并提出了快速的轉化算法。實驗表明，大部分實際系統(tǒng)本身就是CUB-TA，或者只需要很小的代價就能轉換成CUB-TA，因此本文提出的算法非常具有實用性。此外，本文的算法性能在大部分情況下高于其他算法。
　　4.模型檢驗的成功很大程度上得益于驗證工具的支持。本文在模型驗證工具PAT框架中實現(xiàn)了上述所有算法，并結合PAT工具本身對各種形式化建模語言和語言解析的支持，使得用戶可以方便地建模實際系統(tǒng)和待檢驗