CWI (THE NETHERLANDS)
muCRL (micro Common Representation Language)
CADP (Construction and Analysis of Distributed Processes)
1700 lines of muCRL
JavaSpacesTM is a coordination architecture
developed by Sun Microsystems, based on the Linda paradigm and
implemented as a JiniTM service. It provides
strong high-level primitives for communication and synchronization,
guaranteeing global consistency. JavaSpaces applications consist of
loosely-coupled agents, which communicate by sharing information via a
common dataspace. The basic operations are writing, reading, and
looking up objects in the dataspace. Also, notify operations allow an
agent to inform the dataspace about its interest in future incoming
data entries matching a certain template. JavaSpaces operations can be
grouped in transactions, which preserve the ACID properties: Atomicity,
Consistency, Isolation, and Durability.
In order to verify JavaSpaces applications formally, a model of JavaSpaces was developed in muCRL. The shared dataspace and the application agents are modeled as muCRL processes. The muCRL toolset can then be used to generate the state space of the system, which is subsequently analyzed using the CADP verification toolbox.
This methodology is illustrated by the analysis of a typical coordination problem, called parallel summation. The dataspace is initially filled with a multiset of numbers, which must be replaced by their total sum. The implementation of the system is required to be efficient and fault tolerant, and to allow transparent replication. The distributed algorithm proposed consists of a number of identical (Worker) processes that independently perform simple additions, and a Master process who is charged to publish the result when the complete sum has been computed.
Two versions of the algorithm were developed: a simple one, which implements a naive solution, and a sophisticated one, which enables replication and is fault tolerant. Various configurations of the system were studied, involving crashes of the Workers and of the Master, several application processes (between 1 and 4) and numbers of values (between 2 and 5). The main correctness requirement (the Master always publishes the correct result) was expressed in regular alternation-free mu-calculus and checked on the corresponding state spaces by using the EVALUATOR model-checker of CADP. The requirement was satisfied by the sophisticated version of the algorithm, but not by the simple one.
A general framework for analyzing JavaSpaces applications by means of
model-checking was developed and assessed using a non-trivial example
of coordination problem. This approach can be generalized in order to
solve other similar coordination problems, such as fault tolerant
distributed implementations of Berry and Boudol's chemical abstract
Jaco van de Pol and Miguel Valero Espada.
"Verification of JavaSpacesTM Parallel Programs".
Proceedings of the 3rd International Conference on Application of
Concurrency to System Design ACSD'03 (Guimaraes, Portugal), IEEE
Computer Society Press, pp. 196-205, June 2003.
Available from the CADP Web 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|