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

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

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