基于符号执行和LTL公式重写的测试用例产生方法

Generation of Test Cases Based on Symbolic Execution and LTL Formula Rewriting

基于模型检验等形式化方法的测试用例自动产生技术成为测试自动化领域一项重要的进展.对于输入和输出为无界抽象数据类型的无限状态系统,利用传统模型检验技术难以有效地产生测试用例集合,提出基于符号执行和公式重写的测试用例产生方法.通过建立程序的符号化执行模型,避免输入和输出变量数值化枚举而导致的无限状态系统的建模和状态爆炸问题;建立基于符号化执行模型的时序公式重写规则,并根据线性时序逻辑(linear temporal logic,LTL)公式的反例模式求取复杂属性及行为约束关系,利用约束求解的方法自动产生测试用例集合.这种方法集成了符号执行技术和时序公式状态重写——一种轻量级模型检验技术,成为基于复杂抽象数据类型系统与属性相关的测试用例自动产生的有效方法.

It is a breakthrough to use model checking technique to automatically generate test cases. For infinite states systems with input/output domains defined on unbounded and types, the function of general model checking technique is very restricted in generating test cases. This paper presents the idea of auto-generation of test cases based on symbolic execution and LTL temporal formula rewriting method. The method proceeds with building the symbolic representation of program execution model, such that it can avoid explicitly building the model of infinite states systems with the enumeration of value of input and output or state explosion problem. Then temporal formula （test purposes） rewriting is applied to the symbolic execution model of program to generate complex constraint requirements according to the counterexample patterns related to test purposes and the suitable SMT（satisfiability modulo theory） solver is called for generating test cases. At the level of syntax, IOSTS and LTL formulae are used to specify interactive behaviors of systems under testing and test purposes, respectively. Therefore, the approach has the advantages of modeling the behaviors and data dependence as well as defining all kinds of test requirements concisely and naturally in a rigorous means. Further, the paper designs the algorithm for LTL formula rewriting engine, which computes the necessary condition satisfied by test cases related to the targeted test purposes. At last, a case study is conducted for showing the usefulness of the method.