Maudeling is an Eclipse developed enviroment, based on Maude, that allow users to specify models, metamodels, and their dynamic behavior. Maude offers a comprehensive toolkit for automating formal analysis of specifications (such as reachability analysis, model checking, or theorem proving) efficient enough to be of practical use.

The new versions of Maudeling has adopted a new representation for models and metamodels, improving its efficiency. In this page you can find all the necessary Maude files to perform the analysis. A graphical editor will be available soon (see E-Motion tool).


To run the example, open (the last alpha of) Maude 2.3, copy Maudeling Maude files and Production system example maude files in the same folder, and load the file PSExample.maude. Now you are aready to simulate and analyze the specifications using, e.g., the commands commented at the end of the file (PSExample.maude).