Multilevel modelling (MLM) approaches make it possible for designers and modellers to work with an unlimited number
of abstraction levels when specifying domain-specific modelling languages (DSMLs). In this paper, we present a functional
infrastructure that allows modellers to define the structure and the operational semantics of multilevel modelling hierarchies,
enabling simulation and analysis. Using the MultEcore tool, one can design and distribute the models that compose the
language family in a multilevel hierarchy, and specify their behaviour by means of multilevel transformation, so-called
multilevel coupled model transformations. We give a rewrite logic semantics to MultEcore’s MLM, on which we have based
our automated transformation from MultEcore to the rewriting logic language Maude. Then, we rely on Maude to execute
MultEcore models and to support analysis techniques, like reachability analysis, bounded and unbounded model checking of
invariants and LTL formulas on systems with both finite and infinite reachable state spaces using equational abstraction. We
illustrate our developed techniques on a DSML family for Petri nets.
