计算机研究与发展
計算機研究與髮展
계산궤연구여발전
JOURNAL OF COMPUTER RESEARCH AND DEVELOPMENT
2013年
12期
2661-2675
,共15页
测试用例自动产生%符号执行%公式重写%模型检验%线性时序逻辑%输入/输出符号变迁系统
測試用例自動產生%符號執行%公式重寫%模型檢驗%線性時序邏輯%輸入/輸齣符號變遷繫統
측시용례자동산생%부호집행%공식중사%모형검험%선성시서라집%수입/수출부호변천계통
auto-generation of test cases%symbolic execution%formula rewriting%model checking%linear temporal logic (LTL)%input/output symbolic transition system (IOSTS)
基于模型检验等形式化方法的测试用例自动产生技术成为测试自动化领域一项重要的进展.对于输入和输出为无界抽象数据类型的无限状态系统,利用传统模型检验技术难以有效地产生测试用例集合,提出基于符号执行和公式重写的测试用例产生方法.通过建立程序的符号化执行模型,避免输入和输出变量数值化枚举而导致的无限状态系统的建模和状态爆炸问题;建立基于符号化执行模型的时序公式重写规则,并根据线性时序逻辑(linear temporal logic,LTL)公式的反例模式求取复杂属性及行为约束关系,利用约束求解的方法自动产生测试用例集合.这种方法集成了符号执行技术和时序公式状态重写——一种轻量级模型检验技术,成为基于复杂抽象数据类型系统与属性相关的测试用例自动产生的有效方法.
基于模型檢驗等形式化方法的測試用例自動產生技術成為測試自動化領域一項重要的進展.對于輸入和輸齣為無界抽象數據類型的無限狀態繫統,利用傳統模型檢驗技術難以有效地產生測試用例集閤,提齣基于符號執行和公式重寫的測試用例產生方法.通過建立程序的符號化執行模型,避免輸入和輸齣變量數值化枚舉而導緻的無限狀態繫統的建模和狀態爆炸問題;建立基于符號化執行模型的時序公式重寫規則,併根據線性時序邏輯(linear temporal logic,LTL)公式的反例模式求取複雜屬性及行為約束關繫,利用約束求解的方法自動產生測試用例集閤.這種方法集成瞭符號執行技術和時序公式狀態重寫——一種輕量級模型檢驗技術,成為基于複雜抽象數據類型繫統與屬性相關的測試用例自動產生的有效方法.
기우모형검험등형식화방법적측시용례자동산생기술성위측시자동화영역일항중요적진전.대우수입화수출위무계추상수거류형적무한상태계통,이용전통모형검험기술난이유효지산생측시용례집합,제출기우부호집행화공식중사적측시용례산생방법.통과건립정서적부호화집행모형,피면수입화수출변량수치화매거이도치적무한상태계통적건모화상태폭작문제;건립기우부호화집행모형적시서공식중사규칙,병근거선성시서라집(linear temporal logic,LTL)공식적반례모식구취복잡속성급행위약속관계,이용약속구해적방법자동산생측시용례집합.저충방법집성료부호집행기술화시서공식상태중사——일충경량급모형검험기술,성위기우복잡추상수거류형계통여속성상관적측시용례자동산생적유효방법.
