Probabilistic Model Checking at Runtime for the Provisioning of Cloud Resources

Abstract. We elaborate on the ingredients of a model-driven approach for the dynamic provisioning of cloud resources in an autonomic man-ner. Our solution has been experimentally evaluated using a NoSQL database cluster running on a cloud infrastructure. In contrast to other techniques, which work on a best-effort basis, we can provide probabilis-tic guarantees for the provision of sufficient resources. Our approach is based on the probabilistic model checking of Markov Decision Processes (MDPs) at runtime. We present: (i) the specification of an appropriate MDP model for the provisioning of cloud resources, (ii) the generation of a parametric model with system-specific parameters, (iii) the dynamic instantiation of MDPs at runtime based on logged and current measure-ments and (iv) their verification using the PRISM model checker for the provisioning/deprovisioning of cloud resources to meet the set goals1.