@inproceedings{gurevich2000using, author = {Gurevich, Yuri and Schulte, Wolfram and Veanes, Margus and Barnett, Mike}, title = {Using Abstract State Machines at Microsoft: A Case Study}, series = {Lecture Notes in Computer Science}, booktitle = {Abstract State Machines}, year = {2000}, month = {January}, abstract = {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.}, publisher = {Springer}, url = {http://approjects.co.za/?big=en-us/research/publication/using-abstract-state-machines-at-microsoft-a-case-study/}, pages = {367-379}, volume = {1912}, isbn = {3-540-67959-6}, edition = {Abstract State Machines}, }