computer science Computer science is the study of computation, automation, and information. Computer science spans theoretical disciplines (such as algorithms, theory of computation, information theory, and automation) to Applied science, practical discipli ...

, an abstract state machine (ASM) is a

state machine A finite-state machine (FSM) or finite-state automaton (FSA, plural: ''automata''), finite automaton, or simply a state machine, is a mathematical model of computation. It is an abstract machine that can be in exactly one of a finite number o ...

operating on states that are arbitrary data structures (

structure A structure is an arrangement and organization of interrelated elements in a material object or system, or the object or system so organized. Material structures include man-made objects such as buildings and machines and natural objects such as ...

in the sense of

mathematical logic Mathematical logic is the study of logic, formal logic within mathematics. Major subareas include model theory, proof theory, set theory, and recursion theory. Research in mathematical logic commonly addresses the mathematical properties of for ...

, that is a nonempty

set Set, The Set, SET or SETS may refer to: Science, technology, and mathematics Mathematics *Set (mathematics), a collection of elements *Category of sets, the category whose objects and morphisms are sets and total functions, respectively Electro ...

together with a number of functions ( operations) and relations over the set).

Overview

The ASM Method is a practical and scientifically well-founded

systems engineering Systems engineering is an interdisciplinary field of engineering and engineering management that focuses on how to design, integrate, and manage complex systems over their enterprise life cycle, life cycles. At its core, systems engineering util ...

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 Agent may refer to: Espionage, investigation, and law *, spies or intelligence officers * Law of agency, laws involving a person authorized to act on behalf of another ** Agent of record, a person with a contractual agreement with an insuranc ...

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 Verify or verification may refer to: General * Verification and validation, in engineering or quality management systems, is the act of reviewing, inspecting or testing, in order to establish and document that a product, service or system meets ...

(by reasoning) or

validation Validation may refer to: * Data validation, in computer science, ensuring that data inserted into an application satisfies defined formats and other input criteria * Forecast verification, validating and verifying prognostic output from a numerica ...

(by experimentation, testing model executions).

History

The concept of ASMs is due to

Yuri Gurevich Yuri Gurevich, Professor Emeritus at the University of Michigan, is an American computer scientist and mathematician and the inventor of abstract state machines. Gurevich was born and educated in the Soviet Union. He taught mathematics there an ...

, who first proposed it in the mid-1980s as a way of improving on Turing's thesis that every

algorithm In mathematics and computer science, an algorithm () is a finite sequence of rigorous instructions, typically used to solve a class of specific Computational problem, problems or to perform a computation. Algorithms are used as specificat ...

simulated A simulation is the imitation of the operation of a real-world process or system over time. Simulations require the use of models; the model represents the key characteristics or behaviors of the selected system or process, whereas the s ...

by an appropriate

Turing machine A Turing machine is a mathematical model of computation describing an abstract machine that manipulates symbols on a strip of tape according to a table of rules. Despite the model's simplicity, it is capable of implementing any computer algori ...

. He formulated the ''ASM Thesis'': every algorithm, no matter how abstract, is step-for-step

emulated In computing, an emulator is Computer hardware, hardware or software that enables one computer system (called the ''host'') to behave like another computer system (called the ''guest''). An emulator typically enables the host system to run so ...

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 State may refer to: Arts, entertainment, and media Literature * ''State Magazine'', a monthly magazine published by the U.S. Department of State * ''The State'' (newspaper), a daily newspaper in Columbia, South Carolina, United States * ''Our S ...

involves only a bounded part of the state, and everything is

invariant Invariant and invariance may refer to: Computer science * Invariant (computer science), an expression whose value doesn't change during program execution ** Loop invariant, a property of a program loop that is true before (and after) each iteratio ...

under

isomorphisms In mathematics, an isomorphism is a structure-preserving mapping between two structures of the same type that can be reversed by an inverse mapping. Two mathematical structures are isomorphic if an isomorphism exists between them. The word i ...

of structures. (Structures can be viewed as

algebras In mathematics, an algebra over a field (often simply called an algebra) is a vector space equipped with a bilinear product. Thus, an algebra is an algebraic structure consisting of a set together with operations of multiplication and addition ...

, which explains the original name ''evolving algebras'' for ASMs.) The axiomatization and characterization of sequential algorithms have been extended to

parallel Parallel is a geometric term of location which may refer to: Computing * Parallel algorithm * Parallel computing * Parallel metaheuristic * Parallel (software), a UNIX utility for running programs in parallel * Parallel Sysplex, a cluster of ...

and interactive algorithms. In the 1990s, through a community effort, the ASM method was developed, using ASMs for the

formal specification In computer science, formal specifications are mathematically based techniques whose purpose are to help with the implementation of systems and software. They are used to describe a system, to analyze its behavior, and to aid in its design by verif ...

and analysis (

verification and validation Verification and validation (also abbreviated as V&V) are independent procedures that are used together for checking that a product, service, or system meets requirements and specifications and that it fulfills its intended purpose. These are ...

) of

computer hardware Computer hardware includes the physical parts of a computer, such as the computer case, case, central processing unit (CPU), Random-access memory, random access memory (RAM), Computer monitor, monitor, Computer mouse, mouse, Computer keyboard, ...

