Formal Specification of JavaSpaces™ Architecture Using μCRL

  • Jaco van de Pol
  • Miguel Valero Espada
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 2315)


We study a formal specification of the shared data space architecture, JavaSpaces. This Java technology provides a virtual space for entities, like clients and servers, to communicate by sharing objects. We use μCRL, a language that combines abstract data types with process algebra, to model an abstraction of this coordination architecture. Besides the basic primitives write, read and take, our model captures transactions and leasing. The main purpose of the proposed formalism is to allow the verification of distributed applications built under the JavaSpaces model. A simple case study is analyzed and automatically model checked using the μCRL and CADP tool sets.


Model Checker Application Program Interface Label Transition System Process Algebra External Process 
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.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. [1]
    S.C.C. Blom, W.J. Fokkink, J.F. Groote, I.A. Langevelde, B. Lisser, and J.C. van de Pol. μCRL: a toolset for analysing algebraic specifications. In Proc. of CAV, LNCS 2102, pages 250–254. Springer, 2001.Google Scholar
  2. [2]
    M. Boasson. Control systems software. IEEE Trans. on Automatic Control, 38(7):1094–1106, July 1993.CrossRefMathSciNetGoogle Scholar
  3. [3]
    M.M. Bonsangue, J.N. Kok, and G. Zavattaro. Comparing coordination models based on shared distributed replicated data. In Proc. of SAC, pages 146–155. ACM, 1999.Google Scholar
  4. [4]
    N. Busi, R. Gorrieri, and G. Zavattaro. Process calculi for coordination: From Linda to JavaSpaces. In Proc. of AMAST, LNCS 1816, pages 198–212. Springer, 2000.Google Scholar
  5. [5]
    N. Busi and G. Zavattaro. On the serializability of transactions in JavaSpaces. In U. Montanari and V. Sassone, editors, Electronic Notes in Theoretical Computer Science, volume 54. Elsevier Science Publishers, 2001.Google Scholar
  6. [6]
    N. Carriero and D. Gelernter. How to Write Parallel Programs: A First Course. MIT Press, 1990.Google Scholar
  7. [7]
    P.F.G. Dechering and I.A. van Langevelde. The verification of coordination. In Proc. of COORDINATION, LNCS 1906, pages 335–340. Springer, 2000.Google Scholar
  8. [8]
    J.-C. Fernandez, H. Garavel, A. Kerbrat, L. Mounier, R. Mateescu, and M. Sighireanu. CADP — a protocol validation and verification toolbox. In Proc. of CAV, LNCS 1102, pages 437–440. Springer, 1996.Google Scholar
  9. [9]
    W. J. Fokkink. Introduction to Process Algebra. Texts in Theoretical Computer Science. Springer-Verlag, 2000.Google Scholar
  10. [10]
    E. Freeman, S. Hupfer, and K. Arnold. JavaSpaces principles, patterns, and practice. Addison-Wesley, Reading, MA, USA, 1999.Google Scholar
  11. [11]
    J.F. Groote and M.A. Reniers. Algebraic process verification. In J.A. Bergstra et al., editor, Handbook of Process Algebra, chapter 17. Elsevier, 2001.Google Scholar
  12. [12]
    J.M.M. Hooman and J.C. van de Pol. Formal verification of replication on a distributed data space architecture. In Proceedings ACM SAC, Coordination Models, Languages and Applications, page (to appear), Madrid, 2002. ACM press.Google Scholar
  13. [13]
    R. Mateescu. Verification des proprietes temporelles des programmes paralleles. PhD thesis, Institut National Polytechnique de Grenoble, 1998.Google Scholar
  14. [14]
    SUN Microsystems. JavaSpaces tm Service Specification, 1.1 edition, October 2000. See
  15. [15]
    SUN Microsystems. Jini tm Technology Core Platform Specification, 1.1 edition, October 2000. See

Copyright information

© Springer-Verlag Berlin Heidelberg 2002

Authors and Affiliations

  • Jaco van de Pol
    • 1
  • Miguel Valero Espada
    • 1
  1. 1.Centrum voor Wiskunde en InformaticaAmsterdamThe Netherlands

Personalised recommendations