Asmeta Overview

This site is dedicated to the Abstract State Machine Metamodel (AsmM, in brief), a metamodel for the Abstract State Machines (ASMs) formal method developed by following the guidelines of the Model-Driven Engineering (MDE).

We exploit the metamodelling approach suggested by MDE to achieve the goals of developing a unique notation for ASM, a notation independent from any specific implementation syntax and allowing a more direct encoding of the ASM mathematical concepts and constructs, and tacking the problem of ASM tool interoperability.

The AsmM can be seen as a pivot metamodel towards a definition of a standard family of languages for the ASMs and a systematic integration of ASM tools. Through metamodels and model transformations, the metamodel of each tool (usually not given explicitly, but is built-in into the tool that provide it) is linked to those of other tools by the logical pivot metamodel which abstracts a certain number of general concepts about ASMs.

The AsmM is defined by using EMF, the modelling framework proposed by eclipse. It was originally has been defined by using the MOF (v. 1.4) meta-language of the Object Management Group (OMG) framework.

The AsmM definition comprises:

  1. an abstract syntax, i.e., an EMF-compliant metamodel representing in an abstract way concepts and constructs of the ASM formalism as described in the ASM book;
  2. a concrete syntax (AsmetaL : the Asmeta Language), namely an EBNF (extended Backus-Naur Form) grammar derived from the AsmM (the abstract syntax) as a notation to be used by modelers to effectively write ASM models in a textual form;
  3. an interchange syntax, i.e., a standard XMI-based format automatically derived from the AsmM, for the interchange of ASM models among tools.

For the metamodel semantics, we adopt the ASMs semantics given in the ASM book.

A standard AsmM Library containing predefined ASM domains and functions is also provided.

Asmeta tool set

Around the AsmM we have developed and we are developing a set of tools:

  • (available) the AsmetaL compiler: to compile an Asm specification written in AsmetaL to xmi
  • (available) the AsmetaS simulator: to simulate an Asm specification
  • (available) Asmee: a plugin for eclipse for AsmetaL and AsmetaS
  • (available) the ATGT: a test generator for Asms
  • (available) the AsmetaV validator: to test/validate your Asm specification
  • (available) the AsmetaSMV model checker: to model check an Asm specification
  • (available) the AsmetaMA model advisor: to check for common defects of AsmetaL models
  • (available) the AsmetaRE: to generate executable ASMs from Use Case models
  • (available) the SCA-ASM: a language and an engine for service oriented components
  • (work in progress) a graphical editor
  • (work in progress) AsmetaL to coreAsm translator


Jul 12: we present the use of ASMs for testing web applications @ ICWE 2012
Jul 11: we present the SCA-ASM modeling language at the EUROMICRO SEAA 2011
Apr 10: we present the asmeta model advisor at the NFM 2010
Dic 09: we present asmeta to SMV at the ABZ conference 2010
Oct 08: we present asmeta at ICSEA 08
Sept 08: we present avalla and AsmetaV at ABZ 2008
Jun 08: we have almost completed the porting of asmeta to emf
Oct 07: Asmee has been presented at Eclipse-IT 07


Thanks to stan4j to provide us with their valuable tool. We use stan4j to analyze and improve Asmeta.