and

software Software is a set of computer programs and associated documentation and data. This is in contrast to hardware, from which the system is built and which actually performs the work. At the lowest programming level, executable code consists ...

. Comprehensive ASM specifications of

programming languages A programming language is a system of notation for writing computer programs. Most programming languages are text-based formal languages, but they may also be graphical. They are a kind of computer language. The description of a programming ...

(including

Prolog Prolog is a logic programming language associated with artificial intelligence and computational linguistics. Prolog has its roots in first-order logic, a formal logic, and unlike many other programming languages, Prolog is intended primarily ...

, C, and

Java Java (; id, Jawa, ; jv, ꦗꦮ; su, ) is one of the Greater Sunda Islands in Indonesia. It is bordered by the Indian Ocean to the south and the Java Sea to the north. With a population of 151.6 million people, Java is the world's List ...

) and

design language A design language or design vocabulary is an overarching scheme or style that guides the design of a complement of products or architectural settings, creating a coherent design system for styling. Objectives Designers wishing to give their sui ...

s (

UML The Unified Modeling Language (UML) is a general-purpose, developmental modeling language in the field of software engineering that is intended to provide a standard way to visualize the design of a system. The creation of UML was originally m ...

and SDL) have been developed. A detailed historical account can be found elsewhere. A number of software tools for ASM execution and analysis are available.

Publications

Books

* AsmBook:

Egon Börger Egon Börger (born 13 May 1946) is a German-born computer scientist based in Italy. Life and work Börger was born in Bad Laer, Westphalia, Lower Saxony, Germany. Between 1965 and 1971 he studied at the Sorbonne, Paris (France), Université Cath ...

, Robert Stärk
Abstract State Machines: A Method for High-Level System Design and Analysis
* JBook: R.Stärk, J.Schmid, E.Börger
Java and the Java Virtual Machine: Definition, Verification, Validation
* Proceedings/Journal Issues (since 2000) ** 2008: Springer LNCS 523
Abstract State Machines, B and Z
** 2007: J.UCS Special Issue wit
Selected Papers from ASM'07
** 2006: Springer LNCS 511
Rigorous Methods for Software Construction and AnalysisASM and B Dagstuhl Seminar
** 2005: Fundamenta Informatica Special Issue wit

** 2004: Springer LNCS 305
Abstract State Machines 2004
** 2003: Springer LNCS 258
Abstract State Machines 2003: Advances in Theory and Practice
** 2003: TCS special Issue wit
Selected Papers from ASM'03
** 2002: Dagstuhl Seminar Repor
Theory and Applications of Abstract State Machines
** 2001: J.UCS 7.11 Special Issue wit
Selected Papers from ASM'01
** 2000: Springer LNCS 191
Abstract State Machines: Theory and Applications
* Comparative case studies with ASM contributions *
Springer LNCS 1165
*
Production Cell: Software Development Case StudyASM model
*
ASM model
*
Light Control: Requirements Engineering Case StudyDagstuhl Seminar
*
Invoicing: Requirements Capture Case Study

Behavioral models for industrial standards

* OMG for BPMN (version 2006)
Springer LNCS 5316
* OASIS for BPEL
IJBPMI 1.4 (2006)
* ECMA for C#: "A high-level modular definition of the semantics of C♯" * ITU-T for SDL-2000
formal semantics of SDL-2000
an
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"

Tools

(in historical order since 2000)
ASMETA, the Abstract State Machine Metamodel and its tool set
on

SourceForge SourceForge is a web service that offers software consumers a centralized online location to control and manage open-source software projects and research business software. It provides source code repository hosting, bug tracking, mirrorin ...

AsmL
* CoreASM, available a
CoreASM, an extensible ASM execution engine
on

Archive.org The Internet Archive is an American digital library with the stated mission of "universal access to all knowledge". It provides free public access to collections of digitized materials, including websites, software applications/games, music, ...

The XASM open source project
on

Bibliography

* Y. Gurevich, ''Evolving Algebras 1993: Lipari Guide'', E. Börger (ed.), ''Specification and Validation Methods'',

Oxford University Press Oxford University Press (OUP) is the university press of the University of Oxford. It is the largest university press in the world, and its printing history dates back to the 1480s. Having been officially granted the legal right to print books ...

, 1995, 9-36. () * Y. Gurevich, ''Sequential Abstract State Machines capture Sequential Algorithms''
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 Springer Science+Business Media, commonly known as Springer, is a German multinational publishing company of books, e-books and peer-reviewed journals in science, humanities, technical and medical (STM) publishing. Originally founded in 1842 in ...

, 2001. () * E. Börger and R. Stärk, ''Abstract State Machines: A Method for High-Level System Design and Analysis'',

, 2003. () * E. Börger and A. Raschke, ''Modeling Companion for Software Practitioners'',

, 2018. (, )

References

External links

Abstract State MachinesAsmCenterThe TASM toolset: specification, simulation, and formal verification of real-time systems
{{DEFAULTSORT:Abstract State Machines Models of computation Formal methods