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.