Abstract
Gurevich’s [26] Abstract State Machines (ASMs), characterized by the parallel execution of abstract atomic actions in a global state, have been equipped in [13] with a refinement by standard composition concepts for structuring large machines that allows reusing machine components. Among these concepts are parameterized (possibly recursive) sub-ASMs. Here we illustrate their power for incremental and modular system design by unfolding, via appropriate ASM components, the architecture of the Java Virtual Machine (JVM), resulting from the language layering in combination with the functional decomposition of the JVM into loader, verifier, and interpreter.We survey the ASM models for Java and the JVM that appear in [34], together with the mathematical and experimental analysis they support.
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
J. R. Abrial. The B-Book. Assigning Programs to Meanings. Cambridge University Press, 1996.
E. Börger. A logical operational semantics for full Prolog. Part I: Selection core and control. In E. Börger, H. Kleine-Büning, and M. Richter, editors, CSL 89, number 440 in Lecture Notes in Computer Science, pages 36–64. Springer-Verlag, 1989.
E. Börger. A logical operational semantics for full Prolog. Part II: Built-in predicates for database manipulations. In B. Rovan, editor, MFCS’90. Mathematical Foundations of Computer Science, number 452 in Lecture Notes in Computer Science, pages 1–14. Springer-Verlag, 1990.
E. Börger. Logic programming: The evolving algebra approach. In B. Pehrson and I. Simon, editors, IFIP 13th World Computer Congress 1994. Volume I: Technology and Foundations, pages 391–395. Elsevier, Amsterdam, 1994.
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), number 1641 in Lecture Notes in Computer Science, pages 1–43. Springer-Verlag, 1999.
E. Börger. Abstract State Machines at the cusp of the millenium. In Y. Gurevich, P. Kutter, M. Odersky, and L. Thiele, editors, Abstract State Machines. Theory and Applications, number 1912 in Lecture Notes in Computer Science, pages 1–8. Springer-Verlag, 2000.
E. Börger, A. Cavarra, and E. Riccobene. An ASM semantics for UML Activity Diagrams. In T. Rust, editor, Proc. AMAST 2000, number 1912 in Lecture Notes in Computer Science, pages 361–366. Springer-Verlag, 2000.
E. Börger, A. Cavarra, and E. Riccobene. Modeling the Dynamics of UML State Machines. In Y. Gurevich, P. Kutter, M. Odersky, and L. Thiele, editors, Abstract State Machines. Theory and Applications, number 1912 in Lecture Notes in Computer Science, pages 223–241. Springer-Verlag, 2000.
E. Börger and K. Dässler. Prolog: DIN papers for discussion. In ISO/IEC JTCI SC22 WG17 Prolog standardization document, number 58 in ISO/IEC Documents, pages 92–114. NPL Middlesex, 1990.
E. Börger and I. Durdanovic. Correctness of Compiling Occam to Transputer Code. Computer Journal, 39(1):52–92, 1996.
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. Special Requirement Engineering Issue.
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, pages 20–90. Elsevier Science B.V./ North-Holland, 1995.
E. Börger and J. Schmid. Composition and submachine concepts. In P. G. Clote and H. Schwichtenberg, editors, Computer Science Logic (CSL 2000), number 1862 in Lecture Notes in Computer Science, pages 41–60. Springer-Verlag, 2000.
E. Börger, J. Schmid, and P. Päppinghaus. 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, number 1912 in Lecture Notes in Computer Science, pages 361–366. Springer-Verlag, 2000.
U. Glässer, Y. Gurevich, and M. Veanes. Universal Plug and PlayMachine Models. Technical Report MSR-TR-2001-59, Microsoft Research, 2001.
W. Goerigk and H. Langmaack. Compiler Implementation Verification and Trojan Horses. In D. Bainov, editor, Proc. 9th International Colloquium on Numerical Analysis and Computer Science with Applications, Plovdiv, Bulgaria, 2001. Extended Draft Version available at http://www.informatik.uni-kiel.de/~wg/-Berichte/Plovdiv.ps.gz.
W. Goerigk and H. Langmaack. Will Informatics be able to Justify the Construction of Large Computer Based Systems? Technical Report 2015, CS Department University of Kiel, 2001.
G. Goos and W. Zimmermann. Verification of compilers. In Correct System Design, number 1710 in Lecture Notes in Computer Science, pages 201–230. Springer-Verlag, 1999.
G. Goos and W. Zimmermann. Verifying compilers and ASMs. In Y. Gurevich, P. Kutter, M. Odersky, and L. Thiele, editors, Correct System Design, number 1912 in Lecture Notes in Computer Science, pages 177–202. Springer-Verlag, 2000.
J. Gosling, B. Joy, and G. Steele. The Java(tm) Language Specification. Addison Wesley, 1996.
J. Gosling, B. Joy, G. Steele, and G. Bracha. The Java(tm) Language Specification. Addison Wesley, second edition, 2000.
Y. Gurevich. Reconsidering Turing’s Thesis: Toward More Realistic Semantics of Programs. Technical Report CRL-TR-36-84, University of Michigan, Computing Research Lab, 1984.
Y. Gurevich. A New Thesis. Notices of the American Mathematical Society, page 317, 1985. abstract 85T-68-203, received May 13.
Y. Gurevich. Logic and the Challenge of Computer Science. In E. Börger, editor, Current Trends in Theoretical Computer Science, pages 1–57. Computer Science Press, 1988.
Y. Gurevich. Evolving algebras: An attempt to discover semantics. Bulletin of the EATCS, 43:264–284, 1991.
Y. Gurevich. Evolving Algebras 1993: Lipari Guide. In E. Börger, editor, Specification and Validation Methods, pages 9–36. Oxford University Press, 1995.
J. Huggins. Abstract State Machines. ASM Web pages, maintained at http://www.eecs.umich.edu/gasm/<http://www.eecs.umich.edu/gasm/>.
ISO. ISO/IEC 13211-1 Information Technology-Programming Languages-Prolog-Part 1: General Core. ISO, 1995.
ITU. ITU-T Recommendation Z-100: Languages for Telecommunications Applications-Specification and Description Language SDL. Annex F: SDL formal semantics definition, 2000.
A. Kappel. Implementation of Dynamic Algebras with an Application to Prolog. Master’s thesis, CS Dept., University of Dortmund, Germany, November 1990. An extended abstract “Executable Specifications based on Dynamic Algebras” appeared in A. Voronkov (ed.): Logic Programming and Automated Reasoning, volume 698 of LNAI, Springer, 1993, pages 229–240.
T. Lindholm and F. Yellin. The Java(tm) Virtual Machine Specification. Addison Wesley, second edition, 1999.
M. Russo. Java et ses aspect concurrents: semantiques formelle, visualisation et proprietes, 2001. PhD thesis University of Nice-Sophia-Antipolis.
J. Schmid. Executing ASM specifications with AsmGofer, 1999. Web pages at http://www.tydo.de/AsmGofer<http://www.tydo.de/AsmGofer>.
R. Stärk, J. Schmid, and E. Börger. Java and the Java Virtual Machine. Definition, Verification, Validation. Springer-Verlag, 2001.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2001 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Börger, E. (2001). Design for Reuse via Structuring Techniques for ASMs. In: Moreno-Díaz, R., Buchberger, B., Luis Freire, J. (eds) Computer Aided Systems Theory — EUROCAST 2001. EUROCAST 2001. Lecture Notes in Computer Science, vol 2178. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45654-6_2
Download citation
DOI: https://doi.org/10.1007/3-540-45654-6_2
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-42959-3
Online ISBN: 978-3-540-45654-4
eBook Packages: Springer Book Archive