×

Abstract state machines: a unifying view of models of computation and of system design frameworks. (English) Zbl 1066.68047

This paper formulates a new set of definitional suggestions for computation theory, which covers also system specification frameworks. Two concepts of the same author are used: control state Abstract State Machines (ASMs), as a natural extension of Finite State Machines (FSMs), and Turbo ASMs, to establish a sub-machine concept that fits the synchronous parallelism of ASMs and includes sequential composition and iteration. The author instantiates control state ASMs to classical automata and substitution systems: FSMs (like Moore-Mealy and their extensions by stream-processing, timing conditions, co-design control features), pushdown and computation universal automata (like Turing, Scott-Eilenberg, Minsky, Wegner), replacement systems (like Thue, Markov, Post and context-free, attribute and tree adjoining grammars for language generation). He also shows how to model by turbo ASMs structured and functional programming concepts and tree computations, including general forms of recursions. In the last part the author shows how to model by ASMs the basic semantical concepts of the executable high-level design languages UNITY and COLD, of widely used sequential and distributed state-based specification languages (illustrated for sequential system by Parnas tables and B machine, for distributed systems by Petri nets), of dedicated virtual machines and of axiomatic logic-based or stateless modelling systems (like denotational semantics, VDM, Z, and algebraic systems like process algebras).

MSC:

68Q05 Models of computation (Turing machines, etc.) (MSC2010)
68Q42 Grammars and rewriting systems

Software:

