Distribution of a Simple Shared Dataspace Architecture

• Autorzy: Orzan S. , van de Pol. J.
• Języki publikacji: EN

Abstrakty

EN

We study a simple software architecture, in which components are coordinated by writing into and reading from a global set. This simple architecture is inspired by the industrial software architecture Splice. We present two results. First, a distributed implementation of the architecture is given and proved correct formally. In the implementation, local sets are maintained and data items are exchanged between these local sets. Next we show that the architecture is sufficiently expressive in principle. In particular, every global specification of a system's behaviour can be divided into components, which coordinate by read and write primitives on a global set only. We heavily rely on recent concepts and proof methods from process algebra.

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2006
• Tom: Vol. 73, nr 4
• Strony: 535--559
• Opis fizyczny: bibliogr. 28 poz.

Twórcy

autor

Orzan S.

autor

van de Pol. J.

• TU/e, P.O.Box 513, 5600MB Eindhoven, The Netherlands,

Bibliografia

• [1] S.C.C. Blom,W.J. Fokkink, J.F. Groote, I. van Langevelde, B. Lisser, and J.C. van de Pol. μCRL: A toolset for analysing algebraic specifications. In Proceedings CAV'01, volume 2102 of LNCS, pages 250-254, 2001.
• [2] M.A. Bezem and J.F. Groote. Invariants in process algebra with data. In Proceedings CONCUR'94, volume 836 of LNCS, pages 401-416, 1994.
• [3] N. Busi, R. Gorrieri, and G. Zavattaro. On the Turing equivalence of Linda coordination primitives. In Proceedings Express'97, volume 7 of ENTCS, 1997.
• [4] N. Busi, R. Gorrieri, and G. Zavattaro. Process calculi for coordination: From Linda to JavaSpaces. In Proceedings AMAST'00, volume 1816 of LNCS, 2000.
• [5] R. Bloo, J.M. Hooman, and E. de Jong. Semantical aspects of an architecture for distributed embedded systems. In Proceedings SAC'00, pages 149-155, 2000.
• [6] J.A. Bergstra and J.W. Klop. Algebra of communicating processes with abstraction. Theoretical Computer Science, 37(1):77-121, 1985.
• [7] M.M. Bonsangue, J.N. Kok, and G. Zavattaro. Comparing coordination models based on shared distributed replicated data. In Proceedings SAC'99, pages 146 - 155, 1999.
• [8] M.M. Bonsangue, J.N. Kok, and G. Zavattaro. Comparing software architectures for coordination languages. In Proceedings COORDINATION'99, volume 1594 of LNCS, pages 150-164, 1999.
• [9] M. Boasson. Control systems software. IEEE Transactions on Automatic Control, 38(7):1094-1106, 1993.
• [10] J.C.M. Baeten andW.P. Weijland. Process Algebra. Cambridge University Press, 1990.
• [11] N. Carriero and D. Gelernter. Linda in context. Communications of the ACM, 32(4):444-458, 1989.
• [12] P.F.G. Dechering and E. de Jong. Transparent object replication: A formal model. In Proceedings WORDS'99, 2000.
• [13] P.F.G. Dechering and I.A. van Langevelde. The verification of coordination. In Proceedings COORDINATION'00, volume 1906 of LNCS, 2000.
• [14] R. De Nicola, G. Ferrari, and R. Pugliese. KLAIM: A kernel language for agent interaction and mobility. IEEE Transactions on Software Engineering, 24(5):315-330, 1998.
• [15] E. Freeman, S. Hupfer, and K. Arnold. JavaSpaces principles, patterns, and practice. Addison-Wesley, 1999.
• [16] W. Fokkink. Introduction to Process Algebra. Texts in Theoretical Computer Science (EATCS). Springer-Verlag, 2000.
• [17] J.F. Groote, A. Ponse, and Y.S. Usenko. Linearization in parallel pCRL. Journal of Logic and Algebraic Programming, 48(1-2):39-72, 2001.
• [18] J.F. Groote and M.A. Reniers. Algebraic process verification. In J.A. Bergstra, A. Ponse, and S.A. Smolka, editors, Handbook of Process Algebra, pages 1151-1208. North-Holland, 2001.
• [19] J.F. Groote and J.S. Springintveld. Focus points and convergent process operators: a proof strategy for protocol verification. Journal of Logic and Algebraic Programming, 49(1-2):31-60, 2001.
• [20] R.J. van Glabbeek and W.P. Weijland. Branching time and abstraction in bisimulation semantics. Journal of the ACM, 43(3):555-600, 1996.
• [21] J.M. Hooman and J.C. van de Pol. Formal verification of replication on a distributed data space architecture. In Proceedings SAC'02, pages 351-358, 2002.
• [22] H. Korver and A. Sellink. A formal axiomatization for alphabet reasoning with parametrized processes. Formal Aspects of Computing, 10(1):30-42, 1998.
• [23] R. Langerak. Transformations and Semantics for LOTOS. PhD thesis, Department of Computer Science, University of Twente, 1992.
• [24] Nany Lynch. Distributed Algorithms. Morgan Kaufmann, 1996.
• [25] U. Nestmann and B.C. Pierce. Decoding choice encodings. In Proceedings CONCUR'96, volume 1119 of LNCS, pages 179-194, 1996.
• [26] Gian Pietro Picco, Amy L.Murphy, and Gruia-Catalin Roman. LIME: Lindameets mobility. In Proceedings ICSE'99, pages 368-377, 1999.
• [27] J.C. van de Pol and M. Valero Espada. Formal specification of JavaSpacesTM architecture using μCRL. In Proceedings COORDINATION'02, volume 2315 of LNCS, pages 274-290, 2002.
• [28] A.I.T. Rowstron and A.M. Wood. Bonita: a set of tuple space primitives for distributed coordination. In Proceedings HICSS'97, pages 379-388, 1997.