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

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

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

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