基于符号执行的软件静态测试研究  

Software Static Test Research Based on Symbolic Execution

作　　者：梁娟娟[1] 刘久富[1] 朱丹丹[1] 陈柯[1] 

机构地区：[1]南京航空航天大学自动化学院,江苏南京210016

出　　处：《计算机技术与发展》2013年第6期42-45,178,共5页Computer Technology and Development

基　　金：国家自然科学基金资助项目(60674100);南京航空航天大学青年科学创新基金(NS2010069)

摘　　要：文中基于符号执行理论,设计了一种面向C语言的静态分析方法。通过词法分析和语法分析构建了程序的抽象语法树,并在此过程中对源代码进行规范性检查,再根据函数调用关系与抽象语法树来确定程序分析层次,并通过约束求解器确定程序中每一条可执行路径,最后依照程序的可执行路径得到每个变量最终的符号执行结果。该方法支持基于C语言文法的程序规范性检查,便于代码质量度量。利用该方法得到的抽象语法树,可开展静态构架分析,同时利用变量值的符号表达式可辅助测试用例生成,有助于提高测试的效率和质量。Design a C static analysis method based on analyzed symbolic execution theory. It constructs the program＇s abstract syntax tree by using lexical analysis and grammatical analysis and does regular inspect for the source code in the process ;then according to the function calls relationship and abstract syntax tree to determine program analysis level and the executable path is determined by the constraint solver;eventually get the final symbolic execution results of each variable through the executable path. It is helpful for measuring code quality by regular inspecting on the source based on C language grammar. It is convenient for anglicizing the static structure of program by using SAT. The symbolic expressions, which were generated by this method can assist generating of test data and improve efficiency and quality of software test.

关 键 词：静态分析 符号执行 抽象语法树 可执行路径 

分 类 号：TP311[自动化与计算机技术—计算机软件与理论]