The modelling and analysis of OceanStore elements using the CSP Dependability Library

Abstract

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 FOR. 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. © Springer-Verlag Berlin Heidelberg 2005.