Database of Case Studies Achieved Using CADP

JavaSpacesTM 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 our FTP 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 our FTP 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


Last modified: Fri Feb 19 09:12:04 2016.


Back to the CADP case studies page