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

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

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

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