From the Conference ASM 2000, published in Abstract State Machines: Theory and Applications, volume 1912 of Lecture Notes in Computer Science, pages 367--379, Springer-Verlag, March 2000.
Using Abstract State Machines at Microsoft: A Case Study
Mike Barnett; Egon Börger; Yuri Gurevich; Wolfram Schulte; Margus Veanes
March 2000
13 p.
Formats:
PDF 329 Kbytes
 

Our goal is to provide a rigorous method, clear notation and convenient tool support for high-level system design and analysis. For this purpose we use abstract state machines (ASMs). Here we describe a particular case study: modeling a debugger of a stack based runtime environment. The study provides evidence for ASMs being a suitable tool for building executable models of software systems on various abstraction levels, with precise refinement relationships connecting the models. High level ASM models of proposed or existing programs can be used throughout the software development cycle. In particular, ASMs can be used to model inter component behavior on any desired level of detail. This allows one to specify application programming interfaces more precisely than it is done currently.

BibTeX Entry