Tool support

The verification system PVS [8]has been used to support our research. Two versions of the semantics, one for the conceptual view of a global dataspace and one for the implementation based view of local dataspaces, have been defined in PVS. The specification language of PVS is a classical, typed higher-order logic with a large number of built-in types (e.g. booleans, integers reals) and type-constructors (as functions, sets, tuples, records), including a powerful mechanism to define abstract datatypes. Specifications can be structured by hierarchies of parameterized theories.

The PVS system contains a powerful theorem prover that can be used to construct proofs of theorems interactively. Proofs are recorded and can be rerun after changes. All results mentioned in this paper have been checked mechanically by means of PVS.