Architecture Design and Analysis

In the research reported here, the ASM (Abstract State Machines) method has been used to develop a practically viable method for defining, in a rigorous but concise way, models for various instruction set architectures and virtual machines.The operational and abstract character of ASMs

• makes the faithfulness of the definitions with respect to the design intentions checkable by direct inspection,
• supports, by stepwise refinements, linking the high-level definition in a transparent and well documented (possibly proven to be correct) way to its implementation.

For a systematic exposition of the ASM systems engineering method in its full generality see the AsmBook. The ASM method provides in particular a framework for the design and the mathematical analysis of architectures. The following papers have pioneered the method through some characteristic examples.

• Java and the JavaVirtual Machine: Definition, Verification, Validation
  Book by R. Stärk, J. Schmid, E. Börger, Springer-Verlag, 2001

• RISC DLX Architecture: Springer LNCS 1212 (1997) 151-187 or AsmBook Ch.3.3

• Transputer Instruction Set Architecture: The Computer Journal 39 (1) 52-92, 1996.
  The ground model for the underlying programming language appears in OCCAM

• Parallel Processor APE100: Ground model APESE and its verified composition (IEEE Proc. ICECCS'95, 145-148). Full Technical Report version Ape100TR

• Parallel Virtual Machine: shortversion Ifip94, full Technical Report version PVM

• Hardware Design Language VHDL: VHDL93Semantics and VHDL93Interpreter