【摘要】：模型檢測是一種自動化形式驗證技術(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ù)在特定的情況下可以大大地提高檢測效率。其中效果較為理想的就是on-the-fly模型檢測。 on-the-fly模型檢測將自動機理論應(yīng)用到模型檢測中，在很多情況下并不需要構(gòu)造整個系統(tǒng)的狀態(tài)空間。這是因為在檢測系統(tǒng)的自動機A和屬性自動機S的乘積時，A的狀態(tài)僅當(dāng)需要它們時才被構(gòu)造出來。 on-the-fly模型檢測優(yōu)勢是，當(dāng)檢測系統(tǒng)的自動機A和屬性自動機S的乘積自動機時，根本就不會生成A的某些狀態(tài)。另外一個優(yōu)勢是，在完成構(gòu)造兩個自動機的交之前，可能已經(jīng)找到了一個反例。一旦找到了一個反例，就沒有必要再繼續(xù)構(gòu)造乘積自動機。 在on-the-fly模型檢測中，乘積自動機的狀態(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)存，這樣可以減少在檢驗器運行過程中對內(nèi)存的需求，從而提高了模型檢測的能力。 本文提出了兩種利用數(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)后，通過實驗分析了動態(tài)管理內(nèi)存中的狀態(tài)的算法的實際效果，并分析了在實際運行中算法的優(yōu)勢和未來的工作。
【學(xué)位授予單位】：電子科技大學(xué)
【學(xué)位級別】：碩士
【學(xué)位授予年份】：2012
【分類號】：TP274;TP333.1

【參考文獻(xiàn)】

相關(guān)期刊論文 前4條

1 林惠民,張文輝;模型檢測:理論、方法與應(yīng)用[J];電子學(xué)報;2002年S1期

2 羅清勝;;一種基于Büchi自動機的LTL程序模型檢測方法[J];計算機與現(xiàn)代化;2010年08期

3 駱翔宇;蘇開樂;楊晉吉;;有界模型檢測同步多智體系統(tǒng)的時態(tài)認(rèn)知邏輯[J];軟件學(xué)報;2006年12期

4 王紅;內(nèi)存抖動問題分析及解決對策[J];濰坊高等專科學(xué)校學(xué)報;2000年01期

本文編號：2565684