基于JPF的Java程序验证

Verification of Java Program Using JPF

形式化方法是提高并发系统的安全性与可靠性的重要手段。JPF(Java Pathfinder)是一种精确的Java字节码状态模型检测工具。在阐述JPF工作原理的基础上,提出了一种适用于JPF的Java程序模型检测方法,包括Java程序模型的建立、状态空间搜索算法的扩展和配置,开发了Java程序反例轨迹轻量级的输出监听器。对Java程序实例进行验证,结果表明:该方法能有效地检测出多线程Java应用程序中难以检测到的并行漏洞。

Formal methods is one of the most important ways to promote the safety and reliability of concurrent system.JPF（Java Pathfinder） is a kind of explicit state model checker for Java bytecode.Based on the introduction of the working principles of JPF,this paper proposed an approach for model checking to verify Java programs used in JPF,including how to build Java program model,extend and configure the algorithms for state space searching,and develop a lightweight listener for JPF to output the Java program counterexample traces.Through verifying a Java program by using the model checking procedures mentioned above,the result shows that this method can find the parallel bugs in the multithreaded Java applications effectively,which is hard to be detected in normal ways.