Formal Verification of Replication on a Distributed Data Space Architecture

Jozef Hooman and Jaco van de Pol

Appeared in: Proceedings of the 17th ACM Symposium on Applied Computing (SAC 2002), Special Track on Coordination Models, pages 351-358, 2002.


We investigate the formal verification of safety-critical systems 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. We use two complementary formal tools: first the muCRL tool set 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. These formal techniques are used to investigate transparent replication of certain components on top of Splice. We prove that a convenient solution can be obtained by means of a slight extension of the write primitive of Splice.