类复制变异和JPF技术的Eclipse模型检测方法

廖慧芬，詹 芹

LIAO Hui-fen，ZHAN Qin

（九江学院 信息科学与技术学院，九江 330005）

1 JPF工作原理和体系结构

JPF的基本工作原理是从被检测对象中筛选出少量的状态等价于原系统，然后交给JVM检测，再对不符合系统性质的检测结果，JPF可以用不同的方式显示错误路径及性质违例。JPF有三种不同的输出方式：分别是JPF报告系统（Reporting System）、JPF日志和应用输出。

JPF中的整个设计重点基本是JVM和Search对象，JVM的功能相当于状态生成器，在执行过程中，首先JVM生成模型检测使用的程序状态，同时JVM中的三个重要的方法：Forward（）表示下一个状态、Backtrack（）存储回溯栈中的上一个状态和RestoreState（）存储一个任意状态，控制程序状态；Search的功能相当于是JVM的驱动，筛选出供JVM处理的状态，告诉JPF虚拟机在状态空间中是前进还是后退，同时具有性质验证器的功能。

2 JPF的关键技术

在检测过程中，JAVA程序状态一般包括三部分，分别是对象的动态变量、类的静态变量和每个线程的信息。由此可见，JAVA程序的状态数量一般都是很大，在解决严重的状态爆炸问题方面，JPF使用了启发式路径选择生成器、on-the-fly偏序规约、主机VM执行、状态抽象、静态分析、对称规约和符号执行等一系列的解决方案。

偏序规约（Partial Order Reduction）方法是利用行为的独立性（Independence）来减少并行系统模型检测中的状态空间爆炸问题。因此，在算法中只需要考虑其中的一种状态而忽略另一种状态，状态S通过这种方式可以转换成比较小的另一个状态S'，在执行状态空间遍历时，只需要选择合适并具有代表性的状态集代替全部状态集，从而达到减少状态数量。

图1 系统状态转移图

近年来，在模型检测中经常用对称（Symmetry）方法来避免状态爆炸问题，对称方法主要是利用了系统中的对称结构来进行状态精简的。在JPF中，把对称方法和偏序规约技术结合形成对称规约技术，它的基本思想是，在模型检测过程中对系统中需要进行性质验证的状态形成等价状态，只需要检测这些等价状态中的一个就可以了。假设一个并行系统中，行为集A={xi,yi,zi,ni}，状态集S={Ni,Ti,Ci}。形成的完整系统状态转移如图1所示。注意到，图1中存在明显的对称关系，使用对称规约可以得到如图2所示的新的状态转移图。同时，行为y、z是独立的，可以使用偏序规约对系统作进一步的状态精简，从而得到与原系统等价的状态较少的状态空间，如图3所示。

图2 对称规约后的状态转移图图

图3 偏序规约后的状态转移图

3 基于JPF的Eclipse模型检测平台实现

JPF不仅可以实现对Java程序的模型检测功能，它还提供了很强的程序扩展功能。本文使用JPF的Eclipse的PDE来进行JPF插件的开发，使用PDE提供工程向导，新建一个Eclipse Plug-in项目。

3.1 分析插件要实现的功能，标识需要进行添加的扩展点

plugin.xml是插件和Eclipse内核的接口，它提供的扩展点非常多，常见的扩展点有透视图（perspectives）、视图（views）、编辑器（editors）、首选项（preferencePages）、帮助（toc）和上下文帮助（context）。需要为每个class关联一个配置文件（后缀为.cjp），通过读取cjp文件的配置信息，使用JPF来检测目标class文件。首先在工具栏中设计一个按钮来启动插件的配置对话框，用于配置和管理被检测类的配置文件，然后还需要专门的面板来并显示检测的结果。

3.2 根据扩展点的规范来实现这些扩展

新建一个类MyJpfButtonAction，实现接口IWorkbenchWindowActionDelegate，然后在run（）方法中添加实现打开配置对话框的代码。

然后，需要定义两个视图，一个用于管理配置需要验证的文件，另一个用来显示验证的结果。作为view的扩展，它必须继承ViewPart类，将它们分别命名为OutputView和TopicView。让他们重载父类的createPartControl（）方法，来设计各自的面板内容。在OutputView中，设计一个列表来显示线程选择信息，当用户点击某个线程时，在右边显示线程检测的详细信息，为了实现此功能，让OutputView类实现JFace的一个视图UI接口ISelectionChangedListener。

添加一个右键菜单项，新建两个类JavaClass LaunchAction和RunJpfAction，实现接口IObjectActionDelegate。在JavaClassLaunchAction的run（）方法中使用IProject和IFile来为class文件创建配置文件，并初始化配置文件的内容。在RunJpfAction的run（）方法中调用JPF来完成指定文件的检测工作。

图4 配置面板

3.3 编辑plugin.xml文件

PDE为插件清单文件plugin.xml提供了专门的插件清单编辑器。PDE中的插件编辑器为多页编辑器，其中包括概述、依赖项、运行时、扩展、扩展点、编译、MANIFEST.MF、plugin. xml和build.properties等，可在每个配置页面中为其定制相关的属性。为每一个扩展点添加一个＜extension＞节点，然后在子节点中配置扩展点的id、实现类的路径、名称、图标、标签文字等扩展点属性。

调用JPF来执行检测功能，需要设计一个专门的类来完成此项工作。新建一个类VerifyJob，继承Eclipse的核心类Job，该类包含4个主要属性：IFile变量来存储配置文件信息，Config变量来自JPF的配置类，布尔型变量step指示是否单步执行，PrintStream变量用于输出。根据默认的配置文件和用户自定义的配置文件，生成JPF的Config对象，然后在VerifyJob的run（）方法中使用Config对象构造一个JPF对象，最后执行JPF的run（）方法。自定义一个监听器，用于检测并输出JPF的检测结果，然后通过调用JPF的addSearchListener（）和addVMListener（）方法，将该监听器添加到当前的JPF对象中去。

3.4 插件测试、打包与发布

PDE提供了很方面的测试、调试手段。每添加一次代码，就可以通过在插件项目上点击鼠标右键，选择”Run As Eclipse Application”来测试新插件的功能效果。当然，最终的测试，需要将打包发行后的插件安装到Eclipse中来观察插件的工作情况。

插件项目在打包时，仅将src源文件对应的编译文件打成一个jar包。其它文件如xml、图像文件等都需要手工复制到打包目录下。可使用Eclipse导出功能，或Ant来打包插件。

Eclipse还可以通过新建一个Update Site项目的方法，将新的插件以网页的形式发布出去。利用建立Update Site项目向导，最终会形成一个web目录，该目录下包含了你要发布的plugins和features文件夹，另外还有一个site.xml文件和一个index.html文件。site.xml中定义了改更新站点可以提供的插件的下载路径，这样用户可以通过Eclipse的UpdateManager来在线安装插件。

4 实例应用分析

为测试JPF的死锁检测功能，首先创建一个存在死锁问题的Java类Deadlock，该类实现Runnable接口，在mian（）函数中启动两个Deadlock对象，并用synchronized控制对象本身的访问。考虑这样一种情况：1）线程T1在对象t1上同步，然后调用对象t2的foo方法，允许被抢先执行。2）另一个线程T2开始执行，在对性t2上同步。3）T2获得t2，继续执行，企图获得t1，调用t1的foo方法。但获取失败，因为T1占有t1。于是，T2阻塞，等待T1释放t1。4）轮到T1继续执行，T1试图获得t2，但不能成功，因为t2已经被T2占有了。至此，T1和T2都被阻塞，程序死锁。配置JPF，实现死锁检测。

在运行Deadlock类后，由于配置了NotDeadlockedProperty属性，JPF可以很快发现程序中的死锁问题，并输出导致死锁的程序执行路径。JPF的出现，为Java程序模型检测注入了新的力量，它在许多方面都得到了实际应用，包括航天软件的研制、实时系统验证和网络协议验证[等。Eclipse是Java程序员比较常用的一种Java编辑工具，利用JPF在其基础上开发一款Java模型检测工具是非常有意义的，可以使得程序员在编写程序的同时检测程序代码的逻辑正确性。

[1]杨明远,罗贵明.一种大规模并行程序模型的检测方法[J].计算机工程,2008,34,（13）：72-74.

[2]钟诚,唐春艳.运用类复制变异和JPF技术生成类间测试用例[J].小型微型计算机系统,2009,30,（8）.