Skip to main content
SpringerLink
Log in
Book cover

Languages for System Specification pp 247–269Cite as

Linking Architectural and Component Level System Views by Abstract State Machines

  • Chapter

Abstract

In hardware and software design model checkers are nowadays used with success to verify properties of system components [23]. The limits of the approach to cope with the size and the complexity of modern computerbased systems are felt when it comes to provide evidence of the trustworthiness of the entire system that has been built out of verified components. To achieve this task one has to experimentally validate or to mathematically verify the composition of the system. This reveals a gap between the finite state machine (FSM) view of model-checkable components and the architectural system view. In this paper we show how Abstract State Machines (ASM) can be used to fill this gap for both design and analysis, using a flexible concept of ASM component.

This is a preview of subscription content, 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   129.00
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD   169.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info
Hardcover Book
USD   169.99
Price excludes VAT (USA)
  • Durable hardcover 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

Learn about institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. M. Anlauff and P. Kutter. Xasm Open Source. Web pages at http://www.xasm.org/, 2001.

  2. M. Anlauff, P. Kutter, and A. Pierantonio. Montages/Gem-Mex: a meta visual programming generator. TIK-Report 35, ETH Zürich, Switzerland, 1998.

    Google Scholar 

  3. M. Anlauff, P. Kutter, and A. Pierantonio. Enhanced control flow graphs in Montages. In D. Bjoerner and M. Broy, editors, Proc. Perspectives of System Informatics (PSI’99), volume 1755 of Lecture Notes in Computer Science, pages 40–53. Springer-Verlag, 1999.

    Google Scholar 

  4. M. Anlauff, P. Kutter, A. Pierantonio, and A. Sünbül. Using domain-specific languages for the realization of component composition. In T. Maibaum, editor, Fundamental Approaches to Software Engineering (FASE 2000), volume 1783 of LNCS, pages 112–126, 2000.

    Google Scholar 

  5. M. Barnett and W. Schulte. The ABCs of specification: AsmL, behavior, and components. Informatica, 25(4):517–526, 2002.

    Google Scholar 

  6. M. Barnett and W. Schulte. Contracts, components and their runtime Verification on the NET platform. J. Systems and Software, Special Issue on Component-Based Software Engineering, 2002, to appear.

    Google Scholar 

  7. C. Beierle, E. Börger, I. Durdanović, U. Glässer, and E. Riccobene. Refining abstract machine specifications of the steam boiler control to well documented executable code. In J.-R. Abrial, E. Börger, and H. Langmaack, editors, Formal Methods for Industrial Applications. Specifying and Programming the Steam-Boiler Control, number 1165 in LNCS, pages 62–78. Springer, 1996.

    Google Scholar 

  8. T. Bolognesi and E. Börger. Abstract State Processes. In E. Börger, A. Gargantini, and E. Riccobene, editors, Abstract State Machines 2003-Advances in Theory and Applications, volume 2589 of Lecture Notes in Computer Science, pages 22–32. Springer-Verlag, 2003.

    Google Scholar 

  9. E. Börger. High-level system design and analysis using Abstract State Machines. In D. Hutter, W. Stephan, P. Traverso, and M. Ullmann, editors, Current Trends in Applied Formal Methods (FM-Trends 98), volume 1641 of LNCS, pages 1–43. Springer-Verlag, 1999.

    Google Scholar 

  10. E. Börger. The ASM ground model method as a foundation of requirements engineering. In N. Dershowitz, editor, Manna-Symposium, volume 2772 of LNCS. Springer-Verlag, 2003.

    Google Scholar 

  11. E. Börger. The ASM refinement method. Formal Aspects of Computing, 14, 2003.

    Google Scholar 

  12. E. Börger. Teaching asms to practice-oriented students. In Teaching Formal Methods Workshop, pages 5–12. Oxford Brookes University, 2003.

    Google Scholar 

  13. E. Börger. Abstract State Machines: A unifying view of models of computation and of system design frameworks. Annals of Pure and Applied Logic, 2003, to appear.

    Google Scholar 

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

    Google Scholar 

  15. E. Börger, G. Fruja, V. Gervasi, and R. Stärk. A complete formal Definition of the semantics of C#. Technical report, In preparation, 2003.

    Google Scholar 

  16. E. Börger, Y. Gurevich, and D. Rosenzweig. The bakery algorithm: Yet another specification and Verification. In E. Börger, editor, Specification and Validation Methods, pages 231–243. Oxford University Press, 1995.

    Google Scholar 

  17. E. Börger and L. Mearelli. Integrating ASMs into the software development life cycle. J. Universal Computer Science, 3(5):603–665, 1997.

    Google Scholar 

  18. E. Börger, P. Päppinghaus, and J. Schmid. Report on a practical application of ASMs in software design. In Y. Gurevich, P. Kutter, M. Odersky, and L. Thiele, editors, Abstract State Machines: Theory and Applications, volume 1912 of LNCS, pages 361–366. Springer-Verlag, 2000.

    Google Scholar 

  19. E. Börger, E. Riccobene, and J. Schmid. Capturing requirements by Abstract State Machines: The light control case study. J. Universal Computer Science, 6(7):597–620, 2000.

    Google Scholar 

  20. E. Börger and D. Rosenzweig. The WAM-Definition and compiler correctness. In C. Beierle and L. Plümer, editors, Logic Programming: Formal Methods and Practical Applications, volume 11 of Studies in Computer Science and Artificial Intelligence, chapter 2, pages 20–90. North-Holland, 1995.

    Google Scholar 

  21. E. Börger and J. Schmid. Composition and submachine concepts for sequential ASMs. In P. Clote and H. Schwichtenberg, editors, Computer Science Logic (Proceedings of CSL 2000), volume 1862 of Lecture Notes in Computer Science, pages 41–60. Springer-Verlag, 2000.

    Google Scholar 

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

    Google Scholar 

  23. E. M. Clarke, O. Grumberg, and D. A. Peled. Model Checking. MIT Press, 1999.

    Google Scholar 

  24. G. Del Castillo. 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 

  25. G. Del Castillo and K. Winter. Model checking support for the ASM high-level language. In S. Graf and M. Schwartzbach, editors, Proc. 6th Int. Conf. TACAS 2000, volume 1785 of Lecture Notes in Computer Science, pages 331–346. Springer-Verlag, 2000.

    Google Scholar 

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

    Google Scholar 

  27. A. Dold, T. Gaul, V. Vialard, and W. Zimmermann. ASM-based mechanized Verification of compiler back-ends. In U. Glässer and P. Schmitt, editors, Proc. 5th Int. Workshop on Abstract State Machines, pages 50–67. Magdeburg University, 1998.

    Google Scholar 

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

  29. A. Gargantini and E. Riccobene. Encoding Abstract State Machines in PVS. In Y. Gurevich, P. Kutter, M. Odersky, and L. Thiele, editors, Abstract State Machines: Theory and Applications, volume 1912 of LNCS, pages 303–322. Springer-Verlag, 2000.

    Google Scholar 

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

    Google Scholar 

  31. R. Groenboom and G. R. Renardel de Lavalette. A formalization of evolving algebras. In S. Fischer and M. Trautwein, editors, Proc. Accolade 95, pages 17–28. Dutch Research School in Logic, ISBN 90-74795-31-5, 1995.

    Google Scholar 

  32. A. Hejlsberg, S. Wiltamuth, and P. Golde. C# Language Specification. Addison-Wesley, 2003.

    Google Scholar 

  33. L. Lamport. Specifying Systems. Addison-Wesley, 2003.

    Google Scholar 

  34. L. Lavagno, A. Sangiovanni-Vincentelli, and E. M. Sentovitch. Models of computation for system design. In E. Börger, editor, Architecture Design and Validation Methods, pages 243–295. Springer-Verlag, 2000.

    Google Scholar 

  35. W. Mueller, R. Dömer, and A. Gerstlauer. The formal execution semantics of SpecC. Technical Report TR ICS 01-59, Center for Embedded Computer Systems at the University of California at Irvine, 2001.

    Google Scholar 

  36. S. Nanchen and R. F. Stärk. A security logic for Abstract State Machines. In TR 423 CS Dept ETH Zürich, 2003.

    Google Scholar 

  37. A. Poetzsch-Heffter. Deriving partial correctness logics from evolving algebras. In B. Pehrson and I. Simon, editors, IFIP 13th World Computer Congress, volume I: Technology/Foundations, pages 434–439, Elsevier, Amsterdam, 1994.

    Google Scholar 

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

    MathSciNet  Google Scholar 

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

    MathSciNet  Google Scholar 

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

  41. J. Schmid. Refinement and Implementation Techniques for Abstract State Machines. PhD thesis, University of Ulm, Germany, 2002.

    Google Scholar 

  42. A. Schönegge. Extending dynamic logic for reasoning about evolving algebras. Technical Report 49/95, Universität Karlsruhe, Fakultät für Informatik, Germany, 1995.

    Google Scholar 

  43. R. F. Stärk and E. Börger. An ASM specification of C# threads and the.NET memory model. Technical report, Computer Science Department, ETH Zürich, 2003.

    Google Scholar 

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

    Google Scholar 

  45. R. F. Stärk, J. Schmid, and E. Börger. Java and the Java Virtual Machine: Definition, Verification, Validation. Springer-Verlag, 2001.

    Google Scholar 

  46. A. Sünbül. Architectural Design of Evolutionary Software Systems in Continuous Software Engineering. PhD thesis, TU Berlin, Germany, 2001.

    Google Scholar 

  47. J. Teich, R. Weper, D. Fischer, and S. Trinkert. A joint architecture/ compiler design environment for ASIPs. In Proc. Int. Conf. on Compilers, Architectures and Synthesis for Embedded Systems (CASES2000), pages 26–33, San Jose, CA, USA, November 2000. ACM Press.

    Google Scholar 

  48. K. Winter. Model checking for Abstract State Machines. J. Universal Computer Science, 3(5):689–701, 1997.

    MATH  MathSciNet  Google Scholar 

  49. K. Winter. Model Checking Abstract State Machines. PhD thesis, Technical University of Berlin, Germany, 2001.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Dipartimento di Informatica, Università di 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. J.W. Goethe-Universität Frankfurt, Germany

    Christoph Grimm

Rights and permissions

Reprints and permissions

Copyright information

© 2004 Springer Science + Business Media, Inc.

About this chapter

Cite this chapter

Börger, E. (2004). Linking Architectural and Component Level System Views by Abstract State Machines. In: Grimm, C. (eds) Languages for System Specification. Springer, Boston, MA. https://doi.org/10.1007/1-4020-7991-5_16

Download citation

  • DOI: https://doi.org/10.1007/1-4020-7991-5_16

  • Publisher Name: Springer, Boston, MA

  • Print ISBN: 978-1-4020-7990-0

  • Online ISBN: 978-1-4020-7991-7

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation