Addressing Client Needs for Cloud Computing using Formal Foundations
This addresses reliability issues for users of multi-cloud distributed systems, though it appears incremental in applying existing formal methods to this domain.
The authors tackled the problem of unexpected failures in multi-cloud distributed systems by developing a middleware model that coordinates cloud interactions through specification, validation, and verification, using Abstract State Machines and Computation Tree Logic to ensure system reliability.
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.