Formal Quality of Service assurances, ranking and verification of cloud deployment options with a probabilistic model checking method

Context: Existing software workbenches allow for the deployment of cloud applications across a variety of Infrastructure-as-a-Service (IaaS) providers. The expected workload, Quality of Service (QoS) and Non-Functional Requirements (NFRs) must be considered before an appropriate infrastructure is selected. However, this decision-making process is complex and time-consuming. Moreover, the software engineer needs assurances that the selected infrastructure will lead to an adequate QoS of the application. Objective: The goal is to develop a new method for selection of an optimal cloud deployment option, that is, an infrastructure and configuration for deployment and to verify that all hard and as many soft QoS requirements as possible will be met at runtime. Method: A new Formal QoS Assurances Method (FoQoSAM), which relies on stochastic Markov models is introduced to facilitate an automated decision-making process. For a given workload, it uses QoS monitoring data and a user-related metric in order to automatically generate a probabilistic model. The probabilistic model takes the form of a finite automaton. It is further used to produce a rank list of cloud deployment options. As a result, any of the cloud deployment options can be verified by applying a probabilistic model checking approach. Results: Testing was performed by ranking deployment options for two cloud applications, File Upload and Video-conferencing. The FoQoSAM method was compared to a baseline Analytic Hierarchy Process (AHP). The results show that the first ranked cloud deployment options satisfy all hard and at least one of the soft requirements for both methods, however, the FoQoSAM method always satisfies at least an additional QoS requirement compared to the baseline AHP method. Conclusions: The proposed new FoQoSAM method is appropriate and can be used in decision-making when ranking and verifying cloud deployment options. Due to its practical utility it was integrated into the SWITCH workbench.