Abstract
The rapid growth of data has restricted the capability of traditional storage technologies to store and manage data. Massive growth in big data generated through cloud storage systems (CSSs) has been observed. An important feature of CSSs is that data are stored in blocks, and each block is considered as a storage unit. Hence, CSSs usually have two kinds of storage units: ordinary locations and block locations. It makes CSSs very different from ordinary storage systems. Then how do we appeal formal methods to model, describe and reason about CSSs? In this paper, based on Separation Logic, we propose a systematic method to verify the correctness of management programs in CSSs. The main contributions are as follows. (1) A language is introduced to describe the cloud storage management. (2) Assertions in Separation Logic are extended to describe the properties of blocks in CSSs. (3) Hoare-style rules are proposed to reason about the CSSs. Pre- and post-conditions are pairs of assertions. Using these methods, the partial correctness of cloud storage management can be verified.
