Formalising Domain-Specific Modelling Languages

We propose an approach for formalising Domain-Specific Modelling Languages (DSML). Our approach is based on representing models and metamodels as specifications in the Maude algebraic specification language. This provides us with abstract definitions of essential concepts of DSML (model-to-metamodel conformance, operational semantics, and model transformations) that naturally capture their intutive meanings. We also propose equivalent executable definitions for these notions, which can be directly used in Maude for verification. Finally, we show how DSML can be organised as institutions, and model transformation as institution morphisms. We focus on a class of institution morphisms that corresponds to Galois connections between the transition systems generated by two DSML’s operational semantics. Such connections formally capture various forms of semantical preservation that model transformations may satisfy.  

hosted by