A Maude-Based rewriting approach to model and verify Cloud/Fog self-adaptation and orchestration
Autor: | Faiza Belala, Khaled Khebbeb, Nabil Hameurlain |
---|---|
Přispěvatelé: | Laboratoire Informatique de l'Université de Pau et des Pays de l'Adour (LIUPPA), Université de Pau et des Pays de l'Adour (UPPA), Université de Constantine 2 Abdelhamid Mehri [Constantine], Laboratoire d'Informatique Répartie [Algérie] (LIRE) |
Rok vydání: | 2020 |
Předmět: |
Correctness
Computer science Distributed computing Cloud computing [INFO.INFO-SE]Computer Science [cs]/Software Engineering [cs.SE] 01 natural sciences [INFO.INFO-FL]Computer Science [cs]/Formal Languages and Automata Theory [cs.FL] Linear temporal logic Formal specification 0103 physical sciences [INFO]Computer Science [cs] 0601 history and archaeology Orchestration (computing) 010302 applied physics 060102 archaeology business.industry Control reconfiguration 06 humanities and the arts computer.file_format [INFO.INFO-MO]Computer Science [cs]/Modeling and Simulation Hardware and Architecture Rewriting Executable business computer Software |
Zdroj: | Journal of Systems Architecture Journal of Systems Architecture, Elsevier, 2020, pp.101821. ⟨10.1016/j.sysarc.2020.101821⟩ |
ISSN: | 1383-7621 |
DOI: | 10.1016/j.sysarc.2020.101821 |
Popis: | International audience; In the IoT-Fog-Cloud landscape, IoT devices are connected to numerous software applications in order to fully operate. Some applications are deployed on the Fog layer, providing low-latency access to resource, whilst others are deployed on the Cloud to provide important resource capabilities and process heavy computation. In this distributed landscape, the deployment infrastructure has to adapt to the highly dynamic requirements of the IoT layer. However, due to their intrinsic properties, the Fog layer may lack of providing sufficient amount of resource while the Cloud layer fails ensuring low-latency requirements. In this paper, we present a rewriting-based approach to design and verify the Cloud-Fog self-adaption and orchestration behaviors in order to manage infrastructure reconfiguration towards achieving low-latency and resources quantity trade-offs. We rely of the formal specification language Maude to provide an executable solution of these behaviors basing on the rewriting logic and we express properties with linear temporal logic (LTL) to qualitatively verify the adaptations correctness.KeywordsSelf-adaptation; Orchestration; Fog computing; Cloud computing; Formal methods; Rewriting logic; Linear Temporal Logic; Maude |
Databáze: | OpenAIRE |
Externí odkaz: |