Founding member of the Abstract State Machines Research Center
The notion of ABSTRACT STATE MACHINES (ASM) captures in a mathematical rigorous yet transparent form the main operational
intuitions of computing, of programming in the small, of programming in the large,
of programming in the world, and of architectures of computing systems. The notation is familiar from programming
and development practice and from mathematical standards. This allows the practitioner (e.g. the programmer, the
developer, the conceptualiser, the modeler, the software architect)
and the stakeholder to work with ASM without any further explanation, viewing
them as 'pseudocode over machines' which comes with a well defined semantics supporting the intuitive understanding.
At the same time, the ASM specification can be consistently refined by any concrete refinement scheme and refinement
strategy thus ranging from programming in the large or programming in the world to programming in the small without any impedance
mismatch.
The success story of the ASM method is caused by a number of its advantages
for high-level design, analysis, validation and verification of computing systems:
-
The specification method improves industrial practice by proper orchestration of all
phases of software development, by supporting a high-level modeling at any level of
abstraction, and by providing a scientific and formal foundation for systems engineering.
All other specification frameworks known so far only provide a loose coupling of notions,
techniques, and notations used at various levels of abstraction. By using the ASM
method, a system engineer can derive a general application-oriented understanding , may
base the specification on a uniform algorithmic view, and refine the model until the
implementation level is achieved. The three ingredients to achieve this generality are the
notion of the ASM itself, the ground model techniques, and the proper treatment of
refinement.
- Using this specification method the
system architect, the application engineer, the
developer and the programmer obtain a common view on the system they are building,
changing, maintaining, or documenting. The system construction process is accompanied
by common understanding, by common theoretical foundations, and by the ability to prove
validity of properties such as satisfaction of quality criteria. By doing so the construction
process support quality from the very beginning of the process until the implementation of
the system. At the same time, the ASM method supports software development in
changing environments.
- The method supports abstraction and
extension of models, stepwise detailing of models,
and control through execution of the model for their experimental validation.
- Abstract state machines entirely
capture all four principles of computer science:
structure, evolution, collaboration, and abstraction. This coverage of all principles has not
been achieved in any other approach of any other discipline of computer science. Due to
this coverage, the ASM method underpins computer science as a whole.
-
Abstract state machines (ASM) sharpen the Church-Turing thesis by the consideration
of
bounded resources for computing devices. They view computations as an evolution of a state.
Meanwhile, it has shown that all known models of computation can be expressed through
specific abstract state machines. These models can given in an representation independent
way. That is one advantage of transferring these models to ASM. The main advantage is,
however, to provide a unifying theory to all of these models. At the same time ASM can be
refined to other ASM's. Stepwise refinement supports separation of concern during software
development and will support component-based construction of systems thus providing a
foundation of new computational paradigms such as industrial programming, programming-in-
the-large, and programming-in-the-world.
- ASM method has clearly based on a
number of postulates restricting evolution of systems.
For instance, sequential computation is based on the postulate of sequential time, the
postulate of abstract state, and the postulate of bounded exploration of the state space.
These postulates may be extended to postulates for parallel and concurrent computation,
e.g., by extending the last postulate to the postulate of finite exploration.
The generality of the model, the deep foundation, the test of the concept by providing
rigorous
semantics to a large variety of real-life software and hardware products, and - at the same
time - the development of proper tools supporting the entire specification process is the work
of a community headed by two congenial friends - Yuri Gurevich and Egon Börger -
competing at the same time by their results.
A proof of concept has already been given by investigation of practically relevant case studies
and system development problems for Siemens, Microsoft etc.
The ASM community attracted a number of researcher for a program that will entirely
change computer science: improve development and implementation of languages by
providing rigorous semantics, by acquiring tools to prove and to maintain properties of the
developed products, and thus supporting quality at each level of software specification.
