Modeling and performance analysis of resource provisioning in cloud computing using probabilistic model checking