Formal Verification of Cloud and Fog Systems: A Review and Research Challenges

被引:3
作者
Fakhfakh, Fairouz [1 ]
Kallel, Slim [1 ]
Cheikhrouhou, Saoussen [1 ]
机构
[1] Univ Sfax, ReDCAD, Sfax, Tunisia
关键词
Formal verification; Cloud computing; Fog computing; Systematic literature review; Future directions; TEMPORAL LOGIC; SECURE; DEPLOYMENT; ENERGY; MODEL; IOT;
D O I
10.3897/jucs.66455
中图分类号
TP31 [计算机软件];
学科分类号
081202 ; 0835 ;
摘要
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.
引用
收藏
页码:341 / 363
页数:23
相关论文
共 102 条
[1]   Rodin: An open toolset for modelling and reasoning in Event-B [J].
Abrial J.-R. ;
Butler M. ;
Hallerstede S. ;
Hoang T.S. ;
Mehta F. ;
Voisin L. .
International Journal on Software Tools for Technology Transfer, 2010, 12 (06) :447-466
[2]  
Abrial J.-R., 2010, Modeling in Event-B: System and Software Engineering
[3]   A Cross Tenant Access Control (CTAC) Model for Cloud Computing: Formal Specification and Verification [J].
Alam, Quratulain ;
Malik, Saif U. R. ;
Akhunzada, Adnan ;
Choo, Kim-Kwang Raymond ;
Tabbasum, Saher ;
Alam, Masoom .
IEEE TRANSACTIONS ON INFORMATION FORENSICS AND SECURITY, 2017, 12 (06) :1259-1268
[4]   A THEORY OF TIMED AUTOMATA [J].
ALUR, R ;
DILL, DL .
THEORETICAL COMPUTER SCIENCE, 1994, 126 (02) :183-235
[5]   Improving security in cloud by formal modeling of IaaS resources [J].
Amato, Flora ;
Moscato, Francesco ;
Moscato, Vincenzo ;
Colace, Francesco .
FUTURE GENERATION COMPUTER SYSTEMS-THE INTERNATIONAL JOURNAL OF ESCIENCE, 2018, 87 :754-764
[6]   Formal Modeling and Evaluation of Service-based Business Process Elasticity in the Cloud [J].
Amziani, Mourad ;
Melliti, Tarek ;
Tata, Samir .
2013 IEEE 22ND INTERNATIONAL WORKSHOP ON ENABLING TECHNOLOGIES: INFRASTRUCTURE FOR COLLABORATIVE ENTERPRISES (WETICE), 2013, :284-291
[7]  
[Anonymous], 2019, SEFM 2019
[8]  
[Anonymous], 1976, PETRI NET LANGUAGE
[9]   A View of Cloud Computing [J].
Armbrust, Michael ;
Fox, Armando ;
Griffith, Rean ;
Joseph, Anthony D. ;
Katz, Randy ;
Konwinski, Andy ;
Lee, Gunho ;
Patterson, David ;
Rabkin, Ariel ;
Stoica, Ion ;
Zaharia, Matei .
COMMUNICATIONS OF THE ACM, 2010, 53 (04) :50-58
[10]   Linear Temporal Logic LTL: Basis for Admissible Rules [J].
Babenyshev, Sergey ;
Rybakov, Vladimir .
JOURNAL OF LOGIC AND COMPUTATION, 2011, 21 (02) :157-177