SMT Aided Test Case Generation For Constrained Feature Models

With the development of highly configurable and large software, a new challenge has to be addressed, when it comes to software testing. While traditional testing approaches might still apply and succeed in achieving a better quality of service, the high degree of customizable parts of such a system implies the mentioned testing activities on different configurations. If a formal notion is used to express the allowed configurations of a system, one might think of generating such configurations in an automated fashion. However, if there are constraints involved, traditional model-based test-case generation might cause problems to achieve a desired coherency. An idea is, to use those constraints to generate test-cases and to achieve coherency at the same time. Satisfiability modulo theories (SMT) has been an emerging field in current theoretical computer science and developed decision procedures to treat various theoretical fragments in a specific manner. The goal of this thesis is, to look at a translation mechanism from an expression language for constraints into SAT modulo theories and involve this technique into a test-case generation process. Furthermore, the balance between the generation of coherent test-cases as well as the problem-specific purposes of such test-cases is investigated