The Application Of Formal Methods In Cloud Computing

Cloud computing is an emerging business compute model; it will distribute the task inthe resource pool which is composed of a large number of computers. Cloud computing canmake users access computing power, storage space and software service on demand. It canalso provide good underlying architecture for Internet service providers, which can not onlywell solve the problem of resource shortage of hardware and bandwidth, but also greatlyreduce the fundamental hardware investment which services the users, reduce the cost, andgreatly improve the economic benefit.Cloud computing attracts a large number of service providers’ attention by the thoughtpattern of everything is service, and promote the rapid growth of type and quantity of servicein cloud environment. Cloud computing has brought new life style and experience for people,at the same time; it also brings new challenges which are caused by the characteristics ofcloud computing, such as dynamic, heterogeneous, autonomous, etc. Many problems arecaused by the service or resource description is unclear, the interaction of the service andenvironment is not clear. Formal methods is based on the mathematical theory, it is a methodof using mathematics on the basis of specification languages to formally describe andreasoning, and has been widely used in the field of computer science and softwareengineering. To promote the development of cloud computing, In this paper, the formalsemantics in cloud computing system are characterized by using formal methods, and basedon it, the problem of the analysis of the impact of changes in cloud computing and theproblem of data security evaluation are studied deeply, the main work is as follows:1) Characterize the formal semantics of cloud computing system by using AbstractSourceOntology is a knowledge representation method that describes the semantics bydepicting the relationship between entities, but ontolgies can only depict static relationship,nor dynamic change. On the basis of the idea of the introduction of dynamic semantics inontologies, this paper presents a new knowledge representation named Abstract Source. Someaspects of the Abstract Source such as definition, properties, semantic have been deeplyanalyzed; Based on the architecture and feature of cloud computing systems we extract thecommonness of cloud computing systems, using constructors and operators in the Abstract Source to characterize the commonality of cloud computing system; Analyzing the differencesbetween the cloud computing systems from the architecture approach and configuration, andmaking use of constructor refinement, operators refinement and the number of instancesrefinement to describe the properties of cloud computing systems. For example, SCSKPservice, illustrate how to describe the semantic of cloud computing system using AbstractSource. Abstract Source well describe the components and the running mechanism of cloudcomputing systems, providing favourable theoretical basis for the further promotion andpopularization of cloud computing.2) Analyze the impacts of "change" in cloud computing systemsA great deal of resources and service existed in cloud computing systems, which may beabnormal all the time, then affect the continuity and reliability of cloud services, but thepresent research still makes an unclear conclusion on how to quantify the effect of "change"in cloud computing systems. Based on the description of Abstract Source in cloud computingsystem, this paper makes a change transmit model with "change" information in cloudcomputing systems, and makes a definition of code CTMC which make this model berepresented formally. Based on the change transmit model and CTMC coding, this paperanalyzes the norm that embodies the effect the "change" in cloud computing system, andgives the method of these norms for calculation in change transmit model. Analyzing the formof the common "change" in the change transmit model in cloud computing systems, and theimpact analysis method of "change" is given; Through a representative example, how toanalyze the effect of "change" based on the change transmit model is illustrated. This methodcan analyze the effect of the "change" in cloud computing system accurately, and it willprovide a good theoretical support for the optimization of cloud service deployment strategiesand recovery mode.3) Describe cloud computing system using tabular expressions general modelTabular expression is a formal method which uses tabular form to define the functionsand relationships. To solve the problem that using Abstract Source to describe cloudcomputing systems is not intuitive and error-prone, this paper carries out several extensions oftabular expressions, puts forward to Association Table and Conditions Operating Table, andgives a method that using tabular expression in the medium of Abstract Source to describe thecloud computing systems. Use Association Table to describe the entities in Abstract Source ofcloud computing system such as constructor, operator, cases and the relationship betweenentities. Use formal function table to depict the behavior of the operator, use ConditionOperating Table to elaborate the operating effect of operation rules. The description of Abstract Source by tabular expression, making it more clearly and accurately to describeAbstract Source in cloud computing system, and it enhance the applicability of AbstractSource.4) Analyze and evaluate the security of the data in SCSKPThe essence of protecting the cloud security services is to protect the security of data inthe cloud. Cloud storage service is a special cloud service, if it’s possible to evaluate itssecurity, the evaluation method can be extended to the data security evaluation of generalcloud services. This paper studies the security evaluation problem by a special kind of cloudstorage service called SCSKP. We analyze the security protection ability based on the AbstractSource descriptions of SCSKP; Markov model can be used to analyze the possibilities that avariety of illegal invasion which may happen in the SCSKP; Use the results to calculate theloss expectations of the illegal invasion and to quantify the ability of the resistance to theillegal invasion; analyze the effectiveness of the proposed methods in this paper under variousconditions through simulation experiments. The experimental results show that this methodcan analyze the data security in SCSKP more accurately. This method will convert theproblem of security analysis of the data storage in cloud computing system to problem ofillegal invasion of loss expectation, reducing the complexity of the problem, providing atheoretical support for the establishment of the standard of the cloud service securityevaluation.In short, this paper fully takes the advantage of the formal methods, using formalmethods to do some research on cloud conmputing. In order to ensure successful deploymentof cloud services and efficient operation, we research the semantic description of cloudcomputing systems, analyze the impacts of "change" in cloud computing system, and evaluatethe security of the data in SCSKP. This study can provide reference for solving issues relatedto cloud computing, and promote the development of cloud computing to a certain extent.