基于模型檢查的C程序分析技術(shù)研究.pdf

1、軟件測試是為了發(fā)現(xiàn)錯誤而執(zhí)行程序的過程,是保證軟件質(zhì)量的重要手段,因而成為軟件生命周期中的重要階段。在已有的測試工具中,源代碼測試工具有著重要的應用。模型檢查則是一種遍歷系統(tǒng)所有可能執(zhí)行路徑的自動驗證技術(shù)。最早由E.M.Clarke和E.A.Emerson在1981年提出,主要是米驗證有窮狀態(tài)并發(fā)系統(tǒng)的命題性質(zhì)。它通常采用狀態(tài)空間搜索的方法來檢查一個給定的計算模型(程序)是否滿足某個特定性質(zhì)。在基于模型檢查的軟件代碼分析和可靠性驗證方面

2、,國外少數(shù)大學和研究機構(gòu)已經(jīng)取得了一定的進展。目前仍需要解決和改善的問題主要集中在效率和準確性兩個方面。
　　 本文主要討論和分析了程序模型建立、模型檢查和模型精化等方面的研究現(xiàn)狀。針對軟件單元測試和系統(tǒng)整合測試等階段遇到的程序接口調(diào)用問題,給出了一個具體的方案。本文提出了多種策略盡可能滿足用戶對效率和準確性方面的不同需求,同時詳細探討了基于模型檢查的程序測試框架中各個階段使用的技術(shù)和算法,并于最后描述了基于模型檢查的程序接口調(diào)