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:
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:
A tool demo is available as a Gradle project, implementing the examples above, here.