Efficient simulation of ASM runs

04.02.2000

Abstract

Gurevich’s Abstract State Machines (ASM’s) constitutes an powerful and elegant abstract specification method, which is able to specify the operational semantics of any algorithm at an arbitrary abstraction level. However, in order to demonstrate the full expressive power of the ASM approach, tools that combines functionality for prototyping, experimentation, formal analysis and reasoning with ASM’s are badly needed.

A variety of tools, mostly interpreter based exists, however, they suffers from a common set of problems. The older tools have proven inefficient for extensive use. In addition, they are not compatible in terms of architecture and language dialects.

The aim of this thesis has been to improve state of current ASM tool suite, by defining support for efficient ASM prototyping, experimentation and simulation in a homogeneous environment.

Our approach has been to solve the common problems by utilizing and taking advantage of existing tools. By extending the ASM workbench with back-end functionality that composes a compiler and simulation environment (ASMcse), we have achieved the desired properties.

We have implemented the ASMcse, as an ASM to Java Byte Code compiler that generates executable ASM models for the Java platform. In addition we have implemented an ASMcse runtime system, that provides the executing ASM’s with sufficient runtime support as well as to provide an environment that may support validation, experimentation and reasoning with the ASM runs. Several test cases has been conducted in order to measure performance of the simulation and validate the correctness of the ASM implementations.

In summary, it seems that our approach for ASM tool support is feasible. The results give strong indications on the applicability of the ASMcse and we believes that the ASMcse will make an important contribution to the ASM community in terms of tool support.