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 条

[21] Developing an ROV software control architecture: a formal specification approach
de Assis, Fabio Henrique
Takase, Fabio Kawaoka
Maruyama, Newton
Miyagi, Paulo Eigi
[J]. 38TH ANNUAL CONFERENCE ON IEEE INDUSTRIAL ELECTRONICS SOCIETY (IECON 2012), 2012, : 3107 - 3112
[22] Towards Formal Verification for Cyber-physically Agnostic Software: a Case Study
Drozdov, Dmitrii
Patil, Sandeep
Dubinin, Victor
Vyatkin, Valeriy
[J]. IECON 2017 - 43RD ANNUAL CONFERENCE OF THE IEEE INDUSTRIAL ELECTRONICS SOCIETY, 2017, : 5509 - 5514
[23] A component-based approach to verification and validation of formal software models
Desovski, Dejan
Cukic, Bojan
[J]. ARCHITECTING DEPENDABLE SYSTEMS IV, 2007, 4615 : 89 - +
[24] Formal verification of fault-tolerant software design: the CSP approach
Yeung, WL
Schneider, SA
[J]. MICROPROCESSORS AND MICROSYSTEMS, 2005, 29 (05) : 197 - 209
[25] ARCHVerifyr: An Embedded Software-Driven Approach for Architecture Verification
Grimm, Tomas
Lettnin, Djones
Huebner, Michael
[J]. 2018 IEEE COMPUTER SOCIETY ANNUAL SYMPOSIUM ON VLSI (ISVLSI), 2018, : 220 - 225
[26] A Verification-Based Approach to Evaluate Software Architecture Evolution
Li Bixin
Liao Li
Yu Ximeng
[J]. CHINESE JOURNAL OF ELECTRONICS, 2017, 26 (03) : 485 - 492
[27] BGG: A Graph Grammar Approach for Software Architecture Verification and Reconfiguration
Li, Chen
Huang, Linpeng
Chen, Luxi
Yu, Chengyuan
[J]. 2013 SEVENTH INTERNATIONAL CONFERENCE ON INNOVATIVE MOBILE AND INTERNET SERVICES IN UBIQUITOUS COMPUTING (IMIS 2013), 2013, : 291 - 298
[28] A Verification-Based Approach to Evaluate Software Architecture Evolution
LI Bixin
LIAO Li
YU Ximeng
[J]. Chinese Journal of Electronics, 2017, 26 (03) : 485 - 492
[29] Formal Verification of Avionics Software Products
Souyris, Jean
Wiels, Virginie
Delmas, David
Delseny, Herve
[J]. FM 2009: FORMAL METHODS, PROCEEDINGS, 2009, 5850 : 532 - +
[30] Formal Software Verification Measures Up
Greengard, Samuel
[J]. COMMUNICATIONS OF THE ACM, 2021, 64 (07) : 13 - 15

← 1 2 3 4 5 →