Asmeta Metamodel

The Abstract State Machine Metamodel (AsmM, in brief) is 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.