The Abstract State Machines Method

Starting from Gurevich’s New Thesis that every computational device can be simulated by an appropriate dynamic structure , the article describes the development of the Abstract State Machines (ASM) method in theory and practice. ASMs, originally called evolving algebras , provide a computation model on structures capturing arbitrary algorithms—understood very generally to comprise all computation systems—on arbitrary levels of abstraction. The theoretical investigations have resulted in a variety of behavioural theories showing that a particular class of algorithms (or algorithmic systems) is captured by some well-defined class of ASMs. Most importantly, the theories capture the classes of sequential, recursive, synchronous parallel, concurrent and reflective algorithms. Each such class gives rise to an associated ASM logic that enables reasoning over properties of states and state transitions. These logics have been proven to be complete, and recent research resulted in complete temporal extensions. Furthermore, specific subclasses of ASMs have been discovered that capture algorithms solving problems in certain complexity classes. The application-oriented investigations have led to a large variety of rigorous specifications including correct and complete refinements and the verification of desired system properties. This includes among others proofs of compiler correctness for various languages, specification and verification of web browsers, specifications and verification of ambient systems, specifications and verification of hybrid systems, and specifications of reflective programming languages. The seamless coupling of deep theory and rigorous scientific practice enables the targeted analysis of rigorous specifications and the systematic reification on target platforms.