Research And Design Of Symbolic Execution Based Software Testing

The rapid development of computer technology leads to an unprecedented expansion of software code.While the scale of code can be much lager and the software reliability is increasing,how to ensure the quality of software products through all-round high-precision and high-efficiency test methods has become the core problem of software testing.There are many problems in both the test case generation and the program defect detection and the source model checking: randomly generated test cases and manual writing test cases have low effectiveness and can cost a lot of time and labor.It's hard to keep the quality and efficiency of program;IDE and static analysis tools can only detect program errors in syntax and some simple logic errors,dynamic testing tools such as Valgrind only supports limited types of error detection and the comprehensiveness depends on the high coverage of test case;in the field of model checking,software model checking needs to give a description of model by human in general.Some testing tools fetch Boolean logic of program,but they can not check on source level.In order to solve the problems that need to be studied and solved imminently,this thesis makes a deep exploration of them based on symbolic execution technology.In test case generation,it can generate high coverage test cases based on the LLVM-IR instruments and symbolic execution technology.In the aspect of defect detection,it can take a comprehensive and in-depth dynamic detection with the instruments for the buffer overflow,memory leakage and other defects.In the aspect of model checking,an attribute description format is established,and then the transformed attribute rule is added to the constraints to take symbolic execution.Finally,in order to combine testing and the development process and continuous integration,a comprehensive automated test system was created,which made a further study for the application of symbolic execution technique in software testing.From the test results,the system supports some basic types in the C/C++ program,including floating type.The branch coverage can reach one hundred percent on a small scale program testing;it can take a comprehensive testing on buffer overflow,memory leak,memory double free for each branch;system can judge some basic attribute according to the symbolic constraints which transformed from logical properties description.The research and design combined development and automated testing successfully,which generate test case automatically,defecting detection dynamically and automatically,checking the model based on source during the development process of program.