Verifying Replication on a Distributed Shared Data Space with Time Stamps
Jozef Hooman and
Jaco van de Pol
Appeared in: Proceedings of the
2nd workshop on Embedded Systems, PROGRESS 2001,
F. Karelse (Ed.),
pages 107-121, 2001.
ABSTRACT
We investigate transparent replication of components on top of the
distributed data space architecture Splice. In Splice each component
has its own local data space which can be kept small using keys, time
stamps and selective overwriting. Since Splice applications are often
safety-critical, we use two complementary formal tools to ensure
correctness: the muCRL tool set is used for a rapid investigation
of alternatives by a limited verification with state space exploration
techniques; next the most promising solutions are verified in general
by means of the interactive theorem prover of
PVS. With these formal
techniques we showed that replication of transformation components can
be achieved using sequence numbers. We also prove the correctness of a
nicer, more transparent solution which requires a slight extension of
the write primitive of Splice.
Postscript