A Formal Framework for Cloud Systems

A Formal Framework for Cloud Systems

Zakaria Benzadri (University of Constantine 2, Algeria), Chafia Bouanaka (University of Constantine 2, Algeria) and Faïza Belala (University of Constantine 2, Algeria)
DOI: 10.4018/978-1-4666-9466-8.ch021
OnDemand PDF Download:
List Price: $37.50


Cloud Computing is an emerging topic with high potentials in the IT industry. Its offered services need to be adapted to deal with variations caused by hostile environment, such as the Internet. Hence, a challenging issue in Cloud systems architecture is to model and analyze cloud-based services. However, few work has been dedicated to guarantee safe and secure adaptable services. The main objective of this chapter is to propose a formal framework for specifying cloud systems and offering analysis support to model-check their inherent properties. Based on Bigraphical Reactive Systems, the formalization process is achieved via the definition of the BiCloud-Arch model. Then, cloud architecture dynamics is formalized by a set of generic reaction rules to be applied on the obtained bigraphical model. This chapter also addresses a mapping from the proposed model (BiCloud-Arch) to a Maude-based formal executable specification (BiCloud-2M). On this basis, the proposed BiCloud Maude-based Model Checker (BMMC) is used to formally verify some Cloud system properties.
Chapter Preview

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.

Complete Chapter List

Search this Book: