A Formal Approach for QoS Assurance in the Cloud

Cloud computing is an attractive business model offering cost-efficiency and business agility. Recently, the trend is that small and large businesses are moving their services to cloud environments. The quality of service is always negotiated between the cloud users and the cloud providers and documented in the service level agreement (SLA). Yet assuring -- or even measuring -- the quality of the provided service can be challenging. This paper proposes a formal approach for quantifying the quality of service in the cloud systems as promised in the SLA. The proposed approach uses controller synthesis to find a system configuration that meets the SLA requirement. The formal approach suggested in this paper is based on, but not limited to, %the controller synthesis of Time Petri Nets (TPN). As a case study, we focus on service availability as a key performance indicator in the SLA and for a sample set of resources providing a service, we determine the system configuration satisfying the SLA.