Research And Design Of Symbolic Execution Based Automatic Test Case Generation Tool

Software testing is an important way to ensure software quality and improve software reliability. Test cases occupied a pivotal position in a in a variety of testing methods. This thesis is focused on the research of how to generate high coverage test cases sets quickly in the software testing process. Two key technologies are used. The first one is symbolic execution, it is mainly used to construct execution paths of the tested program automatically, and these constructed paths are meant to be non-redundant. The second one is satisfiability modulo theories(SMT), it is used to generate real test case inputs for the corresponding execution path constructed before. Due to the non-redundant characteristic of these paths, the test cases are non-redundant too, so they can reach higher coverage than the traditional test case sets generated randomly. The research and design of this thesis is mainly divided into the following parts:First, this thesis investigates the background, history, research status, principles and problems faced of the symbolic execution techniques systematically. And then this thesis makes a detailed study of six dynamic symbolic execution tools, and makes comparisons of a variety of the somewhat famous dynamic symbolic execution tools in the field.Second, this thesis shows the research on SMT solving technique, it makes a summary of the current effective solver, and then this thesis presents the study summary of the SMT-LIB language and its script provided by Satisfiability Modulo Theories community. These researches offered the theoretical foundation for the constraints solve optimization of later.Third, this thesis makes a summary of the defects of the implementation mechanisms and structures of the current various dynamic symbolic execution tools. In order to generating test cases for software running in various platforms, a C/S-based dynamic execution architecture is designed and implemented to isolate tested programs and testing tool,, this tool can provides test cases generation service for programs running in various platforms for multiple users at one time without change the implementation of the test case generation logic.Fourth, based on the first and the second research, this thesis proposes some solutions to alleviate the path explosion problem and constraint solving problem. For constraint solving, a universal SMT solvers calling interface is designed to make tool adapt to different SMT solvers, which can make the testing tool and SMT solvers loosecoupled. For the path explosion problem, a variety of intelligent search strategies are designed and implemented to provide different coverage standards and to obtain high branch coverage in limited time. And also a parallel mechanism is designed to improve the efficiency of the test case generation tool.Based on the research contents above, this thesis designs and implements a symbolic execution based automatic test case generation tool named AUTCS eventually, AUTCS can provide remote automatic test case generation service for multiple users at the same time, it provides a variety of intelligent coverage criteria, and several optimization schemes are implemented to solve the disadvantage of the architecture and the problems faced by symbolic execution technique.