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

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

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

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

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