  The ability to generate test data is often a necessary prerequisite for
automated software testing. For the generated data to be fit for its intended
purpose, the data usually has to satisfy various logical constraints. When
testing is performed at a system level, these constraints tend to be complex
and are typically captured in expressive formalisms based on first-order logic.
Motivated by improving the feasibility and scalability of data generation for
system testing, we present a novel approach, whereby we employ a combination of
metaheuristic search and Satisfiability Modulo Theories (SMT) for constraint
solving. Our approach delegates constraint solving tasks to metaheuristic
search and SMT in such a way as to take advantage of the complementary
strengths of the two techniques. We ground our work on test data models
specified in UML, with OCL used as the constraint language. We present tool
support and an evaluation of our approach over three industrial case studies.
The results indicate that, for complex system test data generation problems,
our approach presents substantial benefits over the state of the art in terms
of applicability and scalability.
