A Formal Framework for Cloud Systems

1. Introduction

Cloud computing is actually attracting more attention, as a promising model for delivering Information and Communication Technology (ICT) services via the generalization of service reuse to all computer resources. It involves dynamic and on demand provisioning of shared computing resources (Mell et al., 2011). The main principle behind this model is to offer computing, storage and software as a service attempting to reduce IT capital and operating expenditures. Hence, it promotes service availability, emphasizes resource reuse rationalization and provides opportunities for reducing software development costs. Although cloud computing scope is enlarging, it is accompanied with a concentration of risks and brought issues. On the other hand, cloud systems are becoming more and more complex, since large organizations have to manage increasingly heterogeneous cloud systems: hundreds of services, thousands of servers, hundreds of thousands of transactions, more and more users spread over the world, whether customers or suppliers. Consequently, there are still many obstacles slowing down cloud computing model adoption and growth. Many obstacles have been identified by Armbrust et al. (2009), we list in what follows the most significant ones for our work:

• •

  Bugs in Large-Scale Distributed Systems: It is difficult to anticipate and avoid bugs during system development, it is more difficult to find and fix them in a running system. Thus, proposing a model being sufficiently expressive while remaining reasonably analyzable is recognized as an ideal solution.

• •

  Service Availability and Quick Scalability: Availability of service is the degree to which a service is available upon customer demand; it is measured regarding customer’s perception of a service, i.e., customers’ frustration whenever their services are no more available, whereas performance failure is being caused by an unexpected higher number of customers’ demands. The opportunity is then to scale-up quickly as a response to customer’s demand.

Identifying runtime service bugs while maintaining service availability is a complicated task regarding cloud systems architecture and complexity. Since, they allow formal verification of complex software systems giving rise to high quality, more correct software compared to conventional design methods, “formal methods are an effective approach to ensure cloud systems reliability, by providing a high evaluation assurance level ‘EAL7’”; according to (ISO 15408).

To obtain formal executable and analyzable cloud models, we define a new theoretical framework for cloud systems. The proposed framework extends our previous works (Benzadri et al., 2013) and (Benzadri et al., 2014) that are also part of our contribution in this chapter.The presented framework is composed of three main stages (see Figure 1):

Figure 1.

A formal framework for cloud systems

• Step 1: Designing cloud architecture and its shape shifting using Bigraphical Reactive Systems; BRS for short, BRS are an elegant solution to model cloud computing architecture and its dynamics.

• Step 2: Obtaining Maude-based executable specifications, Maude language presents an excellent solution to implement the obtained cloud bigraphical model (proposed in Step 1).

• Step 3: Verifying some cloud systems inherent properties using a Maude-based model checker. Via a judicious coupling of BRS and Maude, dynamic cloud architectures are analyzed and verified.