基于外存的大規(guī)模模型檢測新方法的研究.pdf

1、模型檢測是一種可以對系統(tǒng)進(jìn)行自動驗證的技術(shù)。近年來，模型檢測技術(shù)因其簡單明了且不需太多的人工干預(yù)等良好特性，得到了廣泛的關(guān)注和研究。然而，現(xiàn)有的模型檢測技術(shù)，基本上都是從驗證的層面來檢測系統(tǒng)是否存在反例，即只負(fù)責(zé)找出一個反例。
　　如果對問題做進(jìn)一步的思考，在知道系統(tǒng)存在缺陷后，還要對系統(tǒng)加以修復(fù)。而修復(fù)一個規(guī)模較大的系統(tǒng)，往往需要一次考慮多個反例。然而現(xiàn)有的模型檢測技術(shù)，不能一次找出大規(guī)模系統(tǒng)的多個反例。所以，本文針對大規(guī)模系統(tǒng)

2、這一現(xiàn)狀，提出了一次能夠查找多個反例的思想，并著重對查找所有反例中的關(guān)鍵技術(shù)（查找接受環(huán)）進(jìn)行了分析和研究。
　　本文首先對模型檢測技術(shù)的發(fā)展?fàn)顩r進(jìn)行了綜述，得出現(xiàn)有的模型檢測技術(shù)不能查找出大規(guī)模待檢測系統(tǒng)多個反例的結(jié)論；接著本文對模型檢測中涉及到的基礎(chǔ)理論知識進(jìn)行了介紹。其次，我們利用外存來解決模型檢測過程中狀態(tài)空間爆炸問題；然后，針對大規(guī)模系統(tǒng)，詳細(xì)呈現(xiàn)了一次查找多個接受環(huán)的算法，該算法從初始狀態(tài)開始并基于深度優(yōu)先搜索策略，能

3、夠在線性時間復(fù)雜度找出待檢測系統(tǒng)所有的接受環(huán)。宏觀上來說，該算法首先查找包含接受狀態(tài)的強連通分量Accept-SCC，然后再計算出每一個Accept-SCC中所包含的簡單接受環(huán)。先選擇查找Accept-SCC可以避免大量不必要的重復(fù)路徑的搜索，并且，當(dāng)一個系統(tǒng)不存在Accept-SCC時，說明系統(tǒng)不存在反例，算法就可以提前結(jié)束。在計算Accept-SCC中的簡單接受環(huán)時，提出優(yōu)先處理那些能夠存儲于內(nèi)存中的小規(guī)模Accept-SCC的策略

4、，能夠在一定程度上減少I/O訪問次數(shù)。
　　在實驗環(huán)節(jié)，文中借助開源模型檢測工具Spin，將SAEAC算法嵌入到工具Spin中；然后，選擇能代表不同情況的典型benchmark與本文中提及的DAC和MAP算法進(jìn)行對比實驗。通過對實驗數(shù)據(jù)的分析對比，得出SAEAC算法不僅能夠找出多個反例，并且在平均查找出一個反例的效率上要明顯優(yōu)于DAC和MAP算法。并且，最后的實驗證明了原Spin無法完成對大規(guī)模不含反例的benchmark進(jìn)行檢測