Abstract State Machines: Surveying their Theory and their Industrial Employment

E. Boerger and Joachim Schmid.

April 1st Morning (half day)

ASMs have been proved to be a scientifically well founded and an industrially viable method for the design and analysis of complex systems, which has been applied successfully to programming languages, protocols, embedded systems, architectures, requirements engineering, etc. The analysis covers both verification and validation, using mathematical (possibly theorem-prover-verified or model-checked) reasoning or experimental simulation (by running the executable models). The tutorial, presented by Egon Boerger, starts from scratch by introducing the definition and simple examples of ASMs. Their major scientific and industrial applications are surveyed, covering the period from 1990-2000.

Then an outstanding case study is presented, namely the ASM Definition, Verification and Analysis of JAVA and the Java Virtual Machine (forthcoming book by Robert Staerk, Joachim Schmid and Egon Boerger).

The tutorial concludes with an introduction, presented by Joachim Schmid, of ASMGofer, an ASM programming system making ASM models executable by programming the external functions in Haskell. The ASMGofer introduction includes a demo of the executable versions of the Java/JVM ASM models.