model checking和JPF介绍

首先给大家介绍一种测试思想，model checking，前一段时间试用了一下不过还没有机会应用到项目上，有兴趣的同学可以一起研究，以下是的model checking的介绍和一个例子。

 

软件测试（ST）是通过特定的测试方法用一些输入（inputs）执行待测程序（SUT）去检查SUT的行为是否正确。在这个过程中牵扯到两个部分的选择：输入的数据和测试预期结果。

 

测试方法的不同在于我们如何选择输入的数据（比如随机，边界值等），我们对SUT了解的程度以及执行测试的环境（black/grey/white box），这些因素决定了如何定义以及验证这些正确的行为。这些也就引起了学术上的猜想，就如Edsger说的：program testing can at best show the presence of errors but never their absence。我们通常通过运行“足够”的测试来补偿这种猜想。但是对于测试一个复杂的系统就像大海捞针一样，如果是一个很有经验的测试人员可能很容易找到bug，如果不是，也不用担心，早晚有一天用户也会发现的。

Model checking不是基于猜想。至少从理论上讲，如果有违反的行为，model checking可以找到。Model checking致力于暴露程序的所有可能的行为。

下面我们用随机函数来举个例子：

import java.util.Random;

public class Rand {
     public static void main (String[] args) {
          Random random = new Random(42); // (1)


          int a = random.nextInt(2); // (2)

          System.out.println("a=" + a);

          //... lots of code here


          int b = random.nextInt(3); // (3)

          System.out.println(" b=" + b);

          int c = a/(b+a -2); // (4)

          System.out.println(" c=" + c);
     }
}

我们用JVM来运行这个例子，如果我们一开始不给他一个特定的值，那么会出现不同的结果，但是每次运行只能选择一个a和b的值:

> java Rand
a=1
  b=0
    c=-1
>

我们来看一个图形化的表示。

下面我们就来看看model checking是如何运行的，这里用到的一个利用model checking思想的测试工具-JPF

进入JPF，如果我们只是简单的运行JPF，那么结果没有什么区别，除了a会花费长一些的时间，还有b告诉我们这是一个“search”。

> bin/jpf Rand
JavaPathfinder v4.1 - (C) 1999-2007 RIACS/NASA Ames Research Center
====================================================== system under test
application: /Users/pcmehlitz/tmp/Rand.java

====================================================== search started: 5/23/07 11:48 PM
a=1
  b=0
    c=-1

====================================================== results
no errors detected

====================================================== search finished: 5/23/07 11:48 PM
>

这里的search代表着什么呢？我们可以看代码的第四行，会发现分母可能会出现0，但是这个决定于a和b的值，如果我们只是在普通的JVM里面运行那么可能很难遇到这种情况。我们重新进入JVM，但是这回我们让他寻找所有可能的选择：

> bin/jpf +cg.enumerate_random=true Rand
JavaPathfinder v4.1 - (C) 1999-2007 RIACS/NASA Ames Research Center
====================================================== system under test
application: /Users/pcmehlitz/tmp/Rand.java

====================================================== search started: 5/23/07 11:49 PM
a=0
  b=0
    c=0
  b=1
    c=0
  b=2

====================================================== error #1
gov.nasa.jpf.jvm.NoUncaughtExceptionsProperty
java.lang.ArithmeticException: division by zero
        at Rand.main(Rand.java:15)
....
>

通过计入参数，我们让JPF考虑所有可能的值，JPF从a=0开始，然后选择b=0，得出c=0，但是不想一般的VM，JPF考虑到还有其他的选择，所以他返回然后选择b=1，然后发现c=0，接着他回去试b=2，这时出现了错误。下面的图中描述了这个过程。

上面的这个简单的例子展示了testing和model checking的区别，model checking不会停止知道覆盖了所有数据组合或者找到了一个错误。

Model checking可以找到的问题有：deadlocks, race conditions, unhandled exceptions, application-specific assertions, ...等等。