Domain-Specific Modelling Languages (DSMLs) are languages dedicated to modelling in specific application areas. Recently, the design of DSMLs has become widely accessible to engineers trained in the basics of Model-Driven Engineering (MDE): one designs a <it>metamodel</it> for the language’s abstract syntax; then, the language’s operational semantics is expressed using <\it>model transformations</it> over the metamodel.
The democratisation of DSML design catalysed by MDE is likely to give birth to numerous languages. One can also reasonably expect that there shall be numerous errors in those languages. Indeed, getting a language right (especially its operational semantics) is hard, regardless of whether the language is defined in the modern MDE framework or in more traditional ones.
Formal approaches can benefit language designers by helping them avoid or detect errors. But, in order to be accepted by nonexpert users, formal approaches have to operate in the background of a familiar language design process, such as the \mde-based one mentioned above.
We propose here such an approach, which uses the K-semantic framework to formalise the basic MDE ingredients used in DSML definition: models, metamodels, and model transformations.