We have proven that for the coordination language
introduced in section 2, the semantics according to
the conceptual model of a single global dataspace (presented in
section 3) is equivalent to the semantics corresponding to
the distributed implementation model with a local dataspace
for each process (presented
in section 4).
This proof has been completely formalized and checked mechanically by means of
the interactive theorem prover of PVS. We found this kind of tool support
very useful for checking the correctness of the
semantics definition as well as the proof itself.
Without mechanized support,
the error in the definition of the semantics of the 
-operator as
explained in section 4
might not have been found.
Due to the equivalence it is now possible to use the global dataspace semantics for formally verifying properties of a system implemented on an architecture with local dataspaces.
Interesting subjects for further research are a formal equivalence proof of our semantics and a more operational transition system semantics in the style of [3]. We expect that it is rather straightforward to extend the language with loops and non-blocking readoperations. Furthermore, one of our goals is to study the use of formal methods and techniques in the design process leading from the formal requirements specification of a system towards its correct implementation. In other work (cf. [9,10]), a method for writing formal requirements specifications in PVS has been developed. It is our goal to give a similar semantics as the one presented in this paper to these requirements specifications, and next devise a method to formally verify properties of an implementation of such a specification.