This paper is chapter 16 in the book Languages for system specification [1]. The paper is a discussion of the concepts and applications of abstract state machines (ASMs), for use in software design and verification. ASMs may be viewed as a generalization of finite state machines, in which states are abstractions of states of the target software, abstract data structures are used to associate semantics for the states, transitions on the ASM are abstractions of operations for the target software, and concurrent behaviors are defined. ASMs may be contrasted with statechart models in unified modeling language (UML): statecharts are a visual abstraction, but with incomplete semantic definition, whereas ASMs have a defined (but more complex) semantic definition.

The stated goal of the chapter is to “show how abstract state machines (ASM) can be used” to relate “the finite state machine (FSM) view of model-checkable components and the architectural system view.” In fact, the paper consists of survey and summary statements about the many references, together with snippet examples from several of the references.

For readers familiar with the references, the paper should provide perspective and integration of the concepts; for readers not familiar with the references, the paper should provide a good guide to readings. For example, it might be an appropriate guide for directed readings for graduate students. For a full definition of ASMs, and for examples and case studies, the author refers to his book [2].