In Domain-Specific Modelling (DSM) the general goal is to provide Domain-Specific Modelling Languages (DSMLs) for domain users to model systems using concepts and notations they are familiar with, in their problem domain. Verifying whether a model satisfies a set of requirements is considered to be an important challenge in DSM, but is nevertheless mostly neglected. We present a solution in the form of ProMoBox, a framework that integrates the definition and verification of temporal properties in discrete-time behavioural DSMLs, whose semantics can be described as a schedule of graph rewrite rules. Thanks to the expressiveness of graph rewriting, this covers a very large class of problems. With ProMoBox, the domain user models not only the system with a DSML, but also its properties, input model, run-time state and output trace. A DSML is thus comprised of five sublanguages, which share domain-specific syntax, and are generated from a single metamodel. Generic transformations to and from a verification backbone ensure that both the language engineer and the domain user are shielded from underlying notations and techniques. We explicitly model the ProMoBox framework's process in the paper. Furthermore, we evaluate ProMoBox to assert that it supports the specification and verification of properties in a highly flexible and automated way.

Domain-Specific Modelling Languages (DSLs) allow domain experts to create models using abstractions they are most familiar with. A DSL's syntax is specified in two parts: the abstract syntax defines the language's concepts and their allowed combinations, and the concrete syntax defines how those concepts are presented to the user (typically using a graphical or textual notation). However important concrete syntax is for the usability of the language, current modelling tools offer limited possibilities for defining the mapping between abstract and concrete syntax. Often, the language designer is restricted to defining a single icon representation of each concept, which is then rendered to the user in a (fixed) graphical interface. This paper presents a framework that explicitly models the bi-directional mapping between the abstract and concrete syntax, thereby making these restrictions easy to overcome. It is more flexible and allows, amongst others, for a model to be represented in multiple front-ends, using multiple representation formats, and multiple mappings. Our approach is evaluated with an implementation in our prototype tool, the Modelverse, and by applying it on an example language.

Domain-specific modeling (DSM) is one major building block of model-driven engineering. By moving from the solution space to the problem space, systems are designed by domain experts. The benefits of DSM are not unique to the design of systems, the specification and verification of desired properties of the designed systems by the help of DSM seems the next logical step. However, this latter aspect is often neglected by DSM approaches or only supported by translating design models to formal representations on which temporal properties are defined and evaluated. Obviously, this transition to the solution space is in contradiction with DSM.