Equivalent Semantic Models for a Distributed Dataspace Architecture

Jozef Hooman and Jaco van de Pol

Appeared in: Proceedings Symposium on Formal Methods for Objects and Components (FMCO 2002), LNCS 2852, Springer-Verlag, pages 182-201, 2003.

ABSTRACT

The general aim of our work is to support formal reasoning about components on top of the distributed dataspace architecture Splice. To investigate the basic properties of Splice and to support compositional 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 verification framework based on the denotational semantics is applied to an example of top-down development and transparent replication.