Simulation and analysis of MultEcore multilevel models based on rewriting logic.

Abstract

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.