A modeling language to describe massive data storage management in cyber-physical systems

Massive data storage systems (MDSS, for short) are elementary parts of data gathering and analysis in cyber-physical systems. MDSSs have more features than traditional storage systems. An important one is that data files are split and stored into blocks in MDSSs. And each block is considered as a storage unit. Hence, MDSSs usually have two kinds of storage units: ordinary memory locations and block storage locations. Then it comes the question that how we formally model and describe MDSSs. In this paper we propose a modeling language to describe the management programs in MDSSs. New expressions and commands are introduced which mainly focus on block operations. Their denotational semantics are defined using the concepts of heap and store. According fixed-point theorem is proved. Using this method, management programs of MDSSs can be expressed more clearly and intuitively, and it allows us to analyze MDSSs more easily.