Automated test generation for software components

This report presents a method developed as a part of the LIME-project (Lightweight formal Methods for distributed component-based Embedded systems) for generating test cases for software components. The main technique employed in this work is dynamic symbolic execution, where a program is executed both concretely and symbolically at the same time. During an execution a set of symbolic constraints is collected describing the input values that will force the program to follow an unexplored execution path. By solving the collected constraints new input values are obtained allowing each test run to exercise different behaviour of the program. Based on the methods developed in this work, a tool has been implemented that can be used for automated testing of sequential Java programs