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 条
  • [1] Towards a Formal Verification Approach for Service Component Architecture
    Chargui, Wael
    Rouis, Taoufik Sakka
    Kmimech, Mourad
    Bhiri, Mohamed Tahar
    Sliman, Layth
    Raddaoui, Badran
    NEW TRENDS IN INTELLIGENT SOFTWARE METHODOLOGIES, TOOLS AND TECHNIQUES, 2017, 297 : 466 - 479
  • [2] Towards a Formal Approach for the Verification of SCA/BPEL Software Architectures
    Taoufik, Sakka Rouis
    Tahar, Bhiri Mohamed
    Layth, Sliman
    Mourad, Kmimech
    2017 8TH INTERNATIONAL CONFERENCE ON INFORMATION, INTELLIGENCE, SYSTEMS & APPLICATIONS (IISA), 2017, : 487 - 492
  • [3] A Formal Approach for Cloud Composite Services Verification
    Lahouij, Aida
    Hamel, Lazhar
    Graiet, Mohamed
    El Malki, Mohammed
    2018 IEEE 11TH CONFERENCE ON SERVICE-ORIENTED COMPUTING AND APPLICATIONS (SOCA), 2018, : 161 - 168
  • [4] Software Architecture for the Cloud A Roadmap Towards Control-Theoretic, Model-Based Cloud Architecture
    Pahl, Claus
    Jamshidi, Pooyan
    SOFTWARE ARCHITECTURE (ECSA 2015), 2015, 9278 : 212 - 220
  • [5] Formal Verification of Avionics Software Products
    Souyris, Jean
    Wiels, Virginie
    Delmas, David
    Delseny, Herve
    FM 2009: FORMAL METHODS, PROCEEDINGS, 2009, 5850 : 532 - +
  • [6] Towards Formal Verification of Program Obfuscation
    Lu, Weiyun
    Sistany, Bahman
    Felty, Amy
    Scott, Philip
    2020 IEEE EUROPEAN SYMPOSIUM ON SECURITY AND PRIVACY WORKSHOPS (EUROS&PW 2020), 2020, : 635 - 644
  • [7] Migrating legacy software to the cloud: approach and verification by means of two medical software use cases
    Maenhaut, Pieter-Jan
    Moens, Hendrik
    Ongenae, Veerle
    De Turck, Filip
    SOFTWARE-PRACTICE & EXPERIENCE, 2016, 46 (01) : 31 - 54
  • [8] Behavioral Verification of UML2.0 Software Architecture
    Taoufik, Sakka Rouis
    Tahar, Bhiri Mohamed
    Mourad, Kmimech
    PROCEEDINGS OF 2016 12TH INTERNATIONAL CONFERENCE ON SEMANTICS, KNOWLEDGE AND GRIDS (SKG), 2016, : 115 - 120
  • [9] A formal approach for the correct deployment of cloud applications
    Mammar, Amel
    Belguidoum, Meriem
    Hiba, Saddam Hocine
    SCIENCE OF COMPUTER PROGRAMMING, 2024, 232
  • [10] A formal approach for the specification and verification of a Trustworthy Human Resource Discovery mechanism in the Expert Cloud
    Navimipour, Nima Jafari
    EXPERT SYSTEMS WITH APPLICATIONS, 2015, 42 (15-16) : 6112 - 6131