1、隨著人們對軟件可靠性、安全性的要求越來越高，軟件測試技術的發(fā)展也受到了越來越多的重視，模型檢測技術是一種形式化自動驗證技術，目的是確保系統(tǒng)設計規(guī)范正確性的。
　　JPF(JavaPathfinder)是顯式的Java字節(jié)碼模型檢測工具，它是一個特殊的Java虛擬機，理論上，它能夠執(zhí)行程序中所有可能存在的路徑，主要適用于難以檢測的多線程程序中的并行錯誤，如死鎖和未處理的異常。JPF提供了選擇生成器、指令工廠、屬性系統(tǒng)、MJI、Lis

2、teners以及報告系統(tǒng)等多種擴展方式。
　　SPF是JPF的一個擴展項目，在SPF中，程序執(zhí)行時用符號輸入來代替多個具體的輸入值，程序中變量的值由符號表達式表示，通過分析不同表達式的執(zhí)行路徑來生成各個分支的約束條件，這些約束條件由off-the-shell求解器來確定，并且進行路徑可行性分析和生成測試輸入。SPF與JPF模型檢測器緊密集成，JPF框架為SPF提供了系統(tǒng)級的探索符號程序路徑，不同的線程交錯及出現(xiàn)在代碼中的其它形式的