Wang, Hanpin

Title: Logic for Reasoning about Cloud Storage Systems

Abstract: Cloud storage devices are elementary parts in many cloud computing systems. Cloud Storage Systems (CSS) have more features than traditional storage systems. An important one is that data are stored in blocks in CSSs. 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 presentation, 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.