Cloud computing has become the leading paradigm for deploying large-scale infrastructures and running big data applications, due to its capacity of achieving economies of scale. In this work, we focus on one of the most prominent advantages of cloud computing, namely the on-demand resource provisioning, which is commonly referred to as elasticity. Although a lot of effort has been invested in developing systems and mechanisms that enable elasticity, the elasticity decision policies tend to be designed without guaranteeing or quantifying the quality of their operation. This work aims to make the development of elasticity policies more formalized and dependable. We make two distinct contributions. First, we propose an extensible approach to enforcing elasticity through the dynamic instantiation and online quantitative verification of Markov Decision Processes (MDP) using probabilistic model checking. Second, we propose concrete elasticity models and related elasticity policies. We evaluate our decision policies using both real and synthetic datasets in clusters of NoSQL databases. According to the experimental results, our approach improves upon the state-of-the-art in significantly increasing user-defined utility values and decreasing user-defined threshold violations.
Our work also relates to proposals that employ model checking for cloud solutions and runtime quantitative verification. In the work of @cite_26 , a technique to predict the minimum VM cost of cloud deployments based on existing application logs is introduced. Queuing network theory is used to derive VM resource usage profiles. With the the latter, MDP models are instantiated and used to verify system properties. The work of @cite_3 presents an incremental model verification technique, which is applied on component-based software systems deployed on cloud infrastructures. Their technique achieves lower verification time as only the modified components are verified. Both these techniques are used to analyze the cloud-based systems and not to drive elasticity or other adaptivity decisions. QoSMOS @cite_14 is a framework that also utilizes PRISM to analyse and dynamically choose the appropriate configuration of service-based systems modelled as Markov chains. Finally, the work in @cite_18 introduces a model-driven framework called ADAM, where the users provide activity diagrams that are converted to MDP models, for which cumulative rewards for various quality metrics are computed.
@cite_14 @cite_18 @cite_26 @cite_3
2146044140 2144780749 2125217134
Service-based systems that are dynamically composed at runtime to provide complex, adaptive functionality are currently one of the main development paradigms in software engineering. However, the Quality of Service (QoS) delivered by these systems remains an important concern, and needs to be managed in an equally adaptive and predictable way. To address this need, we introduce a novel, tool-supported framework for the development of adaptive service-based systems called QoSMOS (QoS Management and Optimization of Service-based systems). QoSMOS can be used to develop service-based systems that achieve their QoS requirements through dynamically adapting to changes in the system state, environment, and workload. QoSMOS service-based systems translate high-level QoS requirements specified by their administrators into probabilistic temporal logic formulae, which are then formally and automatically analyzed to identify and enforce optimal system configurations. The QoSMOS self-adaptation mechanism can handle reliability and performance-related QoS requirements, and can be integrated into newly developed solutions or legacy systems. The effectiveness and scalability of the approach are validated using simulations and a set of experiments based on an implementation of an adaptive service-based system for remote medical assistance. Modern software systems are often characterized by uncertainty and changes in the environment in which they are embedded. Hence, they must be designed as adaptive systems. We propose a framework that supports adaptation to non-functional manifestations of uncertainty. Our framework allows engineers to derive, from an initial model of the system, a finite state automaton augmented with probabilities. The system is then executed by an interpreter that navigates the automaton and invokes the component implementations associated to the states it traverses. The interpreter adapts the execution by choosing among alternative possible paths of the automaton in order to maximize the system's ability to meet its non-functional requirements. To demonstrate the adaptation capabilities of the proposed approach we implemented an adaptive application inspired by an existing worldwide distributed mobile application and we discussed several adaptation scenarios. Numerous organisations are considering moving at least some of their existing applications to the cloud. A key motivating factor for this fast-paced adoption of cloud is the expectation of cost savings. Estimating what these cost savings might be requires comparing the known cost of running an application in-house with a predicted cost of its cloud deployment. A major problem with this approach is the lack of suitable techniques for predicting the cost of the virtual machines (VMs) that a cloud-deployed application requires in order to achieve a given service-level agreement. We introduce a technique that addresses this problem by using established results from queueing network theory to predict the minimum VM cost of cloud deployments starting from existing application logs. We describe how this formal technique can be used to predict the cost-performance trade-offs available for the cloud deployment of an application, and presents a case study based on a real-world webmail service.