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

Bernhard Aichernig, Christian Burghard*

*Corresponding author for this work

Research output: Chapter in Book/Report/Conference proceedingConference paperpeer-review


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.

Original languageEnglish
Title of host publicationTesting Software and Systems - 32nd IFIP WG 6.1 International Conference, ICTSS 2020, Proceedings
EditorsValentina Casola, Alessandra De Benedictis, Massimiliano Rak
Number of pages17
Publication statusPublished - 2020
Event32nd IFIP International Conference on Testing Software and Systems: ICTSS 2020 - Virtuell, Italy
Duration: 9 Dec 202011 Dec 2020

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume12543 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349


Conference32nd IFIP International Conference on Testing Software and Systems
Abbreviated titleIFIP-ICTSS 2020


  • Consistency checking
  • Formal semantics
  • Frame problem
  • Model transformation
  • Partial MAX-SAT
  • Partial moore machines

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Fields of Expertise

  • Information, Communication & Computing


Dive into the research topics of 'Giving a Model-Based Testing Language a Formal Semantics via Partial MAX-SAT'. Together they form a unique fingerprint.

Cite this