Cloud computing is a promising concept in the IT evolution that has increasingly attracted attention from both industry and academic sectors. However, it has introduced new security problems and obstacles. Since formal methods provide a reliable mathematical basis giving rise to safely analysable and easily verifiable models, we aim in this paper to propose a formal framework to specify cloud system architectures and verify their inherent proprieties. Bigraphical Reactive Systems are adopted as a semantic framework for their graphical aspect and rigorous basis. We argue that the proposed models are useful for simulation and analysis of cloud systems proprieties as elasticity and plasticity, while using a given model checker tool dedicated to BRS.
In recent years, cloud computing
Cloud service availability introduces a very
important concept that distinguishes cloud
computing paradigm from the other ones, which is
rapid elasticity
Bigraphs
We argue that Milner’s BRS, through their graphical aspect, are capable of representing both locality and connectivity that constitute main concepts of cloud computing architecture.
We propose a bigraph-based model for cloud system composed of two independent regions (physical or logical). For instance, the client and service provider may represent these regions. Then, interactions between these two regions are defined via reaction rules. Since BRS have an executable algebraic language, the obtained formal model serves to modelcheck some proprieties that are inherent to cloud systems as the elasticity and some forms of its violation (plasticity). The rest of the paper is organised as follows. In section 2, we present related work. In section 3, we give a brief overview on Bigraphical Reactive Systems (BRS) and their dedicated model checker. Section 4 presents our bigraphical specification of cloud systems. In, section 5 we formally verify the elasticity and plasticity proprieties. Finally, some concluding remarks and ongoing work rounds up the paper.
There is a significant body of work on defining and
analysing cloud systems, but we are unaware of
approaches involving formal and rigorous
mathematical models. For instance, authors in
Formal models for managing the complexity of
evolving cloud system behaviour while it is executing
is a recent area of interest. Existing approaches in
this context are based on various formalisms.
While our adopted formalism (BRS) is different and
more appropriate, our work has a similar goal in that
it is reasoning about cloud systems. We note a
related bigraphical modelling approach taken on by
Bigraphical reactive systems (BRS) were initially
introduced by
A bigraph is the combination of two independent
structures: the place and link graphs. The place
graph represents system entities geographical
distribution. The Link graph is a hypergraph
representing interconnections between these
entities. Within a BRS, system entities are
represented by nodes and interactions between
them are represented by edges (see Figure 1).
A node can be dotted with ports representing
connection points to edges or inner/outer names. A
control is also associated to each node; consisting
of node type identifier that belongs to a set called
signature. Each control indicates the number of
ports of each node (i.e. arity), which controls are
atomic for empty nodes and which of the non-atomic
controls are active (i.e. subject to reactions) or
passive. The inner/outer names of a bigraph indicate
connectors to other elements. Such interconnection
is only possible if the outer name of a bigraph or root
corresponds to the inner name of another bigraph.
Sites represent holes into which a root or node can
be nested, they are considered as an abstraction
indicating the presence of other elements.
Definition
, ): → , = < , >, =< = (, , , , >,where:
V and E represent finite sets of nodes and edges respectively. ∶ → is a control map that assigns a control to each node. The signature K is a set of controls. are Place and Link graphs respectively.
I and J represent inner and outer names (interfaces) respectively, of the bigraph G. m and n are the number of sites and roots respectively.
In addition to the graphical representation, a term algebraic language is defined to specify bigraphs, language primary operations and elements are summarized in Table 1.
Bigraphs structural dynamics is expressed via reaction rules; each one defines a redex bigraph to be transformed to a reactum one.
As an example, Figure 2 represents a reaction rule that allows a person P in the same root, as a room R, to leave the room. This rule is purely a placing reconfiguration. A linking reconfiguration represents any possible connectivity; reaction rule of Figure 3 represents a person P connecting to a pc in the same root through the edge e0.
Formally, a reaction rule takes the form (R,R',η)
where R:m⟶J is a redex, R':m'⟶J is a reactum and
η:m⟶m′ is a map of ordinals
Few tools for verifying BRS-based distributed
systems inherent properties exist as BigMC
BigMC (Bigraphical Model Checker) is a modelchecker designed to operate on Bigraphical Reactive Systems, where model checking is accomplished through an exhaustive search of all possible states of the bigraphical model that satisfy the property to be verified.
One of the main benefits of a model checking
approach is the ability to provide a counter-example
whenever the desired property does not hold in the
actual system model. In our case, this means
showing system configuration that violates the
specified property, and the transition system path by
which this configuration was reached. The full
grammar of BigMC bigraph terms is summarized in
Table 2
We will use this grammar to specify our cloud model. Then, we will use the BigMC tool to verify some of the cloud system proprieties.
At a high level of abstraction, a cloud computing system is considered as a set of computing resources (e.g. data centers, servers, services) that are distributed across multiple computing sites, and are often referred to as nodes. These resources are provided as on demand services that users (clients) can consume. Thus, two types of entities are identified in cloud computing: the front-end entity and the back-end entity that are interacting via the Internet.
The front-end represents the client interface, used to access the cloud. Clients are classified into two kinds: end users (i.e. simple cloud service consumers) and developers (i.e., costumers exploiting cloud as for Google Apps, Codeita to host their applications).
The back-end is the cloud service provider. It offers a complete system for allocating the required resources to execute user applications and managing the entire system flow.
Many types of resources can exist in a cloud as:
gather cloud computing resources and components.
Load balancers: devices responsible of service requests rooting and resources provision.
Servers: infrastructures for calculation and execution.
Virtual machines (VMs): abstractions of the underlying infrastructure.
Example 1: In order to ease the understanding of our proposed cloud system formalisation, we will first introduce the following generic example illustrating important features that will be considered.
The cloud system is composed of a unique instance of the following cloud components (data center, load balancer, server and virtual machine) and offers two different services for the end users (end user 1, end user 2, end user 3).
In a previous work
Assuming that the two services are deployed in the same virtual machine and an end user is connected to the first service while the others are connected to the second service. The corresponding bigraphical model is shown in Figure 5.
As we can notice in Figure 5, there are two services actually deployed in the virtual machine VM1 and two end users connected to S2 service through the edge e3. Thus, the S2 service cannot be allocated to another end user and the virtual machine VM1 cannot deploy any other service instance. This is expressed in our model by the absence of a site in that virtual machine.
The signature associated to a cloud bigraph is as follows: K = {L: (0, active), N :( 2, atomic)}, L and N represent controls associated to different nodes. The different nodes types used in the model and their associated controls are summarized in Table 4. The cloud system initial configuration expression in BigMC tool appropriate grammar is shown in Figure EU DC LB SE VM
S We notice that each concept involved in the cloud system bigraphs has a precise semantics. The conceived do not specify just the graphical representation, but also the intended mathematical Hamza Sahli ● Faiza Belala ● Chafia Bouanaka models. Furthermore, the proposed formalisation approach is general enough; it remains valid for any cloud architecture examples.
To deal with the dynamic behaviour of cloud system at runtime, we enrich the proposed bigraph-based model with reaction rules. Hence, a set of reaction rules defining system
configurations and their evolution at runtime is specified.
Albeit, bigraphs are sufficient to formally specify cloud systems static structure, they do not represent their dynamic behaviour. Our main contribution is to extend the proposed bigraph-based model for cloud system by a set of reaction rules expressing its possible reconfiguration. based on reaction rules, to graph transformation ones, to deal in this case with Bigraphical Reactive
Therefore, Cloud system dynamics is formalised as bigraphical reactive system.
Its configuration transition is performed through a series of metareaction rules.
Thus, the meta-reaction rule examples cited above can be instantiated to express cloud system changes in terms of shape shifting or elasticity, while preserving cloud architectural constraints. For a better comprehension of our model, we will illustrate more these reaction rules examples in what follows.
It specifies a developer client type (denoted by D) being connected to the cloud in order to deploy a new service. As we can see in the reactum of the reaction rule in Figure 7, a new service S1 is created within the virtual machine (denoted VM) along with a communication link between the developer and the service he deployed. In the redex, presence of site 1 means that VM virtual machine is able to deploy other services while its disappearance in the reactum means that the virtual machine has reached its limits (saturation), we suppose here that virtual machine capacity is of two services. We can also note the existence of another service that is already loaded in virtual machine VM and is actually exploited by a client of type end user (denoted by EU).
This rule expresses the fact that a service may migrate from one virtual machine to another for many reasons, as degraded virtual machine performance or overloaded virtual machine, expressed in our model by the absence of a site in the virtual machine. As shown in Service migration reaction rule of Figure 8, service S changes its placing from virtual machine VM to a virtual machine VM1.
The virtual machine migration reaction rule (see Figure 9) expresses the fact that a virtual machine may migrate from an excessively loaded host server to a less loaded server. A loaded server is expressed in our model by the absence of a site in this server. In the redex below, we can see an excessively loaded server (denoted SE).
The presented rules are just few examples of many other reaction rules that can be expressed through our model (e.g. new client, service allocation, virtual machine replication, service instance replication, new service instance).
Example 2: Let us head back again to our previous example, a new end user wishes to connect to the second service. Assuming that a service instance can handle at most two end users simultaneously, a new instance of the service has to be created within the virtual machine to treat the new request. We also assume that a virtual machine can handle at most two service instances at the same time. Hence, the virtual machine might be replicated in order to deploy the new service instance.
To express our model dynamics, we have defined two meta-reaction rules sequences written in BigMC appropriate grammar. The first reaction rules sequence expresses the scaling up of our running example cloud architecture when the workload rises (see Figure 10). After the workload dropping (e.g. deallocation of service, disconnection of client), the cloud system has to go back to its original configuration shown in Figure 5 (scale down). Hence, the defined second reaction rules sequence provide to our model the ability to scale down (see Figure 12). By applying this first reaction rules sequence (new end user, virtual machine replication, new service instance, service allocation), we expect the cloud system configuration shown in Figure 11. We can notice the appearance of new service S2 instance denoted S2_1, deployed in a new virtual machine VM1_1 and connected to a new end user denoted EU4.
Model checking is a fully automatic and fast verification technique, which makes it very effective one. Thus, for its ability to express and check safety and liveness properties we use BigMC tool, a model checker designed to operate on Bigraphical Reactive Systems, in order to verify some cloud systems inherent properties.
Through the following example, we identify some properties that we intend to verify using BigMC model checker as elasticity property and its dual one, i.e. a form of elasticity violation (the absence of plasticity).
While the elasticity property consists of checking that the cloud system is scaling up, when the workload rises and scaling down when, it drops. Verifying the absence of plasticity is to ensure that a cloud configuration returns to its initial state after an adaptation process.
Example 3: Cloud computing service availability is
key quality that can be affected by many threats as
distributed denial of service (DDoS) attacks
conducting to ensure the elasticity property, which
plays a significant role in keeping a high level of
service availability. To illustrate elasticity and its
verification technique, we return back to our running
example of a cloud system and its possible
reconfiguration.
Elasticity property: in
Using BigMC tool grammar (see Figure 13), we express in our BRS-based analysis technique, this property by the following formula.
BigMC model checker tries to apply the two reaction rules sequences (see Figure 10 and Figure 12) to verify that the elasticity property holds. This means checking whether cloud configuration size is growing and shrinking.
The result of the model checking is shown in Figure 14; we can notice that BigMC model checker reaches the state 9 starting from initial state 1 without reporting any property violation (existence of counter example).This means that the cloud system is scaling up/down.
Plasticity property: this property can be seen as a cloud system stuck in a giving configuration while being incapable to return to its initial one. This time, we have associated the clause of Figure 15, to express the plasticity property, and the BigMC tool checks its absence, which means reaching the state specified in the property clause.
We can notice that the final state 9 corresponds to the initial state (see Figure 16), meaning that the cloud system has returned to its original configuration at some point.
Elasticity is a key aspect in cloud computing that plays a significant role in keeping a high level of service availability in cloud-based systems. In this paper, we have proposed a formal framework to specify cloud-based systems and verify their proprieties as the elasticity property and some forms of its violation (e.g. plasticity). First, Bigraphical Reactive Systems were adopted as a formal framework for designing and reconfiguring cloud architectures. Cloud Bigraphs graphical and formal basis simplify considerably cloud systems readability. Then, to formally analyse the elasticity and plasticity proprieties, we have extended our proposed cloud model by defining associated clauses that are integrated in the model checker BigMC, designed to operate on Bigraphical Reactive Systems.
BigMC model checker is a very interesting tool that enables executing bigraphical models and checking some of their proprieties. As future work, we intend to evaluate our proposed bigraphical model with other complementing model-checkers.