Addressing Client Needs for Cloud Computing using Formal Foundations

TL;DR

This paper introduces a formal model for multi-cloud systems that uses Abstract State Machines and model checking to ensure reliability and adaptability in complex, heterogeneous cloud environments.

Contribution

It presents a novel formal framework for coordinating multi-cloud interactions through specification, validation, and verification using ASM and ASMETA tools.

Findings

Effective monitoring and adaptation processes improve system resilience.

Formal verification ensures system properties are maintained.

Simulation validates the model's correctness and robustness.

Abstract

Cloud-enabled large-scale distributed systems orchestrate resources and services from various providers in order to deliver high-quality software solutions to the end users. The space and structure created by such technological advancements are immense sources of information and impose a high complexity and heterogeneity, which might lead to unexpected failures. In this chapter, we present a model that coordinates the multi-cloud interaction through the specification, validation, and verification of a middle-ware exploiting monitoring and adaptation processes. The monitoring processes handle collecting meaningful data and assessing the state of components, while the adaptation processes restore the system as dictated by the evolution needs and sudden changes in the operating environment conditions. We employ Abstract State Machines to specify the models and we further make use of the ASMETA framework to simulate and validate them. Desired properties of the system are defined and analysed with the aid of the Computation Tree Logic.