Introduction to Abstract State Machines
The Abstract State Machine (ASM) Project (formerly known as
the Evolving Algebras Project) was started by Yuri Gurevich as an
attempt to bridge the gap between formal models of computation and
practical specification methods.
The ASM thesis is that any algorithm can be modeled at
its natural abstraction level by an appropriate ASM.
Based upon this thesis, members of the ASM community have
sought to develop a methodology based upon mathematics which would
allow algorithms to be modeled naturally; that is, described at their
natural abstraction levels. The result is a simple methodology for
describing simple abstract machines which correspond to algorithms.
Plentiful examples exist in the literature of ASMs applied to
different types of algorithms.
The ASM methodology has the following desirable
characteristics.
- Precision.
- One uses a specification methodology to describe a system by
means of a particular syntax and associated semantics. If the
semantics of the specification methodology is unclear, descriptions
using the methodology may be no clearer than the original systems
being described. ASMs use classical mathematical structures to
describe states of a computation; structures are well-understood,
precise models. This distinguishes ASMs from informal
methodologies.
- Faithfulness.
- Given a specification, how does one know
that the specification accurately describes the corresponding real
system? Since there is no method in principle to translate from the
concrete world into an abstract specification, one needs to be able to
see the correspondence between specification and reality directly, by
inspection. ASMs allow for the use of the terms and concepts of
the problem domain immediately, with a minimum of notational coding.
Many popular specification methods require a fair amount of notational
coding which makes this task more difficult.
- Understandability.
- How easy is it to read and write
specifications using a particular methodology? If the system is
difficult to read and write, few people will use it. ASM
programs use an extremely simple syntax, which can be read even by
novices as a form of pseudo-code. Other specification methods,
notably denotational semantics, use complicated syntax whose semantics
are more difficult to read and write.
- Executability.
- Another way to determine the correctness of
a specification is to execute the specification directly. A
specification methodology which is executable allows one to test
for errors in the specification. Additionally, testing can help
one to verify the correctness of a system by experimenting with
various safety or liveness properties. Methods
such as VDM, Z, or process algebras are not directly executable.
- Scalability.
- It is often useful to be able to describe a
system at several different layers of abstraction. With multiple
layers, one can examine particular features of a system while easily
ignoring others. Proving properties about systems also can be made
easier, as the highest abstraction level is often easily proved
correct and each lower abstraction level need only be proven correct
with respect to the previous level. Some specification methodologies,
e.g. Knuth's MIX language, provide only a single level of
abstraction.
- Generality.
- We seek a methodology which is useful
in a wide variety of domains: sequential, parallel, and distributed
systems; abstract-time and real-time systems; finite-state and
infinite-state domains. Many methodologies (e.g. finite
model checking, timed input-output automata, various temporal logics)
have shown their usefulness in particular domains; ASMs
have been shown to be useful in all of these domains.
[an error occurred while processing this directive]
