Equivalent Semantic Models for a Distributed Dataspace Architecture

Abstract. The general aim of our work is to support formal reason-ing about components on top of the distributed dataspace architecture Splice. To investigate the basic properties of Splice and to support com-positional verification, we have defined a denotational semantics for a basic Splice-like language. To increase the confidence in this semantics, also an operational semantics has been defined which is shown to be equivalent to the denotational one using the theorem prover PVS. A ver-ification framework based on the denotational semantics is applied to an example of top-down development and transparent replication.