Test generation with Satisfiability Modulo Theories solvers in model-based testing

This paper presents a framework for UML/OCL model test generation. This framework is based on three parts. The first part is the transformation from a UML/OCL model into a Satisfiability Modulo Theories (SMT) instance. The metamodel associated with the two models and the transformation rules are presented. The second part is the animation strategies used for the generation of SMT instances to compute test sequences. The paper studies five different types of strategy to build the first-order formula used by an SMT instance. The paper also gives the results of experiments on six case studies that were used to validate the method. Copyright (C) 2014 John Wiley & Sons, Ltd.