軟件模型檢驗中謂詞抽象技術(shù)研究.pdf

1、形式化驗證方法主要包括定理證明和模型檢驗,其中模型檢驗因其自動化高得到重視,并已經(jīng)在硬件領(lǐng)域和通訊協(xié)議的分析與驗證中取得了巨大成功。近幾年來,軟件模型檢驗成為研究的熱點,并取得一定的成功。軟件系統(tǒng)通常涉及無窮數(shù)據(jù)域上的運算而呈現(xiàn)出無限狀態(tài),而模型檢驗方法只能對有限狀態(tài)模型進行驗證,因此軟件模型檢驗面臨的最大問題是狀態(tài)空間爆炸。抽象是最有潛力的解決狀態(tài)爆炸問題的方法。謂詞抽象的提出實現(xiàn)了抽象的自動化。當前基于謂詞抽象的反例導(dǎo)向抽象精化方法

2、是軟件模型檢驗的主要方法。本文主要研究內(nèi)容如下。
　　(1)基于抽象解釋和謂詞抽象理論,對謂詞抽象算法和反例導(dǎo)向抽象精化算法進行了研究。
　　(2)對軟件模型檢驗工具BLAST做了研究,該工具使用惰性抽象技術(shù)將反例導(dǎo)向抽象精化方法中的抽象模型構(gòu)造,模型檢驗,抽象精化三個過程整合成為一體,on-the-fly構(gòu)造抽象模型,按需求精化。如果模型檢驗輸出虛假反例,則進行謂詞精化實現(xiàn)抽象模型的精化。BLAST的抽象系統(tǒng)構(gòu)造使用傳統(tǒng)的

3、定理證明器作為求解器,本文研究了將SAT求解器應(yīng)用于BLAST的抽象模型構(gòu)造,這種方法可以克服定理證明器的局限性,并且可以構(gòu)造一個更精確的抽象模型,提高計算效率。
　　(3)在抽象模型構(gòu)造-模型檢驗-謂詞精化的迭代過程中,如果抽象模型不夠精確,模型檢驗將產(chǎn)生抽象虛假反例,其在原始系統(tǒng)中沒有對應(yīng)的具體反例,這時需要進行謂詞精化,增加謂詞用于去除虛假反例。用更新后的謂詞集合重新構(gòu)造一個沒有虛假反例的抽象模型,重新進行模型檢驗。相對其他