Formal verification of replication on a distributed data space architecture
- 11 March 2002
- conference paper
- Published by Association for Computing Machinery (ACM)
- p. 351-358
- https://doi.org/10.1145/508791.508859
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 over-writing. We use two complementary formal tools: first the µCRL 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.Keywords
This publication has 6 references indexed in Scilit:
- Semantical aspects of an architecture for distributed embedded systemsPublished by Association for Computing Machinery (ACM) ,2000
- Comparing coordination models based on shared distributed replicated dataPublished by Association for Computing Machinery (ACM) ,1999
- Branching time and abstraction in bisimulation semanticsJournal of the ACM, 1996
- Formal verification for fault-tolerant architectures: prolegomena to the design of PVSIEEE Transactions on Software Engineering, 1995
- Control systems softwareIEEE Transactions on Automatic Control, 1993
- Algebra of communicating processes with abstractionTheoretical Computer Science, 1985