Research On Formal Modelling And Verification Methods Of Cloud Computing System

With the rapid development of science,technology and service,the innovative computing paradigm called “cloud computing” has been widely applied to resource management,market operation and social service.Based Internet and virtualization technologies,cloud computing provides users with on-demand and measured services,such as infrastructure,platform and software.Cloud computing system is a typical complex system with the characteristics of large scale,multiple layers and complex architecture,making it difficult to guarantee reliability and security.How to appropriately abstract,model and verify cloud computing systems to enhance trustworthiness and reliability,remains a vital problem to solve.This thesis investigates the correct-by-construction problems of cloud computing system using formal methods.Given a framework of cloud computing system,formal modelling,analysis and verification of its important components are performed by combining formal semantics,timed automata and coloured Petri nets.In this thesis,the focused cloud computing system consists of a data processing framework,a data storage system and a resource service system.The data processing framework defines the logic of data processing.The data storage system provides functions about data reading,writing and backuping.The resource service system ensures supply of relevant resources.Modelling and verification methods of these three components are investigated,and an attack tolerance framework is proposed to further improve reliability and security.The main contributions of this thesis are as follows.(1)In order to solve the formal semantic problems of data processing framework in cloud computing system,an execution semantic model called SDAC is proposed for analyzing data processing framework in cloud.In view that formal semantics can provide rigorous and normalized description of computational processes,which contributes to proving and analysing the correctness of programs or systems,this thesis defines distributed abstract configuration and execution semantics by combining formal semantic theories.A comparison between configurations in SDAC and Aeolus is carried out.The rationality and validity of SDAC are demonstrated through a Map Reduce case description and analysis of fault tolerance and performance optimization.(2)In order to solve the modelling and verification problems of data storage system in cloud computing system,a model called MSCDSS-RP for analysis of master-slave cloud data storage systems with replication pipeline is proposed.Since coloured Petri net(CPN)is suitable for modelling and verifying concurrent systems,enabling accurate description of concurrently read,write and message passing with the help of typed tokens and their changes,this thesis uses CPNs to model reading and writing processes among client,meta-server and cluster.The state space is analyzed in CPN Tools and some important properties such as replication consistency are verified.(3)In order to solve the modelling and verification problems of resource provisioning service in cloud computing system,a modelling and verification method for resource provisioning as a service is proposed.With the good expressiveness in describing state and time,timed automata can capture state synchronization and time controlling in service processes.This thesis uses timed automata to present a framework for resource provisioning as a service and its participants' behaviours.Client,service management center(including allocator,termination monitor and time monitor)and resource service are modelled,and the timed automata tool UPPAAL is used to verify consistency properties in relevant service scenarios.(4)In order to solve the attack tolerance problems in cloud computing system,a coloured Petri net based attack tolerance framework is proposed.Coloured Petri net has both a rigorous mathematical basis and an intuitive visual graphical representation,which is suitable for diagnosis and analysis of asynchronous and concurrent processes.This thesis uses coloured Petri net to abstract and model basic attack-network interaction patterns,attack detectors and tolerance solutions.According to the identification information of attack detectors,a tolerance solution would be generated by compositing basic tolerance solutions.Finally,the usability and effectiveness of the method are illustrated through a case study about cloud-based medical information storage.In summary,this thesis systematically investigates data processing framework,data storage system,resource service system and attack tolerance mechanism in cloud computing systems,and explores methods for their related system semantics,process modelling and property verification using a variety of formal theories and tools such as those for formal semantics,timed automata and coloured Petri nets.This work can provide a reference for the application of formal methods to cloud computing system and facilitate research on combining formal means to improve trustworthiness,reliability and security of complex systems.