Strategies Comparison of Test Generation from UML Using SMT Solver

International audienceA principal challenge in Model-Based Testing is to generate tests within a reasonable time and without reducing the test coverage when the size and complexity of the model increases. In the last few years, SMT solvers have become able to solve complex first-order logic formulas with acceptable performance. To meet this requirement, we choose to use Satisfiability Modulo Theory (SMT) solvers. In this paper, we suggest three strategies to generate automatically tests from models written in UML4MBT, a subset of UML. These strategies are evaluated through several experimentations. In particular, we study the influence of the characteristics of the model and the use of multi-threading on the test generation time. All experiments are performed on models representing real life systems