Abstract state machine

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 human understanding and formulation of real-world problems (requirements capture by accurate high-level modeling at the level of abstraction determined by the given application domain)
• the deployment of their algorithmic solutions by code-executing machines on changing platforms (definition of design decisions, system and implementation details).

The method builds upon three basic concepts:

• ASM: a precise form of pseudo-code, generalizing finite-state machines to operate over arbitrary data structures
• ground model: a rigorous form of blueprints, serving as an authoritative reference model for the design
• refinement: a most general scheme for stepwise instantiations of model abstractions to concrete system elements, providing controllable links between the more and more detailed descriptions at the successive stages of system development.

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.

In the 1990s, through a community effort,{{cite book| first=Jonathan P. | last=Bowen | author-link=Jonathan Bowen | chapter=Communities and Ancestors Associated with Egon Börger and ASM | title=Logic, Computation and Rigorous Methods: Essays Dedicated to Egon Börger on the Occasion of His 75th Birthday | series=Lecture Notes in Computer Science | editor1-first=Alexander | editor1-last=Raschke | editor2-first=Elvinia | editor2-last=Riccobene | editor3-first=Klaus-Dieter | editor3-last=Schewe | publisher=Springer International Publishing | isbn=978-3-030-76019-9 | doi=10.1007/978-3-030-76020-5_6 | date=2021 | volume=12750 | pages=96–120 | s2cid=235414337 }} the ASM method was developed, using ASMs for the formal specification and analysis (verification and validation) of computer hardware and software. Comprehensive ASM specifications of programming languages (including Prolog, C, and Java) and design languages (UML and SDL) have been developed.

A detailed historical account can be found elsewhere.{{cite web| url=http://www.di.unipi.it/~boerger/AsmBook/ | title=AsmBook Home Page | date=November 2005 | accessdate=8 June 2021 | publisher=University of Pisa | location=Italy }} (Chapter 9){{cite journal| url=http://www.jucs.org/jucs_8_1/the_origins_and_the | first=Egon | last=Börger | author-link=Egon Börger | title=The Origins and the Development of the ASM Method for High Level System Design and Analysis | journal=Journal of Universal Computer Science | volume=8 | number=1 | doi=10.3217/jucs-008-01-0002 | date=2002 }}

A number of software tools for ASM execution and analysis are available.

• AsmBook: Egon Börger, Robert Stärk. [http://www.di.unipi.it/~boerger/AsmBook/ Abstract State Machines: A Method for High-Level System Design and Analysis]
• JBook: R.Stärk, J.Schmid, E.Börger. [http://www.di.unipi.it/~boerger/jbook/ Java and the Java Virtual Machine: Definition, Verification, Validation]
• Proceedings/Journal Issues (since 2000)
• 2008: Springer LNCS 5238 [http://www.springeronline.com/978-3-540-87602-1 Abstract State Machines, B and Z]
• 2007: J.UCS Special Issue with [http://www.jucs.org/doi?doi=10.3217/jucs-014-12 Selected Papers from ASM'07]
• 2006: Springer LNCS 5115 [https://dblp.org/db/conf/birthday/borger2009 Rigorous Methods for Software Construction and Analysis], [https://www.dagstuhl.de/06191 ASM and B Dagstuhl Seminar]
• 2005: Fundamenta Informatica Special Issue with [https://web.archive.org/web/20090913202642/http://fi.mimuw.edu.pl/abs77.html Selected Papers from ASM'05] ([https://web.archive.org/web/20061002142048/http://www.univ-paris12.fr/lacl/dima/asm05/asm05-contents.html electronic proceedings])
• 2004: Springer LNCS 3052 [https://dblp.org/db/conf/asm/asm2004 Abstract State Machines 2004]
• 2003: Springer LNCS 2589 [https://dblp.org/db/conf/asm/asm2003 Abstract State Machines 2003: Advances in Theory and Practice]
• 2003: TCS special Issue with [http://www.sciencedirect.com/science/issue/5674-2005-996639997-594598 Selected Papers from ASM'03]
• 2002: Dagstuhl Seminar Report [https://www.dagstuhl.de/02101 Theory and Applications of Abstract State Machines]
• 2001: J.UCS 7.11 Special Issue with [http://www.jucs.org/jucs_7_11 Selected Papers from ASM'01]
• 2000: Springer LNCS 1912 [https://dblp.org/db/conf/asm/asm2000 Abstract State Machines: Theory and Applications]
• Comparative case studies with ASM contributions
• [http://www.informatik.uni-kiel.de/~procos/dag9523/dag9523.html Steam-Boiler Control: Specification Case Study], [https://dblp.org/db/conf/dagstuhl/fm1995 Springer LNCS 1165]
• [https://dblp.org/db/conf/korso/korso1995fd Production Cell: Software Development Case Study], [http://www.jucs.org/jucs_3_5/integrating_asm ASM model]
• [https://web.archive.org/web/20090719170052/http://chacs.nrl.navy.mil/books/realtime/overview.html Railcrossing: Formal Methods for Real-Time Computing], [https://dblp.org/db/conf/csl/csl95 ASM model]
• [http://www.jucs.org/jucs_6_7 Light Control: Requirements Engineering Case Study], [https://www.dagstuhl.de/99241 Dagstuhl Seminar]
• [http://www.iste.co.uk/index.php?f=a&ACTION=View&id=100 Invoicing: Requirements Capture Case Study]

• OMG for BPMN (version 2006): [https://dblp.org/db/conf/lipari/lipari2007 Springer LNCS 5316]
• OASIS for BPEL: [http://www.inderscience.com/search/index.php?action=record&rec_id=12626&prevQuery=&ps=10&m=or IJBPMI 1.4 (2006)]
• ECMA for C#: "A high-level modular definition of the semantics of C♯" {{doi|10.1016/j.tcs.2004.11.008}}
• ITU-T for SDL-2000: [https://web.archive.org/web/20090913202636/http://www.sciencedirect.com/science?_ob=ArticleURL&_udi=B6VRG-48FKC55-2&_user=10&_rdoc=1&_fmt=&_orig=search&_sort=d&view=c&_acct=C000050221&_version=1&_urlVersion=0&_userid=10&md5=9da4c19ef309568c1598d3f6c48db4b6The formal semantics of SDL-2000] and [http://www.jucs.org/jucs_7_11/formal_definition_of_sdl Formal Definition of SDL-2000 - Compiling and Running SDL Specifications as ASM Models]
• IEEE for VHDL93: E.Boerger, U.Glaesser, W.Mueller. Formal Definition of an Abstract VHDL'93 Simulator by EA-Machines. In: Carlos Delgado Kloos and Peter T.~Breuer (Eds.), Formal Semantics for VHDL, pp. 107–139, Kluwer Academic Publishers, 1995
• ISO for Prolog: "A mathematical definition of full Prolog" {{doi|10.1016/0167-6423(95)00006-E}}

(in historical order since 2000)

• [https://github.com/constructum/the-asm-workbench The ASM Workbench]
• [https://github.com/asmeta/asmeta ASMETA, the Abstract State Machine Metamodel and its tool set]
• [http://www.codeplex.com/AsmL/ AsmL]
• CoreASM, available at [https://github.com/CoreASM CoreASM, an extensible ASM execution engine]
• [https://web.archive.org/web/20090914111707/http://www.tydo.de/doktorarbeit.html AsmGofer] on Archive.org
• [http://xasm.sourceforge.net/XasmAnl00/XasmAnl00.html The XASM open source project] on SourceForge

• Y. Gurevich, Evolving Algebras 1993: Lipari Guide, E. Börger (ed.), Specification and Validation Methods, Oxford University Press, 1995, 9-36. ({{ISBN|0-19-853854-5}})
• Y. Gurevich, Sequential Abstract State Machines capture Sequential Algorithms, [http://tocl.acm.org ACM Transactions on Computational Logic] 1(1) (July 2000), 77–111.
• R. Stärk, J. Schmid and E. Börger, Java and the Java Virtual Machine: Definition, Verification, Validation, Springer-Verlag, 2001. ({{ISBN|3-540-42088-6}})
• E. Börger and R. Stärk, Abstract State Machines: A Method for High-Level System Design and Analysis, Springer-Verlag, 2003. ({{ISBN|3-540-00702-4}})
• E. Börger and A. Raschke, Modeling Companion for Software Practitioners, Springer-Verlag, 2018.{{cite journal| title=Egon Börger and Alexander Raschke: Modeling companion for software practitioners | last=Bowen | first=Jonathan P. | author-link=Jonathan Bowen | journal=Formal Aspects of Computing | volume=30 | number=6 | date=November 2018 | pages=761–762 | doi=10.1007/s00165-018-0472-4 | s2cid=53086556 }} ({{ISBN|978-3-662-56639-8}}, {{doi|10.1007/978-3-662-56641-1}})

{{reflist}}

• [http://www.eecs.umich.edu/gasm/ Abstract State Machines]
• [http://www.asmcenter.org/ AsmCenter] {{Webarchive|url=https://web.archive.org/web/20190913201414/http://asmcenter.org/ |date=2019-09-13 }}
• [http://portal.acm.org/citation.cfm?id=1770371 The TASM toolset: specification, simulation, and formal verification of real-time systems]

{{DEFAULTSORT:Abstract State Machines}}

Category:Models of computation

Category:Formal methods