FMA-ATL

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

Modelling, Simulation and Verification of EMF-based Systems

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:
  • state model
  • system specification
  • property specification
  • simulation and verification
• Dining philosophers with two forks:
  • state model
  • system specification
  • property specification
  • simulation and verification
• Ring-based version of the leader election problem:
  • state model
  • system specification
  • property specification
  • simulation and verification

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

Credits

• 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.