Distributed Data Space Architectures Described in Space Calculus.

Organisation:	CWI (THE NETHERLANDS)
Method:	space calculus muCRL (micro Common Representation Language)
Tools used:	muCRL toolset CADP (Construction and Analysis of Distributed Processes)
Domain:	Coordination Architectures.
Period:	2003
Size:	n/a
Description:	A shared dataspace (or tuple space) architecture is a distributed storage of information, viewed as an abstract global store, where applications can perform read/write/delete operations on data. The space calculus is an experimental framework in which verification and simulation techniques can be applied to the design of distributed systems that use a shared dataspace to coordinate their components. The shared space is modeled as a graph with atomic spaces as nodes, related by eager or lazy links. When data elements are written in a local space, they are asynchronously transferred over all eager links starting at this local space (eager links allow to model subscription and notification mechanisms). Lazy links are demand-driven: Only when data elements are requested in some atomic space, they are transferred via a lazy link from one of the neighboring spaces. The space calculus also provides a coordination language for representing applications. This language contains various communication primitives (such as write, blocking and non-blocking read, local and global take, publish, subscribe, etc.). Two different tools were developed for the space calculus: a translator to muCRL, which enables the construction of state spaces and their subsequent analysis using the CADP toolbox, and a distributed C code generator, which allows to simulate the system and estimate its performance (number of messages, used bandwidth, bottlenecks). The usefulness of analysis tools to space calculus descriptions was assessed by means of two applications. The first one describes a distributed implementation of the JavaSpaces coordination architecture. Two configurations of a ping-pong game (running on one and two JavaSpaces, respectively) were described in space calculus, translated in muCRL, and checked to be safety equivalent using the CADP toolbox. The second application studies the transparent replication mechanisms implemented in the Splice coordination architecture. The Splice system considered contains three kinds of components: Producer (which writes data to the Splice network), Transformer (which reads the data, applies some transformations on it and writes it back to the network), and Consumer (which reads the transformed data and uses it). Two configurations of this system, containing a single and a replicated transformer, were described in space calculus and checked to be safety equivalent using CADP.
Conclusions:	The space calculus provides a framework for modeling and comparing various paradigms of coordination (such as Splice and Javaspaces). By developing connections to process algebraic languages such as muCRL and standard verification tools such as CADP, individual systems based on shared dataspace architectures can be successfully analyzed.
Publications:	[Orzan-vandePol-03] Simona Orzan and Jaco van de Pol. "Verification of Distributed Dataspace Architectures". Proceedings of the 5th Andrei Ershov International Conference on Perspectives of System Informatics PSI'2003 (Novosibirsk, Russia), Lecture Notes in Computer Science vol. 2890, pp. 192-206, July 2003. Available on-line at: http://www.cwi.nl/~vdpol/papers/psi_full.ps.Z or from the CADP Web site in PDF or PostScript
Contact:	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