The Modelling and Analysis of OceanStore Elements Using the CSP Dependability Library
- 232 Downloads
This paper reports on work undertaken for the FORWARD project on the formal verification of distributed data replication mechanisms using CSP and the CSP model checker FDR.
The Dependability Library is an evolving CSP framework and tool suite for aiding in the design, modelling and verification of fault-tolerant distributed systems; OceanStore is an architecture for a global-scale, persistent, distributed storage mechanism. In this paper, we describe the application of the Dependability Library to two algorithms used by OceanStore; some correctness results are obtained for these algorithms for small static networks.
CSP structural induction is a technique for enabling correctness results of algorithms to be proved for arbitrary large networks. Assumptiom-Commitment is a form of specification in which the specified behaviour of a system is split into the behaviour assumed of the system’s environment and the behaviour the system commits to as a result of that behaviour. We discuss ways in which the Dependability Library is affording support for these important techniques, and how they can be applied to extend the correctness results for the OceanStore algorithms to larger networks.
A software demonstrator of the OceanStore models using the new Dependability Library IDE will be made available on the Forward project website at www.forward-project.org.uk.
KeywordsHash Function Data Item Semantic Model Bloom Filter Structural Induction
Unable to display preview. Download preview PDF.
- 1.Formal Systems (Europe) Limited, FDR User Manual and Tutorial, http://www.fsel.com/
- 2.FORWARD - A Future Of Reliable Wireless Ad-hoc networks of Roaming Devices, http://www.forward-project.org.uk/
- 4.Creese, S.: Data independent induction: CSP Model Checking of Arbitrary Sized Networks, D.Phil. Thesis, University of Oxford (2001)Google Scholar
- 5.Davies, J., Crichton, C.: Concurrency and Refinement in the Unified Modelling Langauge, Electronic Notes in Theoretical Computer Science 70(3) (2002)Google Scholar
- 8.Kubiatowicz, J., Bindel, D., Chen, Y., Eaton, P., Geels, D., Gummadi, R., Rhea, S., Weatherspoon, H., Weimer, W., Wells, C., Zhao, B.: Oceanstore: An architecture for global-scale persistent storage. In: Proceedings of ACM ASPLOS, November 2000. ACM, New York (2000)Google Scholar
- 9.Kurshan, R.P., McMillan, K.: A structural induction theorem for processes. In: Proceedings of the 8th Symposium on Principles of Distributed Computation, Edmonton (1989)Google Scholar
- 10.Lowe, G.: Casper: A compiler for the analysis of security protocols. In: 10th IEEE Computer Security Foundations Workshop (1997)Google Scholar
- 12.Ng, M.Y.: Towards formalizing uml state diagrams in csp. In: First 2003, pp. 138–147. IEEE, Los Alamitos (2003)Google Scholar
- 13.Rhea, S.C., Kubiatowicz, J.: Probabilistic location and routing. In: Proceedings of INFOCOM 2002 (2002)Google Scholar
- 14.Roscoe, A.W.: The Theory and Practice of Concurrency. Prentice-Hall, Englewood Cliffs (1997)Google Scholar
- 15.Wolper, P., Lovinfosse, V.: Verifying properties of large sets of processes with network invariants (extended abstract). In: Sifakis, J. (ed.) CAV 1989. LNCS, vol. 407. Springer, Heidelberg (1990)Google Scholar
- 16.Woodcock, J.C.P., Cavalcanti, A.L.C.: The semantics of circus - a concurrent language for refinement. In: B 2002 and ZB (2002)Google Scholar