JavaSpaces^TM Shared Data Space Architecture.

Organisation:	CWI (THE NETHERLANDS)
Method:	muCRL (micro Common Representation Language)
Tools used:	muCRL toolset CADP (Construction and Analysis of Distributed Processes)
Domain:	Coordination Architectures.
Period:	2002
Size:	n/a
Description:	JavaSpacesTM is a coordination architecture developed by Sun Microsystems as a JiniTM service. It allows two programming styles of process coordination: a shared dataspace (inspired from the Linda coordination language) and a reactive style. Application agents interact simultaneously with a shared dataspace of objects, the space being responsible for handling the concurrent access to the data. Agents can use several communication primitives: write places a copy of an entry into the shared space; read returns a copy of an object from the space that matches a given template, or null if no object has been found; ReadIfExists performs like read, but blocks if the matching object(s) have conflicting locks from one or more transactions; take returns a copy of an object and removes it from the space; TakeIfExists is the blocking counterpart of take; and notify expresses interest in future incoming objects, i.e., the space will notify an agent of the presence of an object matching a given template. JavaSpaces also supports a transactional model ensuring that a set of grouped operations are performed on the space atomically. Two specifications of the JavaSpaces architecture have been developed in muCRL: the first one [vdPol-Espada-02-a] focuses on the basic features of the shared dataspace style (write, read, take, ReadIfExists, TakeIfExists, and transactions), and the second one [vdPol-Espada-02-b] focuses on the implementation of the notify primitive. Two examples of JavaSpaces applications (an arcade Ping-Pong game, in which two players throw one ball from one to the other, and a "Hello world" notification example) were also specified. Several safety properties were described using regular alternation-free mu-calculus. Verification was performed by constructing the state spaces corresponding to the two JavaSpaces applications and by checking the safety properties on these state spaces using the EVALUATOR 3.0 model-checker of the CADP toolbox.
Conclusions:	The development of a formal specification of the JavaSpaces architecture has several benefits. Firstly, several difficulties in interpretation were found, some of which are solved in the implementation of JavaSpaces but not in its specification. Secondly, the formal specifications allow to model-check more complex JavaSpaces applications and also to study the architecture itself and resolve unclear or ambiguous points.
Publications:	[vdPol-Espada-02-a] Jaco van de Pol and Miguel Valero Espada. "Formal Specification of JavaSpacesTM Architecture using muCRL". Proceedings of 5th International Conference on Coordination Models and Languages COORDINATION'02 (York, UK), Lecture Notes in Computer Science vol. 2315, pp. 274-290, April 2002. Available on-line at: http://www.cwi.nl/~vdpol/papers/javaspaces.ps.Z or from the CADP Web site in PDF or PostScript [vdPol-Espada-02-b] Jaco van de Pol and Miguel Valero Espada. "MuCRL Specification of Event Notification in JavaSpacesTM". Proceedings of X Jornadas de Concurrencia (Jaca, Spain), pp. 191-204, Universidad de Zaragoza, June 2002. Available on-line at: http://www.cwi.nl/~vdpol/papers/notify.ps.Z or from the CADP Web site in PDF or PostScript
Contact:	Dr. Jaco van de Pol CWI / Department of Software Engineering SEN2 (Specification and Analysis of Embedded Systems) Kruislaan 413, 1098 SJ Amsterdam, The Netherlands Room: M341 Tel: +31-(0)20-592 4137 Fax: +31-(0)20-592 4199 E-mail: Jaco.van.de.Pol@cwi.nl
Further remarks:	This case study, amongst others, is described on the CADP Web site: http://cadp.inria.fr/case-studies

Back to the CADP case studies page