Supporting testing using the KLEE test generator

OData support
Dr. Micskei Zoltán Imre
Department of Measurement and Information Systems

Today it is very hard to live without using or benefiting from software at all. Moreover, some of these software are safety-critical and may risk human life if not working correctly. Thus, one of the main challenges of software development is to develop programs with sufficient reliability and safety for the given domain and requirements. When creating a software, how can we tell, if it works as stated in the specification and it does not misbehave? The most fundamental method tackling this problem is software testing.

When doing manual testing, equivalence partitioning often comes up as a good way for defining sufficient number of test inputs. Equivalence partition basically stands for defining ranges of an input value where each range is treated the same by the specification.

Besides manual work, the demand for automatic tools supporting software testing is constantly growing as software projects are getting more and more complex and trends like continuous delivery tries to make the developing process faster and faster. One type of software testing supporting tools are test generators. In my thesis, I am going to introduce several aspects of software testing, but the emphasize is going to be on test generation, especially when symbolic execution is being used for it.

Symbolic execution is a technique where the program is executed without concretizing its input parameters. Today there are more and more freely available tools using this technique. One of these free tools is KLEE, which is used for generating test cases for C language programs and will be introduced in details with its pros and cons.

The main work of my thesis is to extend the KLEE with a feature to make it more usable for industrial uses. In most cases, generated tests can be hardly interpreted, thus it would be rewarding if the equivalence partitions could also be generated. The extension I have developed gives more insights for the testers about the execution paths of the tested program by extracting and displaying in a readable format the most important equivalence partitions. With the use of this, testers could compare the generated partitions to the already defined ones and could check if some partitions were missing or wrong. They could also revise their current test suites or the partitions could even be used at the test planning phase.

The solution has been tested on various test programs to show that it can handle the basic C language elements well. It can deal with most of the basic types, decision statements, loops, function calls and also structs and arrays. It has also been tested on an industrial code used for (aircraft) traffic collision avoidance system.


Please sign in to download the files of this thesis.