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

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

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

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

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