CWI (THE NETHERLANDS)
muCRL (micro Common Representation Language)
CADP (Construction and Analysis of Distributed Processes)
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.
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.
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 our FTP site in PDF or PostScript
Jaco van de Pol
CWI / Department of Software Engineering
SEN2 (Specification and Analysis of Embedded Systems)
Kruislaan 413, 1098 SJ Amsterdam, The Netherlands
Tel: +31-(0)20-592 4137
Fax: +31-(0)20-592 4199
|Further remarks:||This case study, amongst others, is described on the CADP Web site: http://cadp.inria.fr/case-studies|