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.
ABSTRACT
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.
Postscript