Java程序模型驗證中的程序建模問題研究.pdf

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

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

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