دانلود رایگان مقاله انگلیسی استدلال درباره سیستم های ذخیره سازی ابری - IEEE 2018

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.

5. Conclusion

In the paper, we have extended Separation Logic to verify the correctness of management programs in CSSs. The imperative language of Separation Logic is incorporated with block operations. Assertions in Separation Logic are extended to contain quantifiers over block variables and file variables. Hoare-style rules are proposed to reason about the CSSs. Using these methods, the partial correctness of cloud storage management can be verified. Future work will be done alone the following directions: (1) Consider more characteristics of CSSs, such as parallelism, (key,value) pairs and the relations between blocks and locations. (2) Investigate the expressiveness, decidability and model checking algorithms of assertions. (3) Work out the expressiveness and completeness of the specification rules above.