Skip to main content
SpringerLink
Log in

The ASM Method for System Design and Analysis. A Tutorial Introduction

  • Conference paper
Frontiers of Combining Systems (FroCoS 2005)

Part of the book series: Lecture Notes in Computer Science ((LNAI,volume 3717))

Included in the following conference series:

Abstract

We introduce into and survey the ASM method for high-level system design and analysis. We explain the three notions—Abstract State Machine [37], ASM ground model (system blueprint) [7] and ASM refinement [8]—that characterize the method, which integrates also current validation and verification techniques. We illustrate how the method allows the system engineer to rigorously capture requirements by ASM ground models and to stepwise refine these to code in a validatable and verifiable way.

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. Altenhofen, M., Börger, E., Lemcke, J.: A high-level specification for mediators. In: 1st International Workshop on Web Service Choreography and Orchestration for Business Process Management (2005)

    Google Scholar 

  2. Anlauff, M., Kutter, P.: Xasm Open Source (2001). Web pages at http://www.xasm.org/

  3. Barnett, M., Börger, E., Gurevich, Y., Schulte, W., Veanes, M.: Using Abstract State Machines at Microsoft: A case study. In: Gurevich, Y., Kutter, P.W., Odersky, M., Thiele, L. (eds.) ASM 2000. LNCS, vol. 1912, pp. 367–379. Springer, Heidelberg (2000)

    Chapter  Google Scholar 

  4. Barros, A., Börger, E.: A compositional framework for service interaction patterns and communication flows. In: Lau, K.-K., Banach, R. (eds.) ICFEM 2005. LNCS, vol. 3785, pp. 5–35. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  5. Börger, E.: High-level system design and analysis using Abstract State Machines. In: Hutter, D., Stephan, W., Traverso, P., Ullmann, M. (eds.) FM-Trends 1998. LNCS, vol. 1641, pp. 1–43. Springer, Heidelberg (1999)

    Chapter  Google Scholar 

  6. Börger, E.: The origins and the development of the ASM method for high-level system design and analysis. J. Universal Computer Science 8(1), 2–74 (2002)

    Google Scholar 

  7. Börger, E.: The ASM ground model method as a foundation of requirements engineering. In: Dershowitz, N. (ed.) Verification: Theory and Practice. LNCS, vol. 2772, pp. 145–160. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  8. Börger, E.: The ASM refinement method. Formal Aspects of Computing 15, 237–257 (2003)

    Article  MATH  Google Scholar 

  9. Börger, E.: Modeling with Abstract State Machines: A support for accurate system design and analysis. In: Rumpe, B., Hesse, W. (eds.) Modellierung 2004. GI-Edition Lecture Notes in Informatics, vol. P-45, pp. 235–239. Springer, Heidelberg (2004)

    Google Scholar 

  10. Börger, E.: From finite state machines to virtual machines (Illustrating design patterns and event-B models). In: Cohors-Fresenborg, E., Schwank, I. (eds.) Präzisionswerkzeug Logik–Gedenkschrift zu Ehren von Dieter Rödding. Forschungsinstitut für Mathematikdidaktik Osnabrück (2005); ISBN 3-925386-56-4

    Google Scholar 

  11. Börger, E.: Linking content definition and analysis to what the compiler can verify. In: Proc. IFIP WG Conference on Verified Software: Tools, Techniques, and Experiments, Zurich, Switzerland, October 2005. LNCS. Springer, Heidelberg (2005)

    Google Scholar 

  12. Börger, E., Bolognesi, T.: Remarks on turbo ASMs for computing functional equations and recursion schemes. In: Börger, E., Gargantini, A., Riccobene, E. (eds.) ASM 2003. LNCS, vol. 2589, pp. 218–228. Springer, Heidelberg (2003)

    Chapter  Google Scholar 

  13. Börger, E., Busch, H., Cuellar, J., Päppinghaus, P., Tiden, E., Wildgruber, I.: Konzept einer hierarchischen Erweiterung von EURIS. Siemens ZFE T SE 1 Internal Report BBCPTW91-1, pp. 1–43, Summer (1996)

    Google Scholar 

  14. Börger, E., Dässler, K.: Prolog: DIN papers for discussion. ISO/IEC JTCI SC22 WG17 Prolog Standardization Document 58, National Physical Laboratory, Middlesex, England (1990)

    Google Scholar 

  15. Börger, E., Del Castillo, G.: A formal method for provably correct composition of a real-life processor out of basic components (The APE100 Reverse Engineering Study). In: Werner, B. (ed.) Proc. 1st IEEE Int. Conf. on Engineering of Complex Computer Systems (ICECCS 1995), November 1995, pp. 145–148 (1995)

    Google Scholar 

  16. Börger, E., Durdanović, I.: Correctness of compiling Occam to Transputer code. Computer Journal 39(1), 52–92 (1996)

    Article  Google Scholar 

  17. Börger, E., Fruja, G., Gervasi, V., Stärk, R.: A high-level modular definition of the semantics of C#. Theoretical Computer Science 336(2/3) (2005)

    Google Scholar 

  18. Börger, E., Glässer, U., Müller, W.: The semantics of behavioral VHDL 1993 descriptions. In: EURO-DAC 1994. European Design Automation Conference with EURO-VHDL 1994, pp. 500–505. IEEE Computer Society Press, Los Alamitos (1994)

    Google Scholar 

  19. Börger, E., Päppinghaus, P., Schmid, J.: Report on a practical application of ASMs in software design. In: Gurevich, Y., Kutter, P.W., Odersky, M., Thiele, L. (eds.) ASM 2000. LNCS, vol. 1912, pp. 361–366. Springer, Heidelberg (2000)

    Chapter  Google Scholar 

  20. Börger, E., Rosenzweig, D.: The WAM – definition and compiler correctness. In: Beierle, C., Plümer, L. (eds.) Logic Programming: Formal Methods and Practical Applications, ch. 2. Studies in Computer Science and Artificial Intelligence, vol. 11, pp. 20–90. North-Holland, Amsterdam (1995)

    Google Scholar 

  21. Börger, E., Schmid, J.: Composition and submachine concepts for sequential ASMs. In: Clote, P.G., Schwichtenberg, H. (eds.) CSL 2000. LNCS, vol. 1862, pp. 41–60. Springer, Heidelberg (2000)

    Chapter  Google Scholar 

  22. Börger, E., Schulte, W.: Initialization problems for Java. Software – Concepts and Tools 19(4), 175–178 (2000)

    Article  MATH  Google Scholar 

  23. Börger, E., Sona, D.: A neural abstract machine. J. Universal Computer Science 7(11), 1007–1024 (2001)

    Google Scholar 

  24. Börger, E., Stärk, R.F.: Abstract State Machines. A Method for High-Level System Design and Analysis. Springer, Heidelberg (2003)

    MATH  Google Scholar 

  25. Castillo, G.D., Päppinghaus, P.: Designing software for internet telephony: experiences in an industrial development process. In: Blass, A., Börger, E., Gurevich, Y. (eds.) Theory and Applications of Abstract State Machines, Schloss Dagstuhl, Int. Conf. and Research Center for Computer Science (2002)

    Google Scholar 

  26. Del Castillo, G.: The ASM Workbench. A Tool Environment for Computer-Aided Analysis and Validation of Abstract State Machine Models. PhD thesis, Universität Paderborn, Germany (2001)

    Google Scholar 

  27. Del Castillo, G., Winter, K.: Model checking support for the ASM high-level language. In: Schwartzbach, M.I., Graf, S. (eds.) TACAS 2000. LNCS, vol. 1785, pp. 331–346. Springer, Heidelberg (2000)

    Chapter  Google Scholar 

  28. Dold, A.: A formal representation of Abstract State Machines using PVS. Verifix Technical Report Ulm/6.2, Universität Ulm, Germany (July 1998)

    Google Scholar 

  29. Dold, A., Gaul, T., Vialard, V., Zimmermann, W.: ASM-based mechanized verification of compiler back-ends. In: Glässer, U., Schmitt, P. (eds.) Proc. 5th Int. Workshop on Abstract State Machines, pp. 50–67. Magdeburg University (1998)

    Google Scholar 

  30. Farahbod, R., Gervasi, V., Glässer, U.: CoreASM: An extensible ASM execution engine. In: Beauquier, D., Börger, E., Slissenko, A. (eds.) Proc.ASM 2005, Université de Paris (December 2005)

    Google Scholar 

  31. Foundations of Software Engineering Group, Microsoft Research. AsmL (2001). Web pages at http://research.microsoft.com/foundations/AsmL/

  32. Fruja, N.G.: Specification and implementation problems for C#. In: Zimmermann, W., Thalheim, B. (eds.) ASM 2004. LNCS, vol. 3052, pp. 127–143. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  33. Gargantini, A., Riccobene, E.: Encoding Abstract State Machines in PVS. In: Gurevich, Y., Kutter, P.W., Odersky, M., Thiele, L. (eds.) ASM 2000. LNCS, vol. 1912, pp. 303–322. Springer, Heidelberg (2000)

    Chapter  Google Scholar 

  34. Gawanmeh, A., Tahar, S., Winter, K.: Interfacing ASMs with the MDG tool. In: Börger, E., Gargantini, A., Riccobene, E. (eds.) ASM 2003. LNCS, vol. 2589, pp. 278–292. Springer, Heidelberg (2003)

    Chapter  Google Scholar 

  35. Glässer, U., Gotzhein, R., Prinz, A.: Formal semantics of SDL-2000: Status and perspectives. Computer Networks 42(3), 343–358 (2003)

    Article  MATH  Google Scholar 

  36. Goos, G., Zimmermann, W.: Verifying compilers and ASMs. In: Gurevich, Y., Kutter, P.W., Odersky, M., Thiele, L. (eds.) ASM 2000. LNCS, vol. 1912, pp. 177–202. Springer, Heidelberg (2000)

    Chapter  Google Scholar 

  37. Gurevich, Y.: Evolving algebras 1993: Lipari Guide. In: Börger, E. (ed.) Specification and Validation Methods, pp. 9–36. Oxford University Press, Oxford (1995)

    Google Scholar 

  38. Habibi, A.: Framework for System Level Verification: The SystemC Case. PhD thesis, Concordia University, Montreal (July 2005)

    Google Scholar 

  39. Heberle, A.: Korrekte Transformationsphase – der Kern korrekter Übersetzer. PhD thesis, Universität Karlsruhe, Germany (2000)

    Google Scholar 

  40. Huggins, J.: Kermit: Specification and verification. In: Börger, E. (ed.) Specification and Validation Methods, pp. 247–293. Oxford University Press, Oxford (1995)

    Google Scholar 

  41. Kalinov, A., Kossatchev, A., Petrenko, A., Posypkin, M., Shishkov, V.: Using ASM specifications for compiler testing. In: Börger, E., Gargantini, A., Riccobene, E. (eds.) ASM 2003. LNCS, vol. 2589, pp. 415–415. Springer, Heidelberg (2003)

    Chapter  Google Scholar 

  42. Lavagno, L., Sangiovanni-Vincentelli, A., Sentovitch, E.M.: Models of computation for system design. In: Börger, E. (ed.) Architecture Design and Validation Methods, pp. 243–295. Springer, Heidelberg (2000)

    Google Scholar 

  43. Schellhorn, G.: Verification of ASM refinements using generalized forward simulation. J. Universal Computer Science 7(11), 952–979 (2001)

    MathSciNet  Google Scholar 

  44. Schellhorn, G.: ASM refinement and generalizations of forward simulation in data refinement: A comparison. Theoretical Computer Science (2004)

    Google Scholar 

  45. Schellhorn, G., Ahrendt, W.: Reasoning about Abstract State Machines: The WAM case study. J. Universal Computer Science 3(4), 377–413 (1997)

    MATH  MathSciNet  Google Scholar 

  46. Schmid, J.: Executing ASM specifications with AsmGofer. Web pages at http://www.tydo.de/AsmGofer

  47. Schmid, J.: Compiling Abstract State Machines to C++. J. Universal Computer Science 7(11), 1069–1088 (2001)

    Google Scholar 

  48. Schmid, J.: Refinement and Implementation Techniques for Abstract State Machines. PhD thesis, University of Ulm, Germany (2002)

    Google Scholar 

  49. Stärk, R.F., Börger, E.: An ASM specification of C# threads and the .NET memory model. In: Zimmermann, W., Thalheim, B. (eds.) ASM 2004. LNCS, vol. 3052, pp. 38–60. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  50. Stärk, R.F., Nanchen, S.: A logic for Abstract State Machines. J. Universal Computer Science 7(11), 981–1006 (2001)

    Google Scholar 

  51. Stärk, R.F., Schmid, J., Börger, E.: Java and the Java Virtual Machine: Definition, Verification, Validation. Springer, Heidelberg (2001)

    MATH  Google Scholar 

  52. Vajihollahi, M.: High level specification and validation of the Business Process Execution Language for web services. Master’s thesis, School of Computing Science at Simon Fraser University (April 2004)

    Google Scholar 

  53. Zimmerman, W., Gaul, T.: On the construction of correct compiler back-ends: An ASM approach. J. Universal Computer Science 3(5), 504–567 (1997)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Dipartimento di Informatica, Università di Pisa, I-56125, Pisa, Italy

    Egon Börger

Authors
  1. Egon Börger
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Fakultät für Informatik, Technische Universität Wien, Favoritenstr. 9 – E185/2, A-1040, Wien, Austria

    Bernhard Gramlich

Rights and permissions

Reprints and permissions

Copyright information

© 2005 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Börger, E. (2005). The ASM Method for System Design and Analysis. A Tutorial Introduction. In: Gramlich, B. (eds) Frontiers of Combining Systems. FroCoS 2005. Lecture Notes in Computer Science(), vol 3717. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11559306_15

Download citation

  • DOI: https://doi.org/10.1007/11559306_15

  • Publisher Name: Springer, Berlin, Heidelberg

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

  • Online ISBN: 978-3-540-31730-2

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation