Next-generation datacenters (DCs) built on virtualization technologies are pivotal to the effective implementation of the cloud computing paradigm. To deliver the necessary services and quality of service, cloud DCs face major reliability and robustness challenges.

Virtualization is a key aspect to achieve scalability and flexibility in a cloud. Many solutions have been proposed to monitor and deploy Virtual Machines (VM) in resource pool of cloud. However, most of the cloud management systems, such as Amazon EC2 are proprietary. In the said perspective, many open source VM-based platforms have tossed for general users to research. The existing work has mainly focused on the discussion of architecture, feature-set, and performance analysis. Other important aspects, such as formal analysis, modeling, and verification are usually ignored. In this paper, we provide formal analysis, modeling, and verification of three open source state-of-the-art VM-based cloud platforms: (a) Eucalyptus, (b) Open Nebula, and (c) Nimbus. We used High-Level Petri Nets (HLPN) to model and analyze the structural and behavioral properties of the systems. Moreover, to verify the models, we have used Satisfiability Modulo Theories Library (SMT-Lib) and Z3 Solver. We modeled about 100 VM to verify the correctness and feasibility of our models. The results reveal that the models are functioning correctly. Moreover, the increase in the number of VM does not affect the working of the models that indicates the practicability of the models in a highly scalable and flexible environment.