JPF Features and Classification
??到目前為止，應(yīng)該清楚的是筛圆，JPF不僅僅是一個模型檢查器：它是一個可以用于模型檢查的JVM涣脚。但是思杯，如果您熟悉正式的方法，您可能想知道支持什么樣的模型檢查方法和特性闹啦。
一些基本的模型檢查特性是：
Explicit State 顯示狀態(tài) 模型檢查是JPF的標(biāo)準(zhǔn)操作模式沮明，這意味著JPF跟蹤局部變量的具體值，棧窍奋，堆對象和線程狀態(tài)荐健。不包括故意的不同的調(diào)度行為之外酱畅。JPF應(yīng)該產(chǎn)生相同的結(jié)果，像一個正常的JVM江场。當(dāng)然它比較慢（它是在JVM上運(yùn)行的JVM纺酸，做了很多額外的工作）。
Symbolic Execution 符號執(zhí)行 意味JPF可以執(zhí)行從當(dāng)前執(zhí)行路徑中使用某個變量獲得的符號值來執(zhí)行程序址否。
Symbolic Execution means that JPF can perform program execution with symbolic values obtained from how a certain variable was used along the current path of execution (e.g. “x > 0 && x < 43”).
此外餐蔬，JPF甚至可以混合具體和符號執(zhí)行，或者在他們之間切換佑附。有關(guān)詳細(xì)信息樊诺，請參閱Symbolic Pathfinder project文檔。
State Matching 狀態(tài)匹配 狀態(tài)匹配是避免不必要工作的關(guān)鍵機(jī)制音同，程序的執(zhí)行狀態(tài)主要由堆和線程堆棿逝溃快照組成。而JPF執(zhí)行权均，它檢查每個新的狀態(tài)是否已經(jīng)看到一個相等的狀態(tài)缸夹，在這種情況下，沿著當(dāng)前的執(zhí)行路徑繼續(xù)下去是沒有用的螺句，而且JPF可以回到最近的未探索的非確定性選擇。哪些變量有助于狀態(tài)匹配橡类，并且可以由用戶控制狀態(tài)匹配蛇尚。
Backtracking 回溯 回溯意味著jpf可以恢復(fù)以前的執(zhí)行狀態(tài)，看看是否還有未執(zhí)行的選擇顾画。例如取劫，如果JPF達(dá)到程序結(jié)束狀態(tài)，它會回退以尋找不同的尚未執(zhí)行的調(diào)度序列研侣。理論上谱邪，這可以通過從一開始就重新執(zhí)行程序來實(shí)現(xiàn)，如果優(yōu)化了狀態(tài)存儲庶诡，回溯是一種更有效的機(jī)制惦银。
Partial Order Reduction 偏序約簡 偏序是JPF采用減少上下文切換線程之間不產(chǎn)生有趣的新程序狀態(tài)，這是即時完成的末誓，即不預(yù)先分析或注釋程序扯俱，通過檢查哪些指令可以產(chǎn)生線程間的影響。雖然這是快速的喇澡，但它不能處理“diamond case”（應(yīng)該翻譯成極少見的例子）迅栅，因?yàn)樗荒茉诋?dāng)前執(zhí)行之前看到。
JPF的靈活性是通過提供大量擴(kuò)展點(diǎn)的體系結(jié)構(gòu)來實(shí)現(xiàn)的晴玖，其中最重要的是：</br>
- search strategies 搜索策略 -- 控制搜索狀態(tài)空間的順序
- listeners 監(jiān)聽器 -- 監(jiān)視JPF的執(zhí)行并與之交互(例如檢查新屬性)
- native peers 本地同行 -- to model libraries and execute code at the host VM level
- bytecode factories -- 提供不同的執(zhí)行模型(如符號執(zhí)行)
- publishers -- 生成特定的報告
通常读存，通過配置的靈活性是JPF對軟件模型檢查的可擴(kuò)展性問題的回答为流。
