Abstract State Machines

In computer science, an abstract state machine (ASM) is a state machine operating on states that are arbitrary data structures (structure in the sense of mathematical logic, that is a nonempty set together with a number of functions (operations) and relations over the set).

The ASM Method is a practical and scientifically well-founded systems engineering method that 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).

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. (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.

...
Wikipedia