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.


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.