Challenges in formal methods for testing and verification of cloud computing systems

Formal methods are necessary to capture the semantics and behavior of processes of various systems. They characterize and provide insight into the behavior of real systems and thus identify their deterministic and non-deterministic features. The design and deployment of cloud computing systems utilize the current technology development in order to provide the appropriate service and accommodate the increasing demand while maintaining high quality and error free service. In this paper, we discuss the state of the art on using formal methods for the verification of cloud computing systems. Even though formal methods have been used successfully in the design and verification of several aspects of these systems, there are still many design issues in cloud computing that can be enhanced using formal methods. For instance, several scheduling algorithms are being used for cloud frameworks, such as Hadoop for instance, that are found to suffer from scheduling failures. This could have been avoided if the schedular has been properly verified. On the other hand, several new paradigms have evolved with cloud computing such as big data, these require fundamental changed on methods and algorithms that are being used for classical distributed systems, which in turn, increase the chance of having faulty systems that are difficult to highlight using only simulation methods.