In shared data space architectures, several applications coordinate by reading and writing to a common data store. In this talk we view the data space as a separate process. We show how a number of variants of shared data space architectures can be easily modeled in muCRL, at various levels of abstraction. The main examples of such shared data spaces are Splice (developed at Thales company) and JavaSpaces (developed at Sun Microsystems and derived from Linda).

The main goal of modelling shared data spaces in $mu$CRL is to use the muCRL toolset for the verification of systems based on these architectures. We demonstrate the verification of some small examples. In particular we emphasize the enormous state space reductions that are obtained by applying the techniques that we have been developing in recent years.

Besides verification technology, we have also used the muCRL description to prove some expressiveness results for a very basic version of Splice. In this version, the only operations are "write" and "blocking non-destructive read" on a global set. It appears that every global requirements specification (described in muCRL) has a distributed implementation on this weak architecture.