基于符号执行的复杂软件系统测试与验证研究

Symbolic Execution is one of the most important topics which promote the research of software testing and verification. There are two main obstacles which restrict the analysis of complex software systems by symbolic execution. First, guided traversing of large scale state space of software code. Second, the constraint solving of code with complex characteristics, e.g. floating point computations, nonlinear constraints, third party function calls. ..The main research threads of this project is organized to break through the above two obstacles. This project attacks the key problems behind symbolic execution based test generation, automatic analysis of program behavior and bounded model checking of software code, and will increase the efficiency and scalability of software testing and verification techniques and tools. In detail, the research problems of this project include: deep behavior coverage guided symbolic execution, test case generation with complex program characteristics, complex property guided code behavior detection, and path encoding and traversing based code bounded verification.

近年来符号执行技术成为大力推动软件测试与验证领域研究工作的热点之一。面对复杂软件系统的测试与验证需求，当前符号执行技术受困于两大主要障碍：一是大规模程序状态空间的制导遍历，二是包含复杂程序特征（浮点计算、非线性约束、第三方库函数调用等）的约束问题求解。..本项目以突破符号执行技术面临的这两大障碍为主线，基于符号执行技术解决测试用例生成、程序行为自动分析、代码有界模型检验中的关键问题，进一步提升相关测试和验证技术与工具的有效性和可扩展性。具体研究内容包括面向深度覆盖的符号执行制导、面向复杂程序特征的测试用例生成、面向复杂性质的程序行为自动检测、基于程序路径编码和遍历的有界模型检验。

符号执行是软件测试与验证领域的重要支撑性技术。面对复杂软件系统的测试与验证需求，已有符号执行技术受困于两大主要障碍：一是大规模程序状态空间的制导遍历，二是包含复杂程序特征（浮点计算、非线性约束、第三方库函数调用等）的约束问题求解。.本项目针对复杂软件系统测试与验证需求，突破符号执行技术面临的障碍，在面向深度覆盖的符号执行制导、面向复杂程序特征的测试用例生成、面向复杂性质的程序行为自动检测、基于程序路径编码和遍历的有界模型检验等方面取得一系列重要进展，进一步提高了软件测试与验证技术的有效性和可扩展性；在此基础上研制了基于程序路径遍历的代码有界验证工具、基于智能化学习与搜索的复杂代码符号执行工具、基于正规性质引导的符号执行工具、基于符号执行与模型检验的符号化验证工具、C程序单元级符号执行工具等原型工具，并在工业界开展了实际验证与应用。