基于模型檢驗的軟件分析方法研究.pdf

1、電腦的使用越來越普及，人們對電腦的依賴也越來越嚴重。電腦硬件由于發(fā)展時間較長，硬件的協(xié)議比較簡單，其檢測手段豐富、成熟，安全性要比電腦軟件的安全性高一個等級，甚至更多。同時，生活信息化加深了人們對軟件的依賴，軟件的質(zhì)量的好壞，給使用軟件的各行各業(yè)有很深的影響，因此人們對軟件質(zhì)量推出了越了越高的要求。 在軟件開發(fā)的軟件過程思想出現(xiàn)以后，如何提高軟件質(zhì)量一直是計算機界研究的重點。傳統(tǒng)的軟件測試，使用針對性的測試，可以指出軟件存在的特

2、定缺陷，但是由于測試并不能夠無窮的進行，所有此方法不能指出所有的錯誤，同時也不能證明軟件的正確性。形式化方法使用數(shù)學(xué)方法，能較好的證明系統(tǒng)的完整性、正確性、安全性。形式化方法中的模型檢驗以其高效、自動化使其成為研究的熱點。 自模型檢驗技術(shù)提出以來，人們將其應(yīng)用到硬件驅(qū)動和協(xié)議的開發(fā)上，隨著應(yīng)用過程中的出現(xiàn)問題、解決問題的過程，不斷有相關(guān)的技術(shù)、理論提出。符號化方法使模型檢驗在檢驗時，能夠檢驗10120個狀態(tài)，這使模型檢驗技術(shù)完全

3、勝任了硬件驅(qū)動和協(xié)約驗證的驗證問題。在模型檢驗在硬件、協(xié)議驗證上獲得巨大的成功后，人們將模型檢驗的應(yīng)用對象的研究重點放到軟件系統(tǒng)上來。 使用模型檢驗到軟件系統(tǒng)的的步驟大概分為：對待檢驗系統(tǒng)進行建模、用模型性質(zhì)描述語言對程序性質(zhì)進行描述、使用模型檢驗工具檢驗?zāi)Ｐ褪欠駶M足性質(zhì)。對模型檢驗的研究基本集中在這三個步驟：1）怎樣增加模型檢驗?zāi)軌蚪鉀Q問題的范圍；2）更方便、靈活的描述程序性質(zhì)，3）提高模型檢驗過程的效率。而狀態(tài)爆炸問題是模型

4、檢驗工具在軟件系統(tǒng)中使用的瓶頸。 本文提出一種基于模型檢驗的軟件分析方法。本方法結(jié)合軟件的信息流分析技術(shù)，使用CTL描述語言和NuSMV模型檢驗工具。該方法能夠確定給定C/C++源程序是否滿足我們預(yù)先已定義的程序性質(zhì)。這些性質(zhì)包括：1）不存在未初始化變量；2）內(nèi)存分配和釋放配對；3）不存在變量未使用；4）不存在野指針。通過使用NuSMV模型檢驗工具，結(jié)合模型檢驗和程序分析技術(shù)，完成對程序相關(guān)性質(zhì)的分析。 本文的主要工作包