Test Case Generation using Model Checking for Software Components Deployed into New Environments

In this paper, we show how to generate test cases for a component deployed into a new software environment. This problem is important for software engineers who need to deploy a component into a new environment. Most existing model based testing approaches generate models from high level specifications. This leaves a semantic gap between the high level specification and the actual implementation. Fur-thermore, the high level specification often needs to be man-ually translated into a model, which is a time consuming and error prone process. We propose generating the model automatically by abstracting the source code of the com-ponent using an under-approximating predicate abstraction scheme and leaving the environment concrete. Test cases are generated by iteratively executing the entire system an