JPF Application Goals and Types JPF應(yīng)用程序目標(biāo)和類型

??到目前為止，您已經(jīng)知道在JPF上運(yùn)行在編譯的java程序，就像普通的java虛擬機(jī)。但是，使用JPF的目的是什么？而且基于這些目的，不同的JPF應(yīng)用程序類型是什么。

Why to Use JPF?

??在我們對不同類型的jpf應(yīng)用程序進(jìn)行分類之前，值得一提的是為什么我們真的想應(yīng)用它。忠告：如果你有一個(gè)嚴(yán)格的順序程序，只有幾個(gè)定義良好的輸入值，你最好寫幾個(gè)測試用例 -- 使用JPF對你的幫助并不會太多。</br>
使用JPF的兩大主要原因有：

• Explore Execution Alternatives 可選擇執(zhí)行方案</br>
  ??畢竟，jpf最初是作為軟件模型檢查器開始的,所以它最初的領(lǐng)域是探索執(zhí)行的選擇,其中我們有四種不同的類型:</br>

  • scheduling sequences --- 并發(fā)應(yīng)用仍然是JPF應(yīng)用程序的主要領(lǐng)域，因?yàn)?a)死鎖和數(shù)據(jù)競爭等缺陷是微妙的，通常是虛假的。 (b)調(diào)度程序通常無法從測試環(huán)境中控制。也就是說，這很難甚至不可能被檢測。另一方面，JPF不僅“擁有”調(diào)度程序（它是虛擬機(jī)),而且可以開發(fā)所有的調(diào)度組合。<font color=red>它甚至可以讓你自己定義調(diào)度的策略</font>。
  • input data variation --- JPF允許您探索通過啟發(fā)式定義的輸入值集(例如低于、等于或高于某個(gè)閾值的值),這在編寫測試驅(qū)動程序時(shí)特別有用。
  • environment events --- 像Swing或Web應(yīng)用程序之類的程序類型通常會對類似于用戶輸入的外部事件作出反應(yīng)，這樣的事件可以由JPF作為選擇集來模擬。
  • control flow choices --- JPF不僅可以檢查程序?qū)唧w輸入的反應(yīng)，它還可以回頭，系統(tǒng)地探索程序控制結(jié)構(gòu)(分支指令)，以計(jì)算將執(zhí)行代碼某一部分的輸入數(shù)據(jù)值。

• Execution Inspection 執(zhí)行檢查</br>
  ??即使你的程序沒有很多執(zhí)行選項(xiàng)，你可以利用JPF的檢驗(yàn)?zāi)芰?。作為一臺可擴(kuò)展的虛擬機(jī)，實(shí)現(xiàn)<font color=pink>coverage analyzers 覆蓋分析器</font>或<font color=pink>non-invasive tests 非侵入性測試</font>相對容易，否則會忽略這些情況，因?yàn)樗鼈兒茈y或很乏味地實(shí)現(xiàn)(比如數(shù)字指令中的溢出)。

JPF Application Types JPF應(yīng)用類型

??有三種基本的JPF應(yīng)用類型，它們各有不同的優(yōu)勢和劣勢：JPF- aware, unaware 和 "enabled" programs。

app-types.png

JPF unaware programs
這是通常的情況 --- 在應(yīng)用程序中運(yùn)行jpf，該應(yīng)用程序通常不知道驗(yàn)證。它只在任何兼容java的vm上運(yùn)行。使用JPF檢查這種應(yīng)用的典型原因是查找難以測試的所謂的違反非函數(shù)屬性，例如死鎖或競爭條件。JPF特別擅長發(fā)現(xiàn)和解釋與并發(fā)相關(guān)的缺陷，但你得知道代價(jià)：JPF比java虛擬機(jī)慢得多（它比正常的字節(jié)代碼解釋器做的更多），它可能不支持受測試系統(tǒng)使用的所有Java庫。

JPF dependent programs
我們有模型的應(yīng)用程序 --- 他們存在唯一目的是驗(yàn)證通過JPF(例如，檢查某個(gè)算法)，所以java恰好是實(shí)現(xiàn)語言因?yàn)檫@是JPF的理解。通常，這些應(yīng)用程序是基于特定于域的框架(例如狀態(tài)擴(kuò)展？)編寫的，以便JPF能夠驗(yàn)證模型。因此，模型應(yīng)用程序本身通常較小，規(guī)模很好，并且不需要額外的特性規(guī)范。缺點(diǎn)是開發(fā)底層域框架非常昂貴。

JPF enabled programs
第三類的投資回報(bào)可能是最好的，可以在任何VM上運(yùn)行的程序，但是包含表示無法用標(biāo)準(zhǔn)Java語言表示的屬性的java注釋。

For example, assume you have a class which instances are not thread safe, and hence are not supposed to be used as shared objects. You can just run JPF and see if it finds a defect (like a data race) which is caused by illegally using such an object in a multi-threaded context. But even if JPF out-of-the-box can handle the size of the state space and finds the defect, you probably still have to spend a significant effort to analyze a long trace to find the original cause (which might not even be visible in the program). It is not only more easy on the tool (means faster), but also better for understanding if you simply mark the non-threadsafe class with a @NonShared annotation. Now JPF only has to execute up to the point where the offending object reference escapes the creating thread, and can report an error that immediately shows you where and how to fix it.

There is an abundance of potential property-related annotations (such as @NonNull for a static analyzer and JPF), including support for more sophisticated, embedded languages to express pre- and post-conditions.