Semantic Models of a Timed Distributed Dataspace
Jozef Hooman and
Jaco van de Pol
Appeared in:
Theoretical Computer Science,
Vol. 331, Springer-Verlag,
pages 291-323, 2005.
ABSTRACT
We investigate various formal aspects of a
distributed dataspace architecture in which
data storage is based on time stamps.
An operational and
a denotational semantics have been defined and
the equivalence of these two formulations has been proved.
Moreover, the denotational semantics
is fully abstract with respect to the observation
of produced data items.
It is used as a basis for
compositional reasoning about components,
supported by the interactive theorem prover
PVS.
We use this framework for a small example where
components make mutual assumptions about each other's
output.
pdf © Springer-Verlag