Giving a Model-Based Testing Language a Formal Semantics via Partial MAX-SAT

Abstract : Domain-specific Languages (DSLs) are widely used in model-based testing to make the benefits of modeling available to test engineers while avoiding the problem of excessive learning effort. Complex DSLs benefit from a formal definition of their semantics for model processing as well as consistency checking. A formal semantics can be established by mapping the model domain to a well-known formalism. In this paper, we present an industrial use case which includes a mapping from domain-specific models to Moore Machines, based on a Partial MAX-SAT problem, encoding a predicative semantics for the model-to-model mapping. We show how Partial MAX-SAT solves the frame problem for a non-trivial DSL in which the non-effect on variables cannot be determined statically. We evaluated the performance of our model-transformation algorithm based on models from our industrial use case.