FMA-ATL is an executable formalization of a large excerpt of the model transformation language ATL in Maude, which uses the following front-end languages:

- The Eclipse Modeling Framework (EMF) for defining metamodels and their models
- ATL for defining model transformations

FMA-ATL enables ATL both for modelling and for verifying EMF-based systems, i.e. systems whose state models are represented as Ecore models. In particular, it reuses Maude’s verification tools both to perform (possibly bounded) model checking of invariants and to model check LTL formulas in the resulting system models.

Several examples are available:

- Concurrent Append Problem:
- Dining philosophers with two forks:
- Ring-based version of the leader election problem:

A tool demo is available as a Gradle project, implementing the examples above, here.

- FMA-ATL uses AnATLyzer to parse ATL model transformations in the front-end.
- Maude4J: An Eclipse-independent version of Maude Development Tools for integrating Maude with Java.