Unified syntax for ASM

P. Arcaini, S. Bonfanti, M. Dausend, A. Gargantini, A. Mashkoor, A. Raschke, E. Riccobene, P. Scandurra, M. Stegmaier. Unified syntax for ASM. volume 9676, pages 231-236, DOI 10.1007/978-3-319-33600-8_14, 5, 2016.

  • Paolo Arcaini
  • Silvia Bonfanti
  • Marcel Dausend
  • Angelo Gargantini
  • Atif Mashkoor
  • Alexander Raschke
  • Elvinia Riccobene
  • Patrizia Scandurra
  • Michael Stegmaier
  • Michael Butler
  • Klaus-Dieter Schewe
  • Atif Mashkoor
  • Miklós Biró
BuchAbstract State Machines, Alloy, B, TLA, VDM, and Z - Proc. ABZ 2016
TypIn Konferenzband
SerieLecture Notes in Computer Science

Among the different frameworks for the ASM method (like AsmL, ASM Workbench, ASMGofer, KIV), two of the main ones are ASMETA and CoreASM. These platforms provide industrial strength tools to specify, verify, simulate, and test ASM models. However, they implement different dialects of the pseudo code notation and support slightly different extensions of the original definition. Thus, while the availability of multiple support platforms is obviously an advantage, it may also be confusing for new adopters of the method. Moreover, designers cannot share models among the tools (unless a translator or adapter is defined) and thus cannot easily take advantage of each tool's strengths. To overcome these limitations, the idea of a common syntax definition “Unified ASM” (UASM), driven by the community, open to any actors, has grown in the last two years. This paper presents the activities performed so far. The challenges of this project are both to preserve various useful extensions of the different tools and support a variety of application scenarios. On the one hand, the UASM language should be usable for communication with customers and non-experts but, on the other hand, precise enough to allow automatic analysis (like type checking, property verification, etc.). Moreover, we will try to identify unifying solutions for those ASM aspects for which the two frameworks made different design decisions. Two examples are the syntax and semantics for state initialization and the definition of basic data types.