基于自動機(jī)理論的高效模型檢驗(yàn)算法研究.pdf

1、模型檢驗(yàn)是一種重要的自動化驗(yàn)證技術(shù)，基于狀態(tài)遍歷的思想窮舉系統(tǒng)能夠到達(dá)的所有狀態(tài)，并在系統(tǒng)不滿足指定的性質(zhì)時(shí)提供反例。本文主要關(guān)注適用于軟件系統(tǒ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)算法依賴于自動機(jī)的子集構(gòu)造，容易引

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

3、精化檢驗(yàn)算法、時(shí)間自動機(jī)的精化檢驗(yàn)算法，以及提出了一種新的基于non-Zenoness的時(shí)間自動機(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)于不使用反

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

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

6、時(shí)間自動機(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)