Abstract State Machines
Encyclopedia
In computer science
, an abstract state machine (ASM) is a state machine operating on states
which are arbitrary data structures (structure
in the sense of mathematical logic
, that is a nonempty set together with a number of functions
(operations
over the set) and relations
).
The ASM Method is a practical and scientifically well-founded systems engineering
method which bridges the gap between the two ends of system development:
The method builds upon three basic concepts:
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 (by reasoning) or validation (by experimentation, testing model executions).
, 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. (Structures can be viewed as algebras
, which explains the original name evolving algebras for ASMs.) The axiomatization and characterization of sequential algorithms have been extended to parallel
and interactive algorithms.
In the 1990s, by a community effort, the ASM method has been developed, using ASMs for the formal specification
and analysis (verification and validation) of computer hardware
and software. Comprehensive ASM specifications of programming languages (including Prolog
, C
, and Java
) and design language
s (UML
and SDL
) have been developed.
A detailed historical account can be found in the AsmBook (Chapter 9) or in
this article.
A number of software tools for ASM execution and analysis are available.
Computer science
Computer science or computing science is the study of the theoretical foundations of information and computation and of practical techniques for their implementation and application in computer systems...
, an abstract state machine (ASM) is a state machine operating on states
State (computer science)
In computer science and automata theory, a state is a unique configuration of information in a program or machine. It is a concept that occasionally extends into some forms of systems programming such as lexers and parsers....
which are arbitrary data structures (structure
Mathematical structure
In mathematics, a structure on a set, or more generally a type, consists of additional mathematical objects that in some manner attach to the set, making it easier to visualize or work with, or endowing the collection with meaning or significance....
in the sense of mathematical logic
Mathematical logic
Mathematical logic is a subfield of mathematics with close connections to foundations of mathematics, theoretical computer science and philosophical logic. The field includes both the mathematical study of logic and the applications of formal logic to other areas of mathematics...
, that is a nonempty set together with a number of functions
Function (mathematics)
In mathematics, a function associates one quantity, the argument of the function, also known as the input, with another quantity, the value of the function, also known as the output. A function assigns exactly one output to each input. The argument and the value may be real numbers, but they can...
(operations
Operation (mathematics)
The general operation as explained on this page should not be confused with the more specific operators on vector spaces. For a notion in elementary mathematics, see arithmetic operation....
over the set) and relations
Relation (mathematics)
In set theory and logic, a relation is a property that assigns truth values to k-tuples of individuals. Typically, the property describes a possible connection between the components of a k-tuple...
).
The ASM Method is a practical and scientifically well-founded systems engineering
Systems engineering
Systems engineering is an interdisciplinary field of engineering that focuses on how complex engineering projects should be designed and managed over the life cycle of the project. Issues such as logistics, the coordination of different teams, and automatic control of machinery become more...
method which bridges the gap between the two ends of system development:
- the human understanding and formulation of real-world problems (requirements captureRequirements analysisRequirements analysis in systems engineering and software engineering, encompasses those tasks that go into determining the needs or conditions to meet for a new or altered product, taking account of the possibly conflicting requirements of the various stakeholders, such as beneficiaries or users...
by accurate high-level modeling at the level of abstraction determined by the given application domain) - the deployment of their algorithmic solutions by code-executing machines on changing platforms (definition of design decisions, system and implementation details).
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 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
Software agent
In computer science, a software agent is a piece of software that acts for a user or other program in a relationship of agency, which derives from the Latin agere : an agreement to act on one's behalf...
executes a program in a sequence of steps, possibly interacting with its environment. This notion was extended to capture distributed computations
Distributed computing
Distributed computing is a field of computer science that studies distributed systems. A distributed system consists of multiple autonomous computers that communicate through a computer network. The computers interact with each other in order to achieve a common goal...
, 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 (by reasoning) or validation (by experimentation, testing model executions).
History
The concept of ASMs is due to Yuri GurevichYuri Gurevich
Yuri Gurevich is an American computer scientist and mathematician and the inventor of abstract state machines. He is currently Principal Researcher at Microsoft Research, where he founded the Foundations of Software Engineering group,...
, who first proposed it in the mid-1980s as a way of improving on Turing's thesis
Church–Turing thesis
In computability theory, the Church–Turing thesis is a combined hypothesis about the nature of functions whose values are effectively calculable; in more modern terms, algorithmically computable...
that every algorithm
Algorithm
In mathematics and computer science, an algorithm is an effective method expressed as a finite list of well-defined instructions for calculating a function. Algorithms are used for calculation, data processing, and automated reasoning...
is simulated by an appropriate Turing machine
Turing machine
A Turing machine is a theoretical device that manipulates symbols on a strip of tape according to a table of rules. Despite its simplicity, a Turing machine can be adapted to simulate the logic of any computer algorithm, and is particularly useful in explaining the functions of a CPU inside a...
. He formulated the ASM Thesis: every algorithm, no matter how abstract
Abstraction
Abstraction is a process by which higher concepts are derived from the usage and classification of literal concepts, first principles, or other methods....
, is step-for-step emulated by an appropriate ASM. In 2000, Gurevich axiomatized
Axiomatic system
In mathematics, an axiomatic system is any set of axioms from which some or all axioms can be used in conjunction to logically derive theorems. A mathematical theory consists of an axiomatic system and all its derived theorems...
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
Invariant (mathematics)
In mathematics, an invariant is a property of a class of mathematical objects that remains unchanged when transformations of a certain type are applied to the objects. The particular class of objects and type of transformations are usually indicated by the context in which the term is used...
under isomorphisms of structures. (Structures can be viewed as algebras
Universal algebra
Universal algebra is the field of mathematics that studies algebraic structures themselves, not examples of algebraic structures....
, which explains the original name evolving algebras for ASMs.) The axiomatization and characterization of sequential algorithms have been extended to parallel
Parallel computing
Parallel computing is a form of computation in which many calculations are carried out simultaneously, operating on the principle that large problems can often be divided into smaller ones, which are then solved concurrently . There are several different forms of parallel computing: bit-level,...
and interactive algorithms.
In the 1990s, by a community effort, the ASM method has been developed, using ASMs for the formal specification
Formal specification
In computer science, a formal specification is a mathematical description of software or hardware that may be used to develop an implementation. It describes what the system should do, not how the system should do it...
and analysis (verification and validation) of computer hardware
Computer hardware
Personal computer hardware are component devices which are typically installed into or peripheral to a computer case to create a personal computer upon which system software is installed including a firmware interface such as a BIOS and an operating system which supports application software that...
and software. Comprehensive ASM specifications of programming languages (including Prolog
Prolog
Prolog is a general purpose logic programming language associated with artificial intelligence and computational linguistics.Prolog has its roots in first-order logic, a formal logic, and unlike many other programming languages, Prolog is declarative: the program logic is expressed in terms of...
, C
C (programming language)
C is a general-purpose computer programming language developed between 1969 and 1973 by Dennis Ritchie at the Bell Telephone Laboratories for use with the Unix operating system....
, and Java
Java (programming language)
Java is a programming language originally developed by James Gosling at Sun Microsystems and released in 1995 as a core component of Sun Microsystems' Java platform. The language derives much of its syntax from C and C++ but has a simpler object model and fewer low-level facilities...
) and design language
Design language
A design language or design vocabulary is an overarching scheme or style that guides the design of a complement of products or architectural settings...
s (UML
Unified Modeling Language
Unified Modeling Language is a standardized general-purpose modeling language in the field of object-oriented software engineering. The standard is managed, and was created, by the Object Management Group...
and SDL
Specification and Description Language
Specification and Description Language is a specification language targeted at the unambiguous specification and description of the behaviour of reactive and distributed systems.- Overview :It is defined by the ITU-T...
) have been developed.
A detailed historical account can be found in the AsmBook (Chapter 9) or in
this article.
A number of software tools for ASM execution and analysis are available.
Books
- AsmBook: E.Börger, R.Stärk. Abstract State Machines: A Method for High-Level System Design and Analysis
- JBook: R.Stärk, J.Schmid, E.Börger. Java and the Java Virtual Machine: Definition, Verification, Validation
- Proceedings/Journal Issues (since 2000)
- 2008: Springer LNCS 5238 Abstract State Machines, B and Z
- 2007: J.UCS Special Issue with and http://osys.grm.hia.no/asm07/proceedings Selected Papers from ASM'07
- 2006: Springer LNCS 5115 Rigorous Methods for Software Construction and Analysis, ASM and B Dagstuhl Seminar
- 2005: Fundamenta Informatica Special Issue with Selected Papers from ASM'05 (electronic proceedings)
- 2004: Springer LNCS 3052 Abstract State Machines 2004
- 2003: Springer LNCS 2589 Abstract State Machines 2003: Advances in Theory and Practice
- 2003: TCS special Issue with Selected Papers from ASM'03
- 2002: Dagstuhl Seminar Report Theory and Applications of Abstract State Machines
- 2001: J.UCS 7.11 Special Issue with Selected Papers from ASM'01
- 2000: Springer LNCS 1912 Abstract State Machines: Theory and Applications
- Comparative case studies with ASM contributions
- Steam-Boiler Control: Specification Case Study, Springer LNCS 1165
- Production Cell: Software Development Case Study, ASM model
- Railcrossing: Formal Methods for Real-Time Computing, ASM model
- Light Control: Requirements Engineering Case Study, Dagstuhl Seminar
- Invoicing: Requirements Capture Case Study
Behavioral Models for Industrial Standards
- OMG for BPMN (version 2006): Springer LNCS 5316
- OASIS for BPEL: IJBPMI 1.4 (2006)
- ECMA for C#: TCS 336 (2006)
- de facto standard for Java/JVM (version 2000): JBook
- ITU-T for SDL-2000: formal semantics of SDL-2000 and Formal Definition of SDL-2000 - Compiling and Running SDL Specifications as ASM Models
- 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 (Eds.), Formal Semantics for VHDL, pp. 107–139, Kluwer Academic Publishers, 1995
- ISO for Prolog: A Mathematical Definition of Full Prolog
Tools
(in historical order since 2000)- ASMETA, the Abstract State Machine Metamodel and its tool set
- AsmL
- CoreASMCoreASMCoreASM is an open source project that focuses on the design of a lean executable ASM language, in combination with a supporting tool environment for high-level design, experimental validation and formal verification of abstract system models.Abstract state machines are known for their...
, available at at CoreASM, an extensible ASM execution engine - AsmGofer
- The TASM toolset: specification, simulation, and formal verification of real-time systems
- The XASM open source project