Formal Specification of JavaSpaces™ Architecture Using μCRL
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.
KeywordsModel Checker Application Program Interface Label Transition System Process Algebra External Process
Unable to display preview. Download preview PDF.
- 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
- 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
- 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
- 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
- N. Carriero and D. Gelernter. How to Write Parallel Programs: A First Course. MIT Press, 1990.Google Scholar
- 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
- 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
- W. J. Fokkink. Introduction to Process Algebra. Texts in Theoretical Computer Science. Springer-Verlag, 2000.Google Scholar
- E. Freeman, S. Hupfer, and K. Arnold. JavaSpaces principles, patterns, and practice. Addison-Wesley, Reading, MA, USA, 1999.Google Scholar
- 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
- 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
- R. Mateescu. Verification des proprietes temporelles des programmes paralleles. PhD thesis, Institut National Polytechnique de Grenoble, 1998.Google Scholar
- SUN Microsystems. JavaSpaces tm Service Specification, 1.1 edition, October 2000. See http://java.sun.com/products/javaspaces/.
- SUN Microsystems. Jini tm Technology Core Platform Specification, 1.1 edition, October 2000. See http://www.sun.com/jini/specs/.