Donghuo Chen and Shizhong Zhao
auto-generation of test cases, symbolic execution, formula rewriting, model checking
It is an attractive research topic to use model checking technique to automatically generate test cases in the research community of formal method and software testing, and recent years has witnessed many work. For infinite states systems with input/output domains defined on unbounded and abstract types, in many contexts, explicit finite state models are not attained easily with the reasonable cost, therefore, testing with traditional model checking is often disenabled. This paper presents the idea of auto-generation of test cases based on symbolic execution and 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. The core tool - FormalTCGenerator is developed and the case study is conducted.
Important Links:
Go Back
