Toward Formal Modeling and Verification of Resource Provisioning as a Service in Cloud

• Main Authors: Wenbo Zhou, Lei Liu, Shuai Lu, Peng Zhang
• Format: Article
• Language: English
• Published: IEEE 2019-01-01
• Series: IEEE Access
• Subjects: Clouds; resource provisioning; Web services; UPPAAL; formal verification
• Online Access: https://ieeexplore.ieee.org/document/8649630/

Cloud service provides a convenient pattern of delivery and management for the Internet-based resource sharing. Reliable resource provisioning is very important to the stability of cloud service systems. In order to guarantee the consistency of resource delivery in cloud service, we propose a method for modeling and verification of resource provisioning as a service in the cloud. First, the framework of resource provisioning as a service and the behaviors of its participants are presented. Then, client, service manager (including allocator, finish monitor, and time monitor), and resource service are modeled based on UPPAAL, respectively. Finally, we define some consistency properties that a service scenario needs to satisfy and formally verify whether our model satisfies these properties using the UPPAAL model checker. The results show that our model satisfies all the proposed properties, which demonstrates the rationality and trustworthiness of our model.