Abstract state machines

In computer science, an abstract state machine (ASM) is a state machine in which the number of states need not be finite and in which the states are not mere points in the state space. More precisely, an ASM state is a structure in the sense of mathematical logic, that is, a nonempty set together with a number of functions (operations over the set) and relations. (Structures can be viewed as algebras, which explains the original name "evolving algebras" for ASMs.) 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.

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: states are structures, the state transition involves only a bounded part of the state, and everything is invariant under isomorphisms of structures. The axiomatization and characterization of sequential algorithms have been extended to parallel and interactive algorithms.

ASMs have been used for the formal specification of computer hardware and software. Egon Börger has long been involved in applying ASMs to hardware and software design and verification, and he is a leading proponent of their use in software engineering. 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. Comprehensive ASM specifications of programming languages (including Prolog, C, and Java) and design languages (UML and SDL) have been developed. A number of software tools for ASM execution and analysis are available.

References

* Y. Gurevich, "Evolving Algebras 1993: Lipari Guide", E. Börger (ed.), "Specification and Validation Methods", Oxford University Press, 1995, 9-36. (ISBN 0-198-53854-5)
* E. Börger and R. Stärk, "Abstract State Machines: A Method for High-Level System Design and Analysis", Springer-Verlag, 2003. (ISBN 3-540-00702-4)
* R. Stärk, J. Schmid and E. Börger, "Java and the Java Virtual Machine: Definition, Verification, Validation", Springer-Verlag, 2001. (ISBN 3-540-42088-6)
* Y. Gurevich, "Sequential Abstract State Machines capture Sequential Algorithms", [http://tocl.acm.org ACM Transactions on Computational Logic] 1(1) (July 2000), 77-111.

External links

* [http://www.eecs.umich.edu/gasm/ Abstract State Machines]
* [http://asmeta.sourceforge.net ASMETA, the Abstract State Machine Metamodel and its tool set]
* [http://www.coreasm.org CoreASM, an extensible ASM execution engine]
* [http://esl.mit.edu/tasm/ TASM, The Timed Abstract State Machine Language and Toolset]
* [http://www.xasm.org The XASM open source project]