论文部分内容阅读
基于模型检验等形式化方法的测试用例自动产生技术成为测试自动化领域一项重要的进展．对于输入和输出为无界抽象数据类型的无限状态系统，利用传统模型检验技术难以有效地产生测试用例集合，提出基于符号执行和公式重写的测试用例产生方法．通过建立程序的符号化执行模型，避免输入和输出变量数值化枚举而导致的无限状态系统的建模和状态爆炸问题；建立基于符号化执行模型的时序公式重写规则，并根据线性时序逻辑（1ineartemporallogic，LTL）公式的反例模式求取复杂属性及行为约束关系，利用约束求解的方法自动产生测试用例集