Towards a Formal Verification Approach for Cloud Software Architecture

被引：0

作者：

Ayach, Amal ^{[1
]}

Sliman, Layth ^{[2
]}

Kmimech, Mourad ^{[3
]}

Bhiri, Mohamed Tahar ^{[4
]}

Raddaoui, Badran ^{[5
]}

机构：

[1] Fac Sci Monastir, Monastir, Tunisia

[2] Efrei Ecole Ingenieur Generaliste Informat, F-94800 Villejuif, France

[3] Univ Tunis El Manar, ENIT, UR OASIS, Tunis, Tunisia

[4] Pole Technol Sfax, Lab Miracl ISIMS, Sakiet Ezzit Sfax, Tunisia

[5] Univ Paris Saclay, CNRS, Telecom SudParis, SAMOVAR, Evry, France

来源：

NEW TRENDS IN INTELLIGENT SOFTWARE METHODOLOGIES, TOOLS AND TECHNIQUES | 2017年 / 297卷

关键词：

cloud computing; ADL; verification; behavior consistency; TOSCA;

D O I：

10.3233/978-1-61499-800-6-490

中图分类号：

TP18 [人工智能理论];

学科分类号：

081104 ; 0812 ; 0835 ; 1405 ;

摘要：

Behavioral consistency of cloud architectures is one of the pivotal challenges in cloud computing. In this paper, we propose a new approach for checking the behavioral consistency of the topology and orchestration of cloud computing. To do so, we choose TOSCA language in order to describe the cloud application. Then, we exploit the Wright ADL that encompasses the CSP language to check the consistency of cloud architectures using FDR2 model-checker.

引用

页码：490 / 502

页数：13

共 50 条

[31] Design and formal verification of a cloud compliant secure logging mechanism [J].

Sandikkaya, Mehmet Tahir ;

Ovatman, Tolga ;

Harmanci, Ali Emre .

IET INFORMATION SECURITY, 2016, 10 (04) :203-214

[32] Formal Verification of Cloud and Fog Systems: A Review and Research Challenges [J].

Fakhfakh, Fairouz ;

Kallel, Slim ;

Cheikhrouhou, Saoussen .

JOURNAL OF UNIVERSAL COMPUTER SCIENCE, 2021, 27 (04) :341-363

[33] Challenges in formal methods for testing and verification of cloud computing systems [J].

Gawanmeh, Amjad ;

Alomari, Ahmad .

Scalable Computing, 2015, 16 (03) :321-332

[34] Formal Verification of Cloud based Distributed System using UPPAAL [J].

Chaudhry, Yasar Ali Khalid ;

Hammed, Mustafa .

2019 INTERNATIONAL CONFERENCE ON INNOVATION AND INTELLIGENCE FOR INFORMATICS, COMPUTING, AND TECHNOLOGIES (3ICT), 2019,

[35] A formal method for analyzing software architecture models in SAM [J].

Yu, HQ ;

He, XD ;

Yi, D ;

Lian, M .

26TH ANNUAL INTERNATIONAL COMPUTER SOFTWARE AND APPLICATIONS CONFERENCE, PROCEEDINGS, 2002, :645-652

[36] Towards Compositional Reuse for Software Architecture [J].

Li Xiaojian ;

Zheng Ying .

2010 INTERNATIONAL COLLOQUIUM ON COMPUTING, COMMUNICATION, CONTROL, AND MANAGEMENT (CCCM2010), VOL II, 2010, :623-626

[37] Towards Compositional Reuse for Software Architecture [J].

Li Xiaojian ;

Zheng Ying .

AFFECTIVE COMPUTING AND INTELLIGENT INTERACTION, 2012, 137 :651-+

[38] ARMISTICE: Microarchitectural Leakage Modeling for Masked Software Formal Verification [J].

de Grandmaison, Arnaud ;

Heydemann, Karine ;

Meunier, Quentin L. .

IEEE TRANSACTIONS ON COMPUTER-AIDED DESIGN OF INTEGRATED CIRCUITS AND SYSTEMS, 2022, 41 (11) :3733-3744

[39] Hybrid cloud computing monitoring software architecture [J].

Aktas, Mehmet S. .

CONCURRENCY AND COMPUTATION-PRACTICE & EXPERIENCE, 2018, 30 (21)

[40] A Review on Formal Verification of Basic Algorithms in Time Triggered Architecture [J].

Sheena, N. ;

Joseph, Shelbi ;

Kumar, Suresh N. .

2018 INTERNATIONAL CONFERENCE ON CONTROL, POWER, COMMUNICATION AND COMPUTING TECHNOLOGIES (ICCPCCT), 2018, :352-355

← 1 2 3 4 5 →