Font Size: a A A

Research And Implementation Of Symbolic Execution Technology For Host-Oriented Embedded Software

Posted on:2012-08-13Degree:MasterType:Thesis
Country:ChinaCandidate:J B LouFull Text:PDF
GTID:2178330338496016Subject:Precision instruments and machinery
Abstract/Summary:PDF Full Text Request
The software testing technology offers ensurence to the software quality, improves the software reliability, and reduces the cost of software. As its important component part, the static analysis lays particular emphasis on program structure analysising and normative validating. It does not have time- dependence and can find errors or bugs of software as early as possible. Because it can ensure the quality of software without running the program, it can dramatically reduce the cost of artificial by dynamic testing. By use of control flow analysis and data flow analysis, it can find program errors. In this way, we can improve the efficiency of review, test and maintenance.As an important method of the static test, symbolic execution uses abstract symbols to represent the value of variables for simulating the execution of program. It can be used to validate the operation rule of the program and understand the constraint relation between variables. It also can overcome the problom that the value of variables is uncertainty in analyzing process. Symbolic execution is useful for path sensitive program assessing, test data generating and code quality analysising.This thesis has strictly analyzed symbolic execution theory, then designed a C analysis method; by traversing abstract syntax tree, makes symbolic execution on the process which meeting the path constraint conditions; gets results of the program by using symbolic instead of value. It is helpful for measuring code quality by regular inspecting on the source based on C language grammar. It is convenient for analysising the static structure of program by using AST. The symbolic expression maded by this method can assist generate test data.This thesis improves symbolic execution algorithm for C/C++ preprocessing process, then has proposed a new method based on condition value; gets preprocessing variables and path conditions; then integrates program information by conditional values module; gets conditional values of variable values and accessibility conditional expression of code. This method can avoid the path feasibility analysis of traditional symbolic evaluation and reduce the algorithm complexity. By using this method, we can better understand the program struct and find practical solutions to refine header file hierarchy.Finally, the thesis has used VC++2005 to realize the host-oriented program static analysis system and completed testing C codes of the embedded Linux platform. The results verify The correctness and practicality of our method.
Keywords/Search Tags:embedded software testing, symbolic execution, constraint solving, preprocessing process, c-value
PDF Full Text Request
Related items