Shadow Symbolic Execution with Java PathFinder
Shadow Symbolic Execution with Java PathFinder
复制标题
使用 Java PathFinder 进行影子符号执行
DOI：
--
复制
发表时间：
2018
期刊：
影响因子：
--
通讯作者：
Timo Kehrer
中科院分区：
文献类型：
--
作者：
Yannic Noller;Hoang Lam Nguyen;Minxing Tang;Timo Kehrer
回归测试确保软件系统在发展时仍然正确执行，并且更改不会引入意外的副作用。然而，创建显示不同行为的回归测试用例需要大量的工作。一个解决方案是影子符号执行的想法，最初是基于KLEE为C编写的程序实现的，它采用新旧程序的统一版本，并执行由具体值指导的符号执行，以探索改变的行为。在这项工作中，我们将影子符号执行的想法应用到Java程序中，因此，提供了一个扩展的Java Path（JPF）项目执行影子符号执行Java字节码。该扩展已应用于JPF测试类中的几个主题，在这些主题中，它成功地生成了暴露回归测试相关分歧的测试输入。
Regression testing ensures that a software system when it evolves still performs correctly and that the changes introduce no unintended side-effects. However, the creation of regression test cases that show divergent behavior needs a lot of effort. A solutionis the idea of shadow symbolic execution, originally implemented based on KLEE for programs written in C, which takes a unified version of the old and the new program and performs symbolic execution guided by concrete values to explore the changed behavior. In this work, we apply the idea of shadow symbolic execution to Java programs and, hence, provide an extension of the Java PathFinder (JPF) project to perform shadow symbolic execution on Java bytecode. The extension has been applied on several subjects from the JPF test classes where it successfully generated test inputs that expose divergences relevant for regression testing.