=Paper=
{{Paper
|id=Vol-1256/paper2
|storemode=property
|title=Model-Checking Cloud Systems Using BigMC
|pdfUrl=https://ceur-ws.org/Vol-1256/paper2.pdf
|volume=Vol-1256
|dblpUrl=https://dblp.org/rec/conf/vecos/SahliBB14
}}
==Model-Checking Cloud Systems Using BigMC==
https://ceur-ws.org/Vol-1256/paper2.pdf
25
Model-Checking Cloud Systems Using BigMC
Hamza Sahli Faiza Belala Chafia Bouanaka
LIRE Laboratory, University of Constantine II
Constantine, Algeria
sahli.hamza.glsd@gmail.com faiza.belala@univ-constantine2.dz@hotmail.com c.bouanaka@umc.edu.dz
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.
Cloud Computing, Reconfiguration, Formal Methods, Bigraphical Reactive System, Model Checking.
1. INTRODUCTION To ensure cloud systems reliability and consistency,
these concepts need to maintain a formal model that
In recent years, cloud computing (Mell et al., 2011) supports specification and analysis of such
has emerged as a new and promising concept in the properties. Until now, there are only few formal
IT evolution; it has increasingly attracted attention models for cloud systems.
from both industry and academic sectors. The basic
idea beyond cloud computing is to provide a poll of Bigraphs (Milner, 2008) enriched with a set of meta-
computing resources as on demand services (e.g. reaction rules, giving rise to Bigraphical Reactive
servers, storage, applications, and services). These Systems, are a good candidate to formalise cloud
resources are consumed by users according to their computing fundamental architectural aspects and
needs and by paying only their real consumption. their reconfiguration. Indeed, bigraphs differ from
Such flexibility and cost effectiveness is what makes traditional formalisms in their expressive power
cloud computing models very attractive. Albeit cloud getting designers a great flexibility to specify their
computing offers numerous benefits, it has raised own reaction rules. In overall terms, our contribution
new obstacles (Michael et al., 2009) and security is two-fold:
concerns (Vic (J.R.), 2011).The fact that the cloud is We argue that Milner’s BRS, through their
accessible from everywhere makes it vulnerable to graphical aspect, are capable of
various types of attacks, like distributed denial of representing both locality and connectivity
service attacks (DDoS). Such attacks could heavily that constitute main concepts of cloud
affect the cloud quality of service (QoS) properties computing architecture.
as high service availability.
We propose a bigraph-based model for
Cloud service availability introduces a very cloud system composed of two independent
important concept that distinguishes cloud regions (physical or logical). For instance,
computing paradigm from the other ones, which is the client and service provider may
rapid elasticity (Guilherme et al., 2012) (Dustdar et represent these regions. Then, interactions
al., 2011). Elasticity goes beyond a simple flexible between these two regions are defined via
and dynamic allocation and deallocation of reaction rules. Since BRS have an
resources on the fly. It implies a permanent executable algebraic language, the
reconfiguration of the underlying network and its obtained formal model serves to model-
associated controls. Elasticity has many forms of check some proprieties that are inherent to
violation such as plasticity (Gambi et al., 2013) (i.e. cloud systems as the elasticity and some
the inability to spontaneously return back to the forms of its violation (plasticity).
original configuration after an adaptation process).
26
Model-Checking Cloud Systems Using BigMC
Hamza Sahli ● Faiza Belala ● Chafia Bouanaka
The rest of the paper is organised as follows. In entities. Thus, it coincides strongly with cloud
section 2, we present related work. In section 3, we computing concepts. A bigraph is composed of two
give a brief overview on Bigraphical Reactive graphs: a place graph for entities locality and
Systems (BRS) and their dedicated model checker. hierarchy representation and a link graph for
Section 4 presents our bigraphical specification of interconnectivity representation. Bigraphs structural
cloud systems. In, section 5 we formally verify the dynamics is formalised by reaction rules that
elasticity and plasticity proprieties. Finally, some express their eventual reconfigurations. Hence,
concluding remarks and ongoing work rounds up the bigraphs can be used for representing system
paper. possible configurations, and reaction rules for
specifying how these configurations may evolve (i.e.
2. RELEATED WORK relations between bigraphs).
There is a significant body of work on defining and 3.1 Structural Aspects
analysing cloud systems, but we are unaware of
approaches involving formal and rigorous A bigraph is the combination of two independent
mathematical models. For instance, authors in structures: the place and link graphs. The place
(Grandison et al., 2010) and (Dong et al., 2010) try graph represents system entities geographical
to tackle the lack of consensus or base distribution. The Link graph is a hypergraph
comprehension on technical constituents of a cloud representing interconnections between these
by presenting an initial definition of cloud computing. entities. Within a BRS, system entities are
They particularly provide some discussion on the represented by nodes and interactions between
relationship between cloud computing and them are represented by edges (see Figure 1).
virtualization.
A node can be dotted with ports representing
Formal models for managing the complexity of connection points to edges or inner/outer names. A
evolving cloud system behaviour while it is executing control is also associated to each node; consisting
is a recent area of interest. Existing approaches in of node type identifier that belongs to a set called
this context are based on various formalisms. signature. Each control indicates the number of
(Freitas et al., 2012) present an abstract ports of each node (i.e. arity), which controls are
formalisation of federated cloud workflows using the atomic for empty nodes and which of the non-atomic
Z notation. In addition, a process algebra framework controls are active (i.e. subject to reactions) or
for the specification of virtual machines migration passive. The inner/outer names of a bigraph indicate
and the associated security policies in the cloud is connectors to other elements. Such interconnection
given in (Jarraya et al., 2012). On the other hand, is only possible if the outer name of a bigraph or root
author in (Rady, 2013) proposes a formal definition corresponds to the inner name of another bigraph.
of service availability in cloud computing using the Sites represent holes into which a root or node can
web ontology language OWL. Authors in (Klai et al., be nested, they are considered as an abstraction
2013) propose a formal model adopting Petri nets indicating the presence of other elements.
for describing service-based business processes in Definition (Milner, 2009): a bigraph is formally
cloud environments. defined by
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 𝑛, 𝑦 >,where:
related bigraphical modelling approach taken on by
(Benzadri et al., 2014) to model-check V and E represent finite sets of nodes and
configurations of a cloud system. In this work, only edges respectively.
some functional properties are verified using LTL 𝑐𝑡𝑟𝑙 ∶ 𝑉 → 𝐾 is a control map that assigns a
Maude tool. Besides, all these research studies do control to each node. The signature K is a
not explicitly tackle the formal analysis of elasticity set of controls.
property which is inherent to cloud systems, expect 𝐺 𝑃 𝑎𝑛𝑑 𝐺 𝐿 are Place and Link graphs
those defining a systematic model-based test respectively.
generation framework for testing the elastic I and J represent inner and outer names
properties of cloud systems (Gambi et al., 2013) and (interfaces) respectively, of the bigraph G. m
(Amziani et al., 2013). and n are the number of sites and roots
respectively.
3. OVERVIEW OF BRS
Bigraphical reactive systems (BRS) were initially
introduced by (Milner, 2008) to provide a graphical
intuitive formal model capable of representing at the
same time connectivity and locality of distributed
27
Model-Checking Cloud Systems Using BigMC
Hamza Sahli ● Faiza Belala ● Chafia Bouanaka
Figure 2: Placing reaction rule.
Figure 1: The anatomy of bigraphs. Figure 3: Linking reaction rule.
In addition to the graphical representation, a term 3.3 A Model Checker for BRS
algebraic language is defined to specify bigraphs,
language primary operations and elements are Few tools for verifying BRS-based distributed
summarized in Table 1. systems inherent properties exist as BigMC
(Perrone et al., 2012) model checker.
Table 1: Terms language for bigraphs
BigMC (Bigraphical Model Checker) is a model-
Term Signification checker designed to operate on Bigraphical
Reactive Systems, where model checking is
U || V Juxtaposition of roots.
accomplished through an exhaustive search of all
U|V Juxtaposition of nodes. possible states of the bigraphical model that satisfy
the property to be verified.
UοV Composition.
One of the main benefits of a model checking
U.V Nesting ( U contains V ). approach is the ability to provide a counter-example
U with outer name x replaced by an whenever the desired property does not hold in the
/x . U
edge. actual system model. In our case, this means
showing system configuration that violates the
x/y Connection inner names y to outer specified property, and the transition system path by
name x. which this configuration was reached. The full
grammar of BigMC bigraph terms is summarized in
3.2 Dynamical aspects Table 2 (Perrone et al., 2012).
Bigraphs structural dynamics is expressed via Table 2: BigMC terms language
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 (Milner, 2008). The 𝑛𝑎𝑚𝑒𝑠 ∶: = 𝑛, 𝑛𝑎𝑚𝑒𝑠 | 𝑛
category of all bigraphs and their reaction rules
𝑛 ∶: = [𝑎 − 𝑧𝐴 − 𝑍][𝑎 − 𝑧𝐴 − 𝑍0 − 9] ∗ | −
constitute a BRS.
𝑃 ∶: = 𝑚𝑎𝑡𝑐ℎ𝑒𝑠(𝑇) | 𝑡𝑒𝑟𝑚𝑖𝑛𝑎𝑙()| ! 𝑃
Using this grammar, we can specify all bigraphical
elements. A BigMC model (designated by M) can be
28
Model-Checking Cloud Systems Using BigMC
Hamza Sahli ● Faiza Belala ● Chafia Bouanaka
composed using other models and/or expressions different services for the end users (end user 1, end
(designated by E). An expression E can be a node user 2, end user 3).
declaration, a reaction rule, a term (T), or a property
(P). A term T can represent a single node, site,
region or a combination of all these elements. Terms
of the form T -> T are considered reaction rules. A
property P represents a state definition to be
checked with BigMC tool.
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.
4. CLOUD SYSTEMS BIGRAPH-BASED
SPECIFICATION
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 Figure 4: Architectural elements of a cloud system.
and the back-end entity that are interacting via the
Internet. 4.1 Modelling Cloud System Architecture
The front-end represents the client interface, used to
In a previous work (Sahli et al., 2014) we have
access the cloud. Clients are classified into two
shown that bigraphs constitute a suitable
kinds: end users (i.e. simple cloud service
mathematical model allowing the formalisation of the
consumers) and developers (i.e., costumers
two parts (back-end and front-end) of cloud
exploiting cloud as for Google Apps, Codeita to host
architecture using two distinct regions of bigraph.
their applications).
This is achieved thanks to a formal mapping based
The back-end is the cloud service provider. It offers
on correspondence rules between the cloud system
a complete system for allocating the required
elements and bigraph concepts (see Table 3).
resources to execute user applications and
managing the entire system flow. Table 3: Correspondence table Cloud / Bigraph
Many types of resources can exist in a cloud as: Concepts
Cloud architecture element Bigraph element
Data centers: physical facilities used to
gather cloud computing resources and Client, Data center, Load Node
components. balancer, Server, Service, Virtual
Load balancers: devices responsible of machine.
service requests rooting and resources Physical or logical Location of the Root
provision. Client and the Cloud.
Various types of Links between Edge/Hyper Edge
Servers: infrastructures for calculation the different elements.
and execution. Abstract elements. Site
Virtual machines (VMs): abstractions of
the underlying infrastructure.
Let us return to our running example and apply the
Example 1: In order to ease the understanding of bigraph based formalisation approach (Sahli et al.,
our proposed cloud system formalisation, we will first 2014) to give a well-defined semantics of its
introduce the following generic example illustrating architectural aspect.
important features that will be considered.
Figure 4 depicts the architecture of a simplified cloud Assuming that the two services are deployed in the
system (back-end) interacting with a set of end users same virtual machine and an end user is connected
(front-end) via the internet. to the first service while the others are connected to
the second service. The corresponding bigraphical
The cloud system is composed of a unique instance model is shown in Figure 5.
of the following cloud components (data center, load
balancer, server and virtual machine) and offers two
29
Model-Checking Cloud Systems Using BigMC
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.
4.2 Modelling Cloud System Reconfiguration
Figure 5: The example’s Bigraphical model. Albeit, bigraphs are sufficient to formally specify
cloud systems static structure, they do not represent
As we can notice in Figure 5, there are two services their dynamic behaviour. Our main contribution is to
actually deployed in the virtual machine VM1 and extend the proposed bigraph-based model for cloud
two end users connected to S2 service through the system by a set of reaction rules expressing its
edge e3. Thus, the S2 service cannot be allocated possible reconfiguration.
to another end user and the virtual machine VM1 Table 5 illustrates how we graft behavioural models,
cannot deploy any other service instance. This is based on reaction rules, to graph transformation
expressed in our model by the absence of a site in ones, to deal in this case with Bigraphical Reactive
that virtual machine. Systems (BRS).
The signature associated to a cloud bigraph is as
follows: K = {L: (0, active), N :( 2, atomic)}, L and N Table 5: Modelling cloud system dynamics
represent controls associated to different nodes.
Cloud system BRS
The different nodes types used in the model and
their associated controls are summarized in Table 4. Configuration CS. Bigraph :
𝑝 𝐿
𝐺𝑐𝑠 = (𝑉𝑐𝑠 , 𝐸𝑐𝑠 , 𝑐𝑟𝑡𝑙𝑐𝑠 , 𝐺𝑐𝑠 ,𝐺𝑐𝑠 )
Table 4: Nodes types of cloud architecture
Reconfiguration from CS Meta reaction rule:
Node Control Attribute Arity Meaning
to CS’. 𝑅𝐿 = (𝐶𝑆, 𝐶𝑆’, 𝑚′ → 𝑚)
Example RL1 : Service deployment
EU N Atomic 2 End User
𝑥/𝐸𝑈𝑥𝑒0𝑒1 |𝐷𝑥𝑒0 ||𝐷𝐶. (𝐿𝐵𝑥𝑒0𝑒2 |𝑆𝐸. (𝑉𝑀. (𝑆𝑒1𝑒2 |𝑑1)|𝑑2)|𝑑3)|𝑑4 →
DC L Active 0 Data center 𝑥/𝐸𝑈𝑥𝑒0𝑒1 |𝐷𝑥𝑒0 ||𝐷𝐶. (𝐿𝐵𝑥𝑒0𝑒2 |𝑆𝐸. (𝑉𝑀. (𝑆𝑒1𝑒2 |𝑆1𝑒2𝑒3 )|𝑑2)|𝑑3)|𝑑4
LB N Atomic 2 Load balancer Example RL2 : Service migration
SE L Active 0 Server 𝑥/𝐷𝑥𝑒0𝑒1 ||𝐷𝐶. (𝐿𝐵𝑥𝑒0𝑒2 |𝑆𝐸. (𝑉𝑀. (𝑆𝑒1𝑒2 )|𝑑2)|𝑑3)|𝑑4 →
VM L Active 0 Virtual 𝑥/𝐷𝑥𝑒0𝑒1 ||𝐷𝐶. (𝐿𝐵𝑥𝑒0𝑒2 |𝑆𝐸. (𝑉𝑀|𝑉𝑀1. (𝑆𝑒1𝑒2 |𝑑1)|𝑑2)|𝑑3)|𝑑4
machine
Example RL3 : Virtual machine migration
S N Atomic 2 Service
𝑥/𝐷𝑥𝑒0𝑒1 ||𝐷𝐶. (𝐿𝐵𝑥𝑒0𝑒2 |𝑆𝐸. (𝑉𝑀. (𝑆𝑒1𝑒2 ))|𝑑3)|𝑑4 →
𝑥/𝐷𝑥𝑒0𝑒1 ||𝐷𝐶. (𝐿𝐵𝑥𝑒0𝑒2 |𝑆𝐸|𝑆𝐸1. (𝑉𝑀. (𝑆𝑒1𝑒2 |𝑑1)|𝑑2)|𝑑3)|𝑑4
The cloud system initial configuration expression in
BigMC tool appropriate grammar is shown in Figure
6. Therefore, Cloud system dynamics is formalised as
bigraphical reactive system. Its configuration
transition is performed through a series of meta-
reaction 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.
Figure 6: Implementing Bigraphical model in BigMC. 4.2.1 Deploying a new service meta-reaction
rule
We notice that each concept involved in the cloud
system has a precise semantics. The conceived It specifies a developer client type (denoted by D)
bigraphs do not specify just the graphical being connected to the cloud in order to deploy a
representation, but also the intended mathematical
30
Model-Checking Cloud Systems Using BigMC
Hamza Sahli ● Faiza Belala ● Chafia Bouanaka
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).
Figure 8: Service migration meta-reaction rule.
4.2.3 Virtual machine migration meta-reaction
rule
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).
Figure 7 : Service deployment meta-reaction rule.
4.2.2 Service migration meta-reaction rule
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.
Figure 9 : Virtual machine meta-reaction rule.
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).
31
Model-Checking Cloud Systems Using BigMC
Hamza Sahli ● Faiza Belala ● Chafia Bouanaka
Example 2: Let us head back again to our previous After the workload dropping (e.g. deallocation of
example, a new end user wishes to connect to the service, disconnection of client), the cloud system
second service. Assuming that a service instance has to go back to its original configuration shown in
can handle at most two end users simultaneously, a Figure 5 (scale down). Hence, the defined second
new instance of the service has to be created within reaction rules sequence provide to our model the
the virtual machine to treat the new request. We also ability to scale down (see Figure 12).
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).
Figure 12: Scaling down reaction rules sequence.
5. FORMAL ANALYSIS OF PROPERTIES
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.
Figure 10: Scaling up reaction rules sequence.
Through the following example, we identify some
By applying this first reaction rules sequence (new properties that we intend to verify using BigMC
end user, virtual machine replication, new service model checker as elasticity property and its dual
instance, service allocation), we expect the cloud one, i.e. a form of elasticity violation (the absence of
system configuration shown in Figure 11. We can plasticity).
notice the appearance of new service S2 instance While the elasticity property consists of checking
denoted S2_1, deployed in a new virtual machine that the cloud system is scaling up, when the
VM1_1 and connected to a new end user denoted workload rises and scaling down when, it drops.
EU4. 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.
Figure 11: The resulting Cloud system configuration.
32
Model-Checking Cloud Systems Using BigMC
Hamza Sahli ● Faiza Belala ● Chafia Bouanaka
Elasticity property: in (Herbst et al., 2013) elasticity
is defined as ability degree of the cloud system to
adapt to workload changes by
provisioning/deprovisioning computing resources in Figure 15: Plasticity property.
an autonomic manner.
Using BigMC tool grammar (see Figure 13), we We can notice that the final state 9 corresponds to
express in our BRS-based analysis technique, this the initial state (see Figure 16), meaning that the
property by the following formula. cloud system has returned to its original
configuration at some point.
Figure 13: Elasticity property.
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.
Figure 16: Plasticity checking result.
6. CONCLUSION
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
Figure 14: Elasticity checking result. proposed cloud model by defining associated
clauses that are integrated in the model checker
Plasticity property: this property can be seen as a BigMC, designed to operate on Bigraphical Reactive
cloud system stuck in a giving configuration while Systems.
being incapable to return to its initial one. This time,
we have associated the clause of Figure 15, to BigMC model checker is a very interesting tool that
enables executing bigraphical models and checking
express the plasticity property, and the BigMC tool
some of their proprieties. As future work, we intend
checks its absence, which means reaching the state
to evaluate our proposed bigraphical model with
specified in the property clause.
other complementing model-checkers.
33
Model-Checking Cloud Systems Using BigMC
Hamza Sahli ● Faiza Belala ● Chafia Bouanaka
REFERENCES Jarraya, Y., Eghtesadi, A., Debbabi, M., Zhang, Y.
and Pourzandi, M. (2012) Cloud calculus: Security
Mell, P. and Grance, T. (2011) The NIST definition verification in elastic cloud computing platform. In
of Cloud Computing. Technical Report, National International Symposium on Security in
Institute of Standards and Technology (NIST), Collaboration Technologies and Systems
Gaithersburg, MD, p. 800-145. (SECOTS2012), IEEE Press, p. 447-454.
Michael, A., Armando, F., Rean, G. and Anthony, D. Rady, M. (2013) Formal definition of service
J. (2009) A Berkeley View of Cloud, A Berkeley View availability in cloud computing using owl. In
of Cloud: s.n. Computer Aided Systems Theory-EUROCAST
Vic (J.R.), W. (2011) Securing the Cloud: Cloud 2013, Springer, p. 189-194.
Computer Security Techniques and Tactics. Klai, K. and Tata, S. (2013) Formal Modelling of
Elsevier. Elastic Service-Based Business Processes.
Guilherme, G. and Luis Carlos, E.D. (2012) A Services Computing (SCC), 2013IEEE International
Survey on Cloud Computing Elasticity. In Conference on, p. 424-431.
Proceedings of the 2012 IEEE/ACM Fifth Benzadri, Z., Bouanaka, C., Belala, F. (2014)
International Conference on Utility and Cloud Verifying Cloud Systems using A Bigraphical
Computing (UCC '12), IEEE Computer Society, Maude-Based Model Checker. The 4th International
Washington, USA, p. 263-270. Conference on Cloud Computing and Services
Dustdar, S., Yike, G., Satzger, B. and Hong-Linh, T. Science, CLOSER, Barcelona, Spain.
(2011) Principles of Elastic Processes. IEEE Amziani, M., Melliti, T. and Tata, S. (2013) Formal
Internet Computing, vol. 15, no. 5, p. 66–71. Modeling and Evaluation of Service-Based Business
Gambi, A., Filieri, A. and Dustdar, S. (2013) Iterative Process Elasticity in the Cloud. 22nd IEEE
Test suites refinement for elastic computing International Conference on Collaboration
systems. In Proceedings of the 2013 9th Joint Technologies and Infrastructure (WETICE 2013),
Meeting on Foundations of Software Engineering Hammamet, Tunisia, p. 284–291.
(ESEC/FSE 2013), ACM, New York, USA, p. 635- Amziani, M., Melliti, T. and Tata, S. (2013) Formal
638. Modeling and Evaluation of Stateful Service-Based
Milner, R. (2008) Bigraphs and their algebra. In Business Process Elasticity in the Cloud. On the
Proceedings of the LIX Colloquium on Emerging Move to Meaningful Internet Systems OTM 2013
Trends in Concurrency Theory (LIX 2006), Conferences, Springer.
Electronic Notes in Theoretical Computer Science, Milner, R. (2009) The Space and Motion of
Volume 209, Elsevier, p. 5-19. Communicating Agents. Cambridge University
Grandison, T., Maximilien, E. M., Thorpe, S. and Press.
Alba, A. (2010) Towards a Formal Definition of a Perrone, G., Debois, S. and Hildebrandt, T. (2012)
Computing Cloud. 6th World Congress on Services, A Model Checker for Bigraphs. In proceedings of the
Miami, p. 191-192. 27th ACM Sym, in Applied Computing ACM-SAC'12,
Dong, H., Hao, Q., Zhang, T. and Zhang B. (2010) p. 1320-1325.
Formal discussion on relationship between Sahli, H., Bouanaka, C. and Dib, A.T.E. (2014)
virtualization and cloud computing. In Parallel and Towards a Formal Model for Cloud Computing
Distributed Computing, Applications and Elasticity. To appear in the 23rd IEEE International
Technologies (PDCAT), International Conference Conference on Collaboration Technologies and
on, p. 448-453. Infrastructure (WETICE 2014), Parma, Italy.
Freitas, L. and Watson, P. (2012) Formalising Herbst, N.R., Kounev, S. and Reussner, R. (2013)
workflows partitioning over federated clouds: Multi- Elasticity in Cloud Computing: What It Is, and What
level security and costs. In Services (SERVICES), It Is Not. Proceedings of the 10th International
2012 IEEE Eighth World Congress on, p. 219-226. Conference on Autonomic Computing (ICAC 13),
San Jose, CA, USENIX, p. 23-27.