Abstract state machine


In computer science, an abstract state machine is a state machine operating on states that are arbitrary data structures.

Overview

The ASM Method is a practical and scientifically well-founded systems engineering method that bridges the gap between the two ends of system development:
  • the human understanding and formulation of real-world problems
  • the deployment of their algorithmic solutions by code-executing machines on changing platforms.
The method builds upon three basic concepts:
  • ASM: a precise form of pseudo-code, generalizing finite-state machines to operate over arbitrary data structures
  • ground model: a rigorous form of blueprints, serving as an authoritative reference model for the design
  • refinement: a most general scheme for stepwise instantiations of model abstractions to concrete system elements, providing controllable links between the more and more detailed descriptions at the successive stages of system development.
In the original conception of ASMs, a single agent executes a program in a sequence of steps, possibly interacting with its environment. This notion was extended to capture distributed computations, in which multiple agents execute their programs concurrently.
Since ASMs model algorithms at arbitrary levels of abstraction, they can provide high-level, low-level and mid-level views of a hardware or software design. ASM specifications often consist of a series of ASM models, starting with an abstract ground model and proceeding to greater levels of detail in successive refinements or coarsenings.
Due to the algorithmic and mathematical nature of these three concepts, ASM models and their properties of interest can be analyzed using any rigorous form of verification or validation.

History

The concept of ASMs is due to Yuri Gurevich, who first proposed it in the mid-1980s as a way of improving on Turing's thesis that every algorithm is simulated by an appropriate Turing machine. He formulated the ASM Thesis: every algorithm, no matter how abstract, is step-for-step emulated by an appropriate ASM. In 2000, Gurevich axiomatized the notion of sequential algorithms, and proved the ASM thesis for them. Roughly stated, the axioms are as follows:
The axiomatization and characterization of sequential algorithms have been extended to parallel and interactive algorithms.
In the 1990s, through a community effort, the ASM method was developed, using ASMs for the formal specification and analysis of computer hardware and software. Comprehensive ASM specifications of programming languages and design languages have been developed.
A detailed historical account can be found elsewhere.
A number of software tools for ASM execution and analysis are available.

Publications

Books

  • AsmBook: Egon Börger, Robert Stärk.
  • JBook: R.Stärk, J.Schmid, E.Börger.
  • Proceedings/Journal Issues
  • * 2008: Springer LNCS 5238
  • * 2008: J.UCS Special Issue with
  • * 2006: Springer LNCS 5115 ,
  • * 2005: Fundamenta Informatica Special Issue with
  • * 2004: Springer LNCS 3052
  • * 2003: Springer LNCS 2589
  • * 2003: TCS special Issue with
  • * 2002: Dagstuhl Seminar Report
  • * 2001: J.UCS 7.11 Special Issue with
  • * 2000: Springer LNCS 1912
  • Comparative case studies with ASM contributions
  • * ,
  • * ,
  • * ,
  • * ,
  • *

    Behavioral models for industrial standards

  • OMG for BPMN :
  • OASIS for BPEL:
  • ECMA for C#: "A high-level modular definition of the semantics of C♯"
  • ITU-T for SDL-2000: and
  • IEEE for VHDL93: E.Boerger, U.Glaesser, W.Mueller. Formal Definition of an Abstract VHDL'93 Simulator by EA-Machines. In: Carlos Delgado Kloos and Peter T.~Breuer, Formal Semantics for VHDL, pp. 107–139, Kluwer Academic Publishers, 1995
  • ISO for Prolog: "A mathematical definition of full Prolog"

    Tools

*
*
*