Rewriting Logic and Maude for the Formalization and Analysis of DSMLs, and the Prototyping of MDSE Tools

Abstract

A few years ago, Antonio Vallecillo and I initiated a long-term collaboration on different matters related to MDSE. In particular, we were interested on the possibilities of analysing models, long before they were implemented. For that, we explored the possibility of graphically defining the behavior of systems and DSMLs. Then, using Maude as back-end tool, and by defining a model transformation between our language for DSML definition and Maude, we were able to execute and analyze DSMLs defined in this way. The simplicity of the setting, and the reduced effort in its implementation allowed us to explore the possibility of considering time-related features, different forms of analysis, including reachability analysis, model checking, and statistical model checking. The same ideas have later been also applied to multi-level modeling in the MultEcore system. This paper summarizes the main contributions by Antonio and myself on these matters.

Keywords

Rewriting logic, Maude, domain-specific modeling languages, timed systems, multi-level modeling, formal verification.

Cite as:

Francisco Durán, “Rewriting Logic and Maude for the Formalization and Analysis of DSMLs, and the Prototyping of MDSE Tools”, Journal of Object Technology, Volume 21, no. 4 (October 2022), pp. 4:1-12, doi:10.5381/jot.2022.21.4.a2.