| Summary: | 碩士 === 國立交通大學 === 資訊科學與工程研究所 === 96 === Testing is one of the most important phases of software quality assurance,
for the process of software construction cannot guarantee the absence of bugs.
Dynamic and static analysis tools are maturely developed in recent years.
In 2005, the concept of concolic (combined word of concrete and symbolic) testing was proposed,
which combines static and dynamic program analysis methods.
In this thesis, we implement ALERT, a concolic testing framework
and an Unspecified Software Feature (USF) Checker based on ALERT.
By using automatic theorem prover library for satisfiability modulo theories,
we can analyze and determine the inputs to direct program's execution along particular paths.
With this mechanism, we can control the values in stack section.
It can also be used to manipulate the values of uninitialized variables
and to trigger specific behavior of the program.
We present a two-phase testing algorithm in this thesis.
In the first phase, we use dynamic analysis tool to retrieve real run-time information.
In the second phase, we analyze the program by using concolic testing method
with the data collected in the first phase.
The result generated by the prover will be the input for the next testing run.
This testing process iterates until a fault is found or all the program execution paths are enumerated.
We use this tool to resolve unspecified program features caused by uninitialized variables.
It successfully extracts the program behavior which cannot be found with traditional program analysis methods.
The method in this thesis resolves the information lost problem caused by source code instrumentation in the
process of testing and improves the accuracy of the test.
|
|---|
