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

• 作者: 刘全 陈冬火
• 来源期刊: 计算机研究与发展
• 学科: 工学
• 关键词: 测试用例自动产生 符号执行 公式重写 模型检验 线性时序逻辑 输入/输出符号变迁系统
• 年，卷（期）: 2013,（12）
• 所属期刊栏目: 软件测试
• 页码范围: 2661-2675
• 页数: 15页
• 分类号: TP311
• 字数: 14864字
• 语种: 中文

摘要

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