Z; UNITY
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Abrial, J.-R., The B-Book (1996), Cambridge University Press · Zbl 0915.68015
[2] Abrial, J.-R., Extending B without changing it (for developing distributed systems), (Habrias, H., 1st Conference on the B Method (1996)), 169-190
[3] Abrial, J.-R.; Mussat, L., Specification and design of a transmission protocol by successive refinements using B, (Broy, M.; Schieder, B., Mathematical Methods in Program Development (1996), Springer-Verlag) · Zbl 0884.68006
[4] Abrial, J.-R.; Mussat, L., Introducing dynamic constraints in B, (Bert, D., B’98: Recent Advances in the Development and Use of the B Method. B’98: Recent Advances in the Development and Use of the B Method, LNCS, vol. 1393 (1998), Springer-Verlag), 82-128
[5] Alur, R.; Dill, D. L., A theory of timed automata, Theoretical Computer Science, 126, 183-235 (1994) · Zbl 0803.68071
[6] Beierle, C.; Börger, E., Refinement of a typed WAM extension by polymorphic order-sorted types, Formal Aspects of Computing, 8, 5, 539-564 (1996) · Zbl 0876.68019
[7] Beierle, C.; Börger, E., Specification and correctness proof of a WAM extension with abstract type constraints, Formal Aspects of Computing, 8, 4, 428-462 (1996) · Zbl 0857.68016
[8] Blass, A.; Gurevich, Y., Abstract state machines capture parallel algorithms, ACM Transactions on Computational Logic, 3 (2002)
[9] Böhm, C.; Jacopini, G., Flow diagrams, Turing machines, and languages with only two formation rules, Communications of the ACM, 9, 5, 366-371 (1966) · Zbl 0145.24204
[10] Bolognesi, T.; Börger, E., Abstract state processes, (Börger, E.; Gargantini, A.; Riccobene, E., Abstract State Machines 2003—Advances in Theory and Applications. Abstract State Machines 2003—Advances in Theory and Applications, LNCS, vol. 2589 (2003), Springer-Verlag), 22-32 · Zbl 1021.68525
[11] Börger, E., Computability, Complexity, Logic (English translation of Berechenbarkeit, Komplexität, Logik), Studies in Logic and the Foundations of Mathematics, vol. 128 (1989), North-Holland
[12] Börger, E., High level system design and analysis using abstract state machines, (Hutter, D.; Stephan, W.; Traverso, P.; Ullmann, M., Current Trends in Applied Formal Methods, FM-Trends 98. Current Trends in Applied Formal Methods, FM-Trends 98, LNCS, vol. 1641 (1999), Springer-Verlag), 1-43
[13] E. Börger, Computation and specification models. A comparative study. in: P.D. Mosses (Ed.), Proceedings of the Fourth International Workshop on Action Semantics, December 2002, Department of Computer Science at University of Aarhus, BRICS Series, vol. NS-02-8, 2002, pp. 107-130; E. Börger, Computation and specification models. A comparative study. in: P.D. Mosses (Ed.), Proceedings of the Fourth International Workshop on Action Semantics, December 2002, Department of Computer Science at University of Aarhus, BRICS Series, vol. NS-02-8, 2002, pp. 107-130
[14] Börger, E., The origins and the development of the ASM method for high level system design and analysis, Journal of Universal Computer Science, 8, 1, 2-74 (2002)
[15] Börger, E.; Bolognesi, T., Remarks on turbo ASMs for computing functional equations and recursion schemes, (Börger, E.; Gargantini, A.; Riccobene, E., Abstract State Machines 2003—Advances in Theory and Applications. Abstract State Machines 2003—Advances in Theory and Applications, LNCS, vol. 2589 (2003), Springer-Verlag), 218-228 · Zbl 1021.68035
[16] Börger, E.; Durdanović, I., Correctness of compiling occam to transputer code, Computer Journal, 39, 1, 52-92 (1996)
[17] Börger, E.; López-Fraguas, F. J.; Rodríguez-Artalejo, M., A model for mathematical analysis of functional logic programs and their implementations, (Pehrson, B.; Simon, I., IFIP 13th World Computer Congress. IFIP 13th World Computer Congress, Technology/Foundations, vol. I (1994), Elsevier, Amsterdam: Elsevier, Amsterdam The Netherlands), 410-415
[18] Börger, E.; Rosenzweig, D., A mathematical definition of full prolog, Science of Computer Programming, 24, 249-286 (1995) · Zbl 0832.68022
[19] Börger, E.; Rosenzweig, D., The WAM—definition and compiler correctness, (Beierle, C.; Plümer, L., Logic Programming: Formal Methods and Practical Applications, Studies in Computer Science and Artificial Intelligence (1995), North-Holland), 20-90, (Chapter 2) · Zbl 0832.68024
[20] Börger, E.; Salamone, R., CLAM specification for provably correct compilation of CLP(R) programs, (Börger, E., Specification and Validation Methods (1995), Oxford University Press), 97-130 · Zbl 0852.68057
[21] Börger, E.; Schmid, J., Composition and submachine concepts for sequential ASMs, (Clote, P.; Schwichtenberg, H., Computer Science Logic, Proceedings of CSL 2000. Computer Science Logic, Proceedings of CSL 2000, LNCS, vol. 1862 (2000), Springer-Verlag), 41-60 · Zbl 0973.68066
[22] Börger, E.; Sona, D., A neural abstract machine, Journal of Universal Computer Science, 7, 11, 1007-1024 (2001)
[23] Börger, E.; Stärk, R., Abstract State Machines. A Method for High-Level System Design and Analysis (2003), Springer-Verlag · Zbl 1040.68042
[24] Chandy, K. M.; Misra, J., Parallel Program Design. A Foundation (1988), Addison Wesley · Zbl 0717.68034
[25] Davis, M., The Universal Computer: The Road from Leibniz to Turing (2000), W.W. Norton: W.W. Norton New York · Zbl 0960.01001
[26] Dijkstra, E. W., Structure of the T.H.E. multiprogrammming system, Communications of the ACM, 11, 341-346 (1968) · Zbl 0164.18704
[27] Eilenberg, S., Automata, Machines and Languages, vol. A (1974), Academic Press · Zbl 0317.94045
[28] Feijs, L. M.G.; Jonkers, H. B.M., Formal Specification and Design (1992), Cambridge University Press · Zbl 0774.68082
[29] Fitzgerald, J.; Larsen, P. G., Modelling Systems. Practical Tool and Techniques in Software Development (1998), Cambridge University Press
[30] Fruja, N. G.; Stärk, R. F., The hidden computation steps of turbo abstract state machines, (Börger, E.; Gargantini, A.; Riccobene, E., Abstract State Machines 2003—Advances in Theory and Applications. Abstract State Machines 2003—Advances in Theory and Applications, Lecture Notes in Computer Science, vol. 2589 (2003), Springer-Verlag), 244-262 · Zbl 1021.68036
[31] Glässer, U.; Gurevich, Y.; Veanes, M., High-level executable specification of the universal plug and play architecture, (Proceedings of 35th Hawaii International Conference on System Sciences—2002 (2002), IEEE Computer Society Press), 1-10
[32] Gurevich, Y., Evolving algebras 1993: Lipari guide, (Börger, E., Specification and Validation Methods (1995), Oxford University Press), 9-36 · Zbl 0852.68053
[33] Gurevich, Y., Sequential abstract state machines capture sequential algorithms, ACM Transactions on Computational Logic, 1, 1, 77-111 (2000) · Zbl 1365.68258
[34] Gurevich, Y.; Spielmann, M., Recursive abstract state machines, Journal of Universal Computer Science, 3, 4, 233-246 (1997) · Zbl 0960.68091
[35] Hall, J. A., Taking Z seriously, (ZUM’97. ZUM’97, LNCS, vol. 1212 (1997), Springer-Verlag)
[36] C. Heitmeyer, Using SCR methods to capture, document, and verify computer system requirements, in: E. Börger, B. Hörger, D.L. Parnas, D. Rombach (Eds.), Requirements Capture, Documentation, and Validation, Dagstuhl Seminar Report 99241, 1999; C. Heitmeyer, Using SCR methods to capture, document, and verify computer system requirements, in: E. Börger, B. Hörger, D.L. Parnas, D. Rombach (Eds.), Requirements Capture, Documentation, and Validation, Dagstuhl Seminar Report 99241, 1999
[37] J.W. Janneck, Syntax and semantics of graphs. Ph.D. Thesis, ETH Zürich, 2000; J.W. Janneck, Syntax and semantics of graphs. Ph.D. Thesis, ETH Zürich, 2000
[38] Johnson, D. E.; Moss, L. S., Grammar formalisms viewed as evolving algebras, Linguistics and Philosophy, 17, 537-560 (1994)
[39] Kohlbrenner, E.; Morris, D.; Morris, B., The history of virtual machines, Web pages at:
[40] Lavagno, L.; Sangiovanni-Vincentelli, A.; Sentovitch, E. M., Models of computation for system design, (Börger, E., Architecture Design and Validation Methods (2000), Springer-Verlag), 243-295
[41] Moschovakis, Y. N., What is an algorithm?, (Engquist, B.; Schmid, W., Mathematics Unlimited—2001 and Beyond (2001), Springer-Verlag) · Zbl 1025.03037
[42] Parnas, D.; Madey, J., Functional documents for computer systems, Science of Computer Programming, 25, 41-62 (1995)
[43] Reisig, W., Elements of Distributed Algorithms (1998), Springer-Verlag
[44] Scott, D., Definitional suggestions for automata theory, Journal of Computer and System Sciences, 1, 187-212 (1967) · Zbl 0164.32103
[45] Stärk, R.; Schmid, J.; Börger, E., Java and the Java Virtual Machine: Definition, Verification, Validation (2001), Springer-Verlag · Zbl 0978.68033
[46] Wegner, P., Why interaction is more powerful than algorithms, Communications of the ACM, 40, 80-91 (1997)
[47] Woodcock, J. C.P.; Davies, J., Using Z: Specification, Refinement, and Proof (1996), Prentice-Hall · Zbl 0855.68060
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.