Unified syntax for ASM

Authors Paolo Arcaini
Silvia Bonfanti
Marcel Dausend
Angelo Gargantini
Atif Mashkoor
Alexander Raschke
Elvinia Riccobene
Patrizia Scandurra
Michael Stegmaier
Editors Michael Butler
Klaus-Dieter Schewe
Atif Mashkoor
Miklós Biró
Title Unified syntax for ASM
Booktitle Abstract State Machines, Alloy, B, TLA, VDM, and Z - Proc. ABZ 2016
Type in proceedings
Publisher Springer
Series Lecture Notes in Computer Science
Volume 9676
ISBN 978-3-319-33599-5
DOI 10.1007/978-3-319-33600-8_14
Month May
Year 2016
Pages 231-236
SCCH ID# 1615

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.