Nowadays, complex software systems pose new challenges for engineers. Verification techniques are getting an important role during the design and implementation phase, since the increasing size and complexity of software leads to increased possibility of defects. Thorough testing during development is a key for the improvement of software quality, however choosing the appropriate test inputs can be a rather complex task in real-world environments.
Automation of test input generation can support the task of selecting the proper inputs. The test input generation procedure can be based on a behavioral model or on the source code itself. Dynamic symbolic execution is one of the latter techniques: it executes the source code symbolically (with symbolic variables and values) and refines the results with constraints derived from concrete executions. The technique is able to effectively discover execution traces of complicated software. However, its industrial application is hindered by the complexity of the technique and the lack of provided information for the test engineer. In this thesis, I present two techniques that are able to alleviate the work with automated test input generation based on symbolic execution.
The first presented technique is the visualization of symbolic execution, which maps the steps of the execution to nodes of an execution tree and enriches it with metadata information (e.g. source code locations, path conditions). The technique supports the better understanding of the execution by 1) decomposing the path conditions of each trace, 2) classifying the execution paths and 3) identifying situations when a trace exits from the unit under test. A tool was implemented and it is open-source and available online.
The second technique to support the industrial usage of symbolic execution is the automated isolation environment generation. Thus, it can automatically replace the external dependencies with doubles. The presented technique discovers the calls going outside from the unit under test, while analyzing them from several aspects. From the results of this analysis, the technique is able to generate source code for unit isolation.
Prototype implementations of both of the techniques were developed and examined through simple and also real-world examples.