Unified syntax for ASM
|Titel||Unified syntax for ASM|
|Buchtitel||Abstract State Machines, Alloy, B, TLA, VDM, and Z - Proc. ABZ 2016|
|Serie||Lecture 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.