Test generation through programming in UDITA
Test generation through programming in UDITA
复制标题
通过 UDITA 编程生成测试
DOI：
10.1145/1806799.1806835
复制
发表时间：
2010
期刊：
影响因子：
--
通讯作者：
D. Marinov
中科院分区：
文献类型：
--
作者：
Miloš Gligorić;Tihomir Gvero;V. Jagannath;S. Khurshid;Viktor Kunčak;D. Marinov
我们提出了一种方法来描述使用非确定性测试生成程序的测试。要编写这样的程序，我们介绍UDITA，一个基于Java的语言与非确定性的选择操作符和接口生成链接结构。我们还描述了新的算法，生成具体的测试，有效地探索空间的所有执行的非确定性UDITA程序。我们实现了我们的方法，并将其整合到官方的、公开可用的Java Path（JPF）存储库中，JPF是一种流行的Java程序验证工具。我们通过为数据结构、重构引擎和JPF本身生成测试来评估我们的技术。我们的实验表明，使用UDITA的测试生成速度更快，并导致测试描述，更容易写比以前的框架。此外，UDITA的新的执行机制是必不可少的，使测试生成可行。使用UDITA，我们发现了Eclipse、NetBeans、Sun javac和JPF中的许多bug。
We present an approach for describing tests using non-deterministic test generation programs. To write such programs, we introduce UDITA, a Java-based language with non-deterministic choice operators and an interface for generating linked structures. We also describe new algorithms that generate concrete tests by efficiently exploring the space of all executions of non-deterministic UDITA programs. We implemented our approach and incorporated it into the official, publicly available repository of Java PathFinder (JPF), a popular tool for verifying Java programs. We evaluate our technique by generating tests for data structures, refactoring engines, and JPF itself. Our experiments show that test generation using UDITA is faster and leads to test descriptions that are easier to write than in previous frameworks. Moreover, the novel execution mechanism of UDITA is essential for making test generation feasible. Using UDITA, we have discovered a number of bugs in Eclipse, NetBeans, Sun javac, and JPF.