Corresponding author: Fairouz Fakhfakh ( fairouz.fakhfakh@gmail.com ) Corresponding author: Slim Kallel ( slim.kallel@gmail.com ) Corresponding author: Saoussen Cheikhrouhou ( saoussen.cheikhrouhou@gmail.com ) © Fairouz Fakhfakh, Slim Kallel, Saoussen Cheikhrouhou. This is an open access article distributed under the terms of the Creative Commons Attribution License (CC BY-ND 4.0). This license allows reusers to copy and distribute the material in any medium or format in unadapted form only, and only so long as attribution is given to the creator. The license allows for commercial use. Citation:
Fakhfakh F, Kallel S, Cheikhrouhou S (2021) Formal Verification of Cloud and Fog Systems:A Review and Research Challenges. JUCS - Journal of Universal Computer Science 27(4): 341-363. https://doi.org/10.3897/jucs.66455 |
Cloud and Fog computing have been widely recognized as attractive solutions in both academic and industrial sectors. Despite their benefits, the adoption of Cloud and Fog computing still have considerable challenges to be handled due to the increase of client requirements. A crucial issue, in this context, is how to verify the correctness of Cloud and Fog systems. The use of formal methods is an efficient mean which provides a real help for the designer to evaluate the behaviour of a system and prevent errors before its implementation. In this paper, we present a systematic literature review (SLR) on the current state of the art in this field. We collect the existing studies on the use of formal methods for proving the correctness of Cloud and Fog systems. The proposed approaches are compared based on some technical properties such as the verification methods, the verification tools, the considered properties, and the application domains. In addition, future directions which need more investigations are presented. We believe that our paper will be useful for industry and academic researchers to understand the existing contributions that deal with the cor- rectness of Cloud and Fog systems. Moreover, it helps them to address several gaps in the literature.