Java程序模型驗(yàn)證中的程序建模問(wèn)題研究.pdf

1、計(jì)算機(jī)系統(tǒng)的發(fā)展對(duì)軟件提出了更高的要求，相應(yīng)的提升軟件質(zhì)量這一課題的研究也日益受到從業(yè)人員的重視，而軟件的可靠性、正確性是保證軟件具有高質(zhì)量的關(guān)鍵因素。 目前，在實(shí)際的軟件驗(yàn)證中，普遍采用的方法是對(duì)系統(tǒng)進(jìn)行大規(guī)模的測(cè)試，通過(guò)輸入多個(gè)測(cè)試用例并檢查執(zhí)行結(jié)果是否正確來(lái)發(fā)現(xiàn)系統(tǒng)中可能存在的問(wèn)題，但是這種方法通常無(wú)法窮舉系統(tǒng)所有可能的行為。近些年來(lái)，模型驗(yàn)證在驗(yàn)證硬件系統(tǒng)組件和通信協(xié)議上的應(yīng)用已經(jīng)相當(dāng)成熟，把模型檢測(cè)應(yīng)用于軟件系統(tǒng)的驗(yàn)證

2、已經(jīng)成為備受關(guān)注的焦點(diǎn)，且已取得顯著成就。許多研究小組開(kāi)發(fā)出了多種實(shí)用的軟件模型驗(yàn)證工具，如SLAM、MAGIC、JPF等。 模型驗(yàn)證技術(shù)成功應(yīng)用于軟件系統(tǒng)中的最大阻礙就是程序建模時(shí)的狀態(tài)爆炸問(wèn)題，本文結(jié)合NASA Ames的自動(dòng)化軟件工程小組開(kāi)源項(xiàng)目JPF(Java PathFinder)，在建模一驗(yàn)證一模型細(xì)化框架下研究了Java程序模型驗(yàn)證的程序建模過(guò)程中縮減程序狀態(tài)空間的兩種方法：程序切片技術(shù)和抽象技術(shù)。 本文的

3、主要工作包括以下幾個(gè)部分： 1．介紹了在建模一驗(yàn)證一模型細(xì)化框架下對(duì)軟件系統(tǒng)進(jìn)行模型驗(yàn)證的方法。 2．在對(duì)處理并發(fā)機(jī)制的并發(fā)流程語(yǔ)言(CFCL)進(jìn)行了形式化描述的基礎(chǔ)上，探討了對(duì)多線程程序切片的正確性進(jìn)行互模擬驗(yàn)證的方法，有效的保證了多線程切片的正確性。 3．提出了正確構(gòu)造多線程程序切片的方法。模型驗(yàn)證與規(guī)范化建模語(yǔ)言的緊密結(jié)合，極大的推動(dòng)了驗(yàn)證自動(dòng)化的發(fā)展。 4．針對(duì)抽象技術(shù)的使用會(huì)出現(xiàn)反例路徑“不可行