BCS-FACS Evening Seminar Series

The Abstract State Machines Method for High-Level System Design and Analysis

Professor Egon Borger University of Pisa, Italy

21 March 2007

We try to answer the often asked question what is special about the Abstract 
State Machines (ASM) Method as a practical and scientifically well-founded 
systems engineering method, a method that enables to construct computer-based 
systems in a certifiably reliable and objectively controllable way, guiding the 
development activities from requirements capture to their implementation and 
thus bridging the gap between the two ends of system development:

* the human understanding and formulation of real-world problems, 
* the deployment of their algorithmic solutions by code-executing machines.

We illustrate the three constituents of the method, namely the notions of ASM 
(generalizing FSMs by abstract states), of ASM ground models (system blueprints) 
and of ASM refinements (controlled introduction of details). Whereas ASM ground 
models are accurate descriptions of requirements at an application-domain-
determined abstraction level that provide an authoritative reference for the 
further system development activities, ASM refinements link more detailed 
descriptions at successive development stages in an organic and effectively 
maintainable chain of rigorous and coherent system models.

We explain how the method allows one to smoothly integrate into best software 
engineering practice both mathematical rigour and a consistent combination of 
system design and analysis (machine-supportable mathematical verification and 
experimental validation).

We highlight some outstanding applications of the method and illustrate its 
uniformity by a comparison with Parnas' table technique and Abrial's Event-B 
machines.