基于JPF的軟件模型檢測(cè)分析與應(yīng)用.pdf

1、形式化方法是提高并發(fā)系統(tǒng)的安全性與可靠性的重要手段。模型檢測(cè)是一種對(duì)有限狀態(tài)并行系統(tǒng)進(jìn)行形式化驗(yàn)證的方法，并已初步應(yīng)用于各種軟件的安全性和可靠性驗(yàn)證中。軟件模型檢測(cè)過程中最大的問題，是如何緩解狀態(tài)空間爆炸問題。
　　 JPF(Java Pathfinder)是一種精確的Java字節(jié)碼狀態(tài)模型檢測(cè)工具。JPF為Java程序的模型檢測(cè)提供了很好的實(shí)現(xiàn)方法，對(duì)并行程序中存在的死鎖和數(shù)據(jù)競(jìng)爭(zhēng)等問題，以及未處理異常等與Java運(yùn)行時(shí)相關(guān)的

2、程序漏洞，JPF都可以有效地進(jìn)行模型檢測(cè)。JPF工作在Java虛擬機(jī)之上，通過VM來對(duì)系統(tǒng)狀態(tài)進(jìn)行搜索和管理，使用啟發(fā)式選擇生成器來構(gòu)建系統(tǒng)的狀態(tài)轉(zhuǎn)移。JPF提供了SearchListener和VMListener、MJI、字節(jié)碼工廠及報(bào)告系統(tǒng)等豐富的擴(kuò)展方式。針對(duì)Java程序本身的特點(diǎn)，JPF提供了一系列限制狀態(tài)空間爆炸的可行性方案，包括偏序規(guī)約、對(duì)稱規(guī)約、謂詞抽象等。
　　 本文基于JPF提出了一種軟件模型檢測(cè)工具的通用設(shè)計(jì)

3、策略，包括狀態(tài)管理、搜索策略和環(huán)境模擬等；實(shí)現(xiàn)了基于Eclipse的Java模型檢測(cè)平臺(tái)，使得程序員可以在編寫代碼的同時(shí)實(shí)時(shí)檢測(cè)自己的代碼；擴(kuò)展了JPF的錯(cuò)誤軌跡輸出方式，在只關(guān)注系統(tǒng)漏洞位置的情況下，可以通過忽略系統(tǒng)反例細(xì)節(jié)的方式來加速程序的模型檢測(cè)過程。通過多個(gè)實(shí)例驗(yàn)證，表明了本文提出的軟件模型檢測(cè)工具設(shè)計(jì)策略的有效性和基于Eclipse的Java模型檢測(cè)平臺(tái)的可靠性。
　　 JPF對(duì)提高Java程序軟件的安全性、保證軟件質(zhì)