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 . 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.