Transformation rules from UML4MBT meta-model to SMT meta-model for model animation
Jérôme Cantenot, Fabrice Ambert, Fabrice Bouquet · 2012
In the Model Based Testing domain, one of the bottleneck elements is the tests generation (time or reachability). In literature, one of the efficient solutions to evaluate a formula is to use an SMT solver. However the input language, SMT-lib, used by the solvers is not adapted to human modelling. To model we choose to use a sufficient sub-part of UML/OCL for Model Based Testing generation, called UML4MBT. This sub-part has been formalized with a meta-model. In this paper, we define the SMT meta-model and we describe the transformation rules from the UML4MBT meta-model to the SMT meta-model. We give the results of the experiments on a first implementation of the rules.