基于內(nèi)存和狀態(tài)管理的模型檢測方法.pdf

1、模型檢測是一種自動化形式驗證技術(shù)，主要用于檢測軟硬件設(shè)計模型，這些模型規(guī)范通過時序邏輯公式給出。模型檢測從用戶所描述的模型開始，然后發(fā)現(xiàn)用戶斷言的假設(shè)對該模型是否有效。如果無效，模型檢測工具可以產(chǎn)生由執(zhí)行軌跡所構(gòu)成的反例。
　　然而模型檢測存在因狀態(tài)空間爆炸而導(dǎo)致內(nèi)存不夠的問題，這也是大規(guī)模并發(fā)系統(tǒng)驗證的瓶頸。很多研究人員做了很多相關(guān)研究，雖然沒有徹底地解決這個問題，然而提出了一些技術(shù)在特定的情況下可以大大地提高檢測效率。其中效果

2、較為理想的就是on-the-fly模型檢測。
　　on-the-fly模型檢測將自動機(jī)理論應(yīng)用到模型檢測中，在很多情況下并不需要構(gòu)造整個系統(tǒng)的狀態(tài)空間。這是因為在檢測系統(tǒng)的自動機(jī) A和屬性自動機(jī) S的乘積時，A的狀態(tài)僅當(dāng)需要它們時才被構(gòu)造出來。
　　on-the-fly模型檢測優(yōu)勢是，當(dāng)檢測系統(tǒng)的自動機(jī)A和屬性自動機(jī)S的乘積自動機(jī)時，根本就不會生成 A的某些狀態(tài)。另外一個優(yōu)勢是，在完成構(gòu)造兩個自動機(jī)的交之前，可能已經(jīng)找到了一

3、個反例。一旦找到了一個反例，就沒有必要再繼續(xù)構(gòu)造乘積自動機(jī)。
　　在on-the-fly模型檢測中，乘積自動機(jī)的狀態(tài)由雙深度優(yōu)先算法按需產(chǎn)生。本文分析了這個雙深度優(yōu)先算法在檢測過程中的內(nèi)存使用情況。雙深度優(yōu)先遍歷中需要用到兩個堆棧，當(dāng)系統(tǒng)規(guī)模很大時，要找的反例路徑可能非常長，這就是使得堆棧上要存放很多狀態(tài)。通過利用數(shù)據(jù)庫，可以將搜索堆棧里暫時用不到的狀態(tài)存儲到外存上，在需要的時候再調(diào)回內(nèi)存，這樣可以減少在檢驗器運(yùn)行過程中對內(nèi)存的需

4、求，從而提高了模型檢測的能力。
　　本文提出了兩種利用數(shù)據(jù)庫的方法。一種是靜態(tài)的狀態(tài)和內(nèi)存管理，一種是動態(tài)的狀態(tài)和內(nèi)存管理。由于使用了數(shù)據(jù)庫，將內(nèi)存中的狀態(tài)存儲到磁盤上可能出現(xiàn)的內(nèi)存抖動問題。針對兩種不同的內(nèi)存和狀態(tài)管理策略，分別提出了相應(yīng)的內(nèi)存狀態(tài)管理策略以很好的解決內(nèi)存抖動的問題。
　　在開源軟件SPIN的基礎(chǔ)上，將本文描述的算法實現(xiàn)，這樣做主要是利用SPIN原有的存儲狀態(tài)的數(shù)據(jù)結(jié)構(gòu)，以及它的輸入輸出方法。算法實現(xiàn)后，通