Article ID | Journal | Published Year | Pages | File Type |
---|---|---|---|---|
9657948 | Theoretical Computer Science | 2005 | 33 Pages |
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.
Related Topics
Physical Sciences and Engineering
Computer Science
Computational Theory and Mathematics
Authors
Jozef Hooman, Jaco van de Pol,