基于模型檢驗(yàn)的軟件分析方法研究.pdf

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

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

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

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