JPF Application Goals and Types JPF应用程序目标和类型

  到目前为止，您已经知道在JPF上运行在编译的java程序，就像普通的java虚拟机。但是，使用JPF的目的是什么？而且基于这些目的，不同的JPF应用程序类型是什么。

Why to Use JPF?

  在我们对不同类型的jpf应用程序进行分类之前，值得一提的是为什么我们真的想应用它。忠告：如果你有一个严格的顺序程序，只有几个定义良好的输入值，你最好写几个测试用例 -- 使用JPF对你的帮助并不会太多。</br>
使用JPF的两大主要原因有：

• Explore Execution Alternatives 可选择执行方案</br>
    毕竟，jpf最初是作为软件模型检查器开始的,所以它最初的领域是探索执行的选择,其中我们有四种不同的类型:</br>

  • scheduling sequences --- 并发应用仍然是JPF应用程序的主要领域，因为(a)死锁和数据竞争等缺陷是微妙的，通常是虚假的。 (b)调度程序通常无法从测试环境中控制。也就是说，这很难甚至不可能被检测。另一方面，JPF不仅“拥有”调度程序（它是虚拟机),而且可以开发所有的调度组合。<font color=red>它甚至可以让你自己定义调度的策略</font>。
  • input data variation --- JPF允许您探索通过启发式定义的输入值集(例如低于、等于或高于某个阈值的值),这在编写测试驱动程序时特别有用。
  • environment events --- 像Swing或Web应用程序之类的程序类型通常会对类似于用户输入的外部事件作出反应，这样的事件可以由JPF作为选择集来模拟。
  • control flow choices --- JPF不仅可以检查程序对具体输入的反应，它还可以回头，系统地探索程序控制结构(分支指令)，以计算将执行代码某一部分的输入数据值。

• Execution Inspection 执行检查</br>
    即使你的程序没有很多执行选项，你可以利用JPF的检验能力。作为一台可扩展的虚拟机，实现<font color=pink>coverage analyzers 覆盖分析器</font>或<font color=pink>non-invasive tests 非侵入性测试</font>相对容易，否则会忽略这些情况，因为它们很难或很乏味地实现(比如数字指令中的溢出)。

JPF Application Types JPF应用类型

  有三种基本的JPF应用类型，它们各有不同的优势和劣势：JPF- aware, unaware 和 "enabled" programs。

app-types.png

JPF unaware programs
这是通常的情况 --- 在应用程序中运行jpf，该应用程序通常不知道验证。它只在任何兼容java的vm上运行。使用JPF检查这种应用的典型原因是查找难以测试的所谓的违反非函数属性，例如死锁或竞争条件。JPF特别擅长发现和解释与并发相关的缺陷，但你得知道代价：JPF比java虚拟机慢得多（它比正常的字节代码解释器做的更多），它可能不支持受测试系统使用的所有Java库。

JPF dependent programs
我们有模型的应用程序 --- 他们存在唯一目的是验证通过JPF(例如，检查某个算法)，所以java恰好是实现语言因为这是JPF的理解。通常，这些应用程序是基于特定于域的框架(例如状态扩展？)编写的，以便JPF能够验证模型。因此，模型应用程序本身通常较小，规模很好，并且不需要额外的特性规范。缺点是开发底层域框架非常昂贵。

JPF enabled programs
第三类的投资回报可能是最好的，可以在任何VM上运行的程序，但是包含表示无法用标准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.