The Modelling and Analysis of OceanStore Elements Using the CSP Dependability Library

  • William Simmonds
  • Tim Hawkins
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 3705)


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


Hash Function Data Item Semantic Model Bloom Filter Structural Induction 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Formal Systems (Europe) Limited, FDR User Manual and Tutorial,
  2. 2.
    FORWARD - A Future Of Reliable Wireless Ad-hoc networks of Roaming Devices,
  3. 3.
    Bloom, B.H.: Space/time trade-offs in hash coding with allowable errors. Communications of the ACM 13(7), 422–426 (1970)CrossRefzbMATHGoogle Scholar
  4. 4.
    Creese, S.: Data independent induction: CSP Model Checking of Arbitrary Sized Networks, D.Phil. Thesis, University of Oxford (2001)Google Scholar
  5. 5.
    Davies, J., Crichton, C.: Concurrency and Refinement in the Unified Modelling Langauge, Electronic Notes in Theoretical Computer Science 70(3) (2002)Google Scholar
  6. 6.
    Jones, C.B.: Tentative steps towards a development method for interfering programs. ACM Transactions on Programming Languages and Systems 5(4), 596–619 (1983)CrossRefzbMATHGoogle Scholar
  7. 7.
    Kay, A., Reed, J.N.: A rely and guarantee method for timed csp: A specification and design of a telephone exchange. IEEE Transactions in Software Engineering 19(6), 625–639 (1993)CrossRefGoogle Scholar
  8. 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. 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. 10.
    Lowe, G.: Casper: A compiler for the analysis of security protocols. In: 10th IEEE Computer Security Foundations Workshop (1997)Google Scholar
  11. 11.
    Misra, J., Chandy, K.M.: Proofs of networks of processes. IEEE Transactions in Software Engineering 7(4), 417–426 (1981)CrossRefMathSciNetGoogle Scholar
  12. 12.
    Ng, M.Y.: Towards formalizing uml state diagrams in csp. In: First 2003, pp. 138–147. IEEE, Los Alamitos (2003)Google Scholar
  13. 13.
    Rhea, S.C., Kubiatowicz, J.: Probabilistic location and routing. In: Proceedings of INFOCOM 2002 (2002)Google Scholar
  14. 14.
    Roscoe, A.W.: The Theory and Practice of Concurrency. Prentice-Hall, Englewood Cliffs (1997)Google Scholar
  15. 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. 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

Copyright information

© Springer-Verlag Berlin Heidelberg 2005

Authors and Affiliations

  • William Simmonds
    • 1
  • Tim Hawkins
    • 1
  1. 1.Trusted Information Management, QinetiQMalvernUK

Personalised recommendations