Formal verification approaches and standards in the cloud computing: A comprehensive and systematic review

Cloud computing as a new internet-based computing model provides different resources as a service dynamically. Today, cloud computing is actually one of the main improvements in the computing procedure. However, by raising user interactions, the complexity of cloud processes is increasing with the advancement of technology. To evaluate the cloud computing challenges, the simulation experiments just satisfy the non-functional properties with a limited majority in forms of QoS factors. In addition, using simulation approaches have not been sufficient for developed complex cloud services that omit some critical test cases in the state space of the model. On the other hand, formal verification is an essential section in the complex information systems development that satisfies both functional and non-functional properties. Therefore, it is essential that the cloud systems use formal verification approaches for increasing the correctness of the system quality in all of the state space of the model. Despite the importance of the formal verification approaches in the cloud environments, to the best of our knowledge, there is not any systematic, comprehensive and detailed survey and review in the field of formal verification approaches and standards in the cloud computing. This paper provides a Systematic Literature Review (SLR) method to examine the current technical studies (published between 2011 and July 2017) in formal verification of the cloud computing. Also, this paper categorizes the formal verification approaches in three classic fields: specification and process algebra, model checking, and theorem proving. The verification approaches are compared with each other according to some technical properties such as specification methods, modeling approaches, verification tools and verification methods. The advantages and disadvantages of each selected study as well as some hints are discussed for solving their problems. The brief contributions of this paper are as follows: (1) providing a comprehensive literature review of the formal verification approaches in the cloud computing, (2) designing a technical taxonomy for the verification approaches in various modeling and specification methods, (3) presenting a technical analysis and comparison for the main challenges of the formal verification in the cloud and (4) highlighting the future open issues in the recent topics.