Formal Modeling and Verification of Cloud Elasticity with Maude and LTL - Archive ouverte HAL Access content directly
Book Sections Year : 2019

Formal Modeling and Verification of Cloud Elasticity with Maude and LTL

(1, 2) , (1) , (3)
1
2
3

Abstract

Elasticity allows Cloud systems to adapt to the demand by (de)provisioning resources as the input workload rises and drops. Given the numerous overlapping factors that impact their elastic behavior, the specification and verification of Cloud elasticity is a particularly challenging task. In this paper, we propose a Maude-based approach to formalize Cloud systems’ elastic behaviors, as a first step towards the verification of their correctness through a LTL (Linear Temporal Logic) state-based model-checking technique.
Not file

Dates and versions

hal-02417562 , version 1 (18-12-2019)

Identifiers

Cite

Khaled Khebbeb, Nabil Hameurlain, Faiza Belala. Formal Modeling and Verification of Cloud Elasticity with Maude and LTL. Attiogbé C., Ferrarotti F., Maabout S. (eds) New Trends in Model and Data Engineering. MEDI 2019. Communications in Computer and Information Science, vol 1085. Springer, Cham, pp.64-77, 2019, ⟨10.1007/978-3-030-32213-7_5⟩. ⟨hal-02417562⟩
67 View
0 Download

Altmetric

Share

Gmail Facebook Twitter LinkedIn More