Abstract State Machines




ASM Studies

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.

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.

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.

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.

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.

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.

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.