Skip to main content
SpringerLink
Log in

Modeling Software: From Theory to Practice

  • Conference paper
  • First Online:
FST TCS 2002: Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2002)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 2556))

Abstract

Modeling of software is hard. The most difficult task is to identify and remain faithful to the right levels of abstraction, to decide what should be in the model and what should be abstracted away. Abstract state machines (ASMs) give the modeler the maximal flexibility in dealing with this task. ASMs are able to simulate arbitrary computer systems on their natural level of abstraction. This is known as the ASM thesis; it has theoretical support and has been confirmed by numerous academic and industrial projects. In order to use ASMs for modeling industrial software, the group on Foundations of Software Engineering at Microsoft Research developed the Abstract State Machine Language. It provides a modern object-oriented, component-based specification environment complete with tools to test and enforce specifications.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. M. Barnett and W. Schulte. The ABCs of Specification: AsmL, Behavior, and Components, Informatica, 25(4), 2001.

    Google Scholar 

  2. M. Barnett and W. Schulte. Contracts, Components, and their Runtime Verification on the.NET Platform, Microsoft Research, Technical Report, MSR-TR-2002-38, 2002. To appear in The Journal of Systems and Software.

    Google Scholar 

  3. Blass and Y. Gurevich. Background, reserve, and Gandy machines, in Proc. Computer Science Logic, Lecture Notes in Computer Science, Vol. 1862, pages 1–17, Springer, 2000.

    Google Scholar 

  4. Blass and Y. Gurevich. Abstract State Machines Capture Parallel Algorithms. Microsoft Research, Technical Report, MSR-TR-2001-117, 2002. To appear in ACM Transactions on Computational Logic.

    Google Scholar 

  5. E. Börger. Why use evolving algebras for hardware and software engineering? Lecture Notes in Computer Science, Vol. 1012, pages 236–271, Springer, 1995.

    Google Scholar 

  6. E. Börger. High Level System Design and Analysis using Abstract State Machines. In D. Hutter, W. Stephan, P. Traverso, M. Ullman, eds., Current Trends in Applied Formal Methods (FM-Trends 98). Lecture Notes in Computer Science, Vol. 1641, pp. 1–43, Springer, 1999.

    Chapter  Google Scholar 

  7. E. Börger. The Origins and the Development of the ASM Method for High Level System Design and Analysis. Journal of Universal Computer Science, 2(8): 2–74, Springer, 2002.

    Google Scholar 

  8. E. Börger and J. Huggins, Abstract state machines 1988–1998: Commented ASM bibliography, Bulletin of EATCS, Nr 64, pages 105–128, 1998.

    Google Scholar 

  9. U. Glässer, Y. Gurevich and M. Veanes. An Abstract Communication Model. Microsoft Research, Technical Report, MSR-TR-2002-55, 2002.

    Google Scholar 

  10. Y. Gurevich. Evolving Algebras 1993: Lipari Guide. In E. Börger, editor, Specification and Validation Methods, Oxford University Press, pages 9–36, 1995.

    Google Scholar 

  11. Y. Gurevich, A new thesis, American Mathematical Society Abstracts, p. 317, 1985.

    Google Scholar 

  12. Y. Gurevich. Sequential Abstract State Machines Capture Sequential Algorithms, ACM Transactions on Computational Logic, vol. 1, no. 1, July 2000, pages 77–111.

    Article  MathSciNet  Google Scholar 

  13. Y. Gurevich and N. Tillmann. Partial Updates: Exploration. Journal of Universal Computer Science, 11(7): 917–951, Springer, 2001.

    MathSciNet  Google Scholar 

  14. W. Grieskamp, Y. Gurevich, W. Schulte and M. Veanes. Generating Finite State Machines from Abstract State Machines, ISSTA 02, Software Engineering Notes 27(4) 112–122, ACM, 2002.

    Article  Google Scholar 

  15. W. Reisig. On Gurevich’s Theorem for Sequential ASM, Informatik-Berichte Nr. 160, Humboldt-Universität zu Berlin, Juli 2002.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Microsoft Research, Redmond, WA, USA

    Margus Veanes

Authors
  1. Margus Veanes
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Department of Computer Science and Engineering, Indian Institute of Technology, 208016, Kanpur, India

    Manindra Agrawal  & Anil Seth  & 

Rights and permissions

Reprints and permissions

Copyright information

© 2002 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Veanes, M. (2002). Modeling Software: From Theory to Practice. In: Agrawal, M., Seth, A. (eds) FST TCS 2002: Foundations of Software Technology and Theoretical Computer Science. FSTTCS 2002. Lecture Notes in Computer Science, vol 2556. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-36206-1_5

Download citation

  • DOI: https://doi.org/10.1007/3-540-36206-1_5

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-00225-3

  • Online ISBN: 978-3-540-36206-7

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation