ICAASE'2014 BiCloud-2M: A Combined Bigraph Maudebased Tool for Cloud Specification and Analysis BiCloud-2M: A Combined Bigraph Maude- based Tool for Cloud Specification and Analysis Zakaria Benzadri Chafia Bouanaka and Faiza Belala LIRE Laboratory LIRE Laboratory University of Constantine 2 University of Constantine 2 Constantine, Algeria Constantine, Algeria c.bouanaka@umc.edu.dz and benzadri@gmail.com belalafaiza@hotmail.com Abstract – Service availability is a challenging issue in Cloud Computing. It implies continuous reconfiguration of cloud architecture by adding or removing different resources (virtual machines, services...) to ensure the suited quality of service. Thus a main goal in Cloud systems design is to model and analyse cloud architecture and its dynamic reconfiguration. Based on Bigraphical Reactive Systems (BRS) theory as a semantic framework and Maude language as an executable specification language, we propose a tool called BiCloud- 2M offering a formal support for specifying and analysing cloud architecture systems. In this paper, we describe the BiCloud-2M implementation, and how it can be used to verify some cloud inherent properties. Keywords – Cloud Computing; Bigraphical Reactive Systems; Maude; Model checking. seem adequate for two reasons. Firstly, the model emphasizes on both locality and 1. INTRODUCTION connectivity that can be used to specify location and interconnection of cloud systems. Secondly, Cloud Computing is a recent paradigm for a set of reaction rules, providing to bigraphs the information technology that enables remote, on- ability to reconfigure themselves, are very useful demand access to a set of configurable to formalize cloud system dynamics. A nice computing resources as internet-based services. consequence of this axiomatization is that Although this cloud model promotes service relationships between cloud services and cloud availability, emphasizes on resources reuse customers have been exploited to formally rationalization and provides opportunities for analyse some cloud inherent properties. This reducing software development costs, there are would not have been possible without a mapping still many open issues. One major challenging of the bigraphical model to a Maude-based topic is to formally model cloud-based specification [3]. Maude [4] is a high-level architecture and analyse its shape shifting. The language and a high-performance system that main objective of this paper is to propose a supports rewriting logic specification and combined bigraph Maude-based tool (BiCloud- programming of systems. 2M) to specify cloud systems and offer analysis support to model-check their inherent properties. BiCloud-2M implements our bigraphical To ease BiCloud-2M exploitation, the tool offers a modelling methodology in which both the cloud java user interface that assists designers to architecture elements and their interactions are specify cloud systems and analyse them. modelled explicitly. It has an efficient Maude- based rewriting engine, able to execute and Bigraphical Reactive Systems (BRS) [1] were analyse the cloud architecture specifications. adopted as a semantic basis to specify fundamental aspects of cloud computing [2]. BRS International Conference on Advanced Aspects of Software Engineering ICAASE, November, 2-4, 2014, Constantine, Algeria. 165 ICAASE'2014 BiCloud-2M: A Combined Bigraph Maudebased Tool for Cloud Specification and Analysis The rest of the paper is organized as follows. The aforementioned works are limited and focus Section 2 discusses related work. Section 3 solely on enhancing the financial and serves as a brief introduction to the proposed technological aspects of cloud computing. modelling methodology. Then, section 4 Consequently, cloud computing lacks a describes the main principles of our tool, and its theoretical framework that associates a clear uses. Finally, section 5 compares our work with semantics to its basic concepts: service delivery other related proposals and section 6 draws and deployment models. This framework might some conclusions and outlines some future be able to support major cloud computing research activities. concepts specification and allows formal analysis of high level services provided over the cloud computing architecture. Within this 2. RELATED WORK perspective, we have proposed a formal semantic framework for specifying cloud systems [2]. In this In the literature, several frameworks have been paper, we develop a tool called BiCloud-2M that recently provided but do not deal with all offers analysis support to model-check their fundamental concepts of cloud computing. They inherent properties. particularly focus on cloud computing financial and technological aspects; MobiCloud (Cloud Framework for Mobile Computing and 3. BiCloud-2M FORMAL BASIS Communication) [5], is a new cloud framework for MANETs that focuses on interrelated system The BiCloud-2M modelling methodology is based components including resource and information on a judicious coupling of BRS theory as a flow isolations. It enhances communication by semantic framework and Maude language as an addressing trust management, secure routing, executable specification language. We have and risk management issues in the network. The proposed [2] a formal model for cloud computing work in [6] aims to present technical and business architecture design and its shape shifting challenges for organizational Cloud adoption, specification using Bigraphical Reactive and describes four key areas to be addressed: Systems. A mapping to Maude executable Classification; Organizational Sustainability specifications was also defined in order to Modelling; Service Portability and Linkage. The analyse the obtained specifications [3]. Cloud Computing Business Framework (CCBF) A cloud service is modelled by a node has been proposed to help organizations representing an abstraction of three different achieving Cloud design, deployment, and service service delivery models (IaaS, PaaS and SaaS) migration. It has been used in several that collaborate to ensure front end requests. organizations offering added values and positive Controls attached to nodes allow distinguishing impacts. In [7], the authors identify the necessary between the three service delivery models. Cloud perspectives to capture benefits of cloud customers are also modelled as nodes equipped computing. Then, they propose a conceptual with specific controls that enable determining framework for cloud computing benefits. Their both types of Cloud customers (End users and framework accounts for the different business Independent Software Vendors). Cloud areas and organizational levels where each of the architecture dynamics in terms of interactions benefits manifests. Ricardo J. et al [8] propose an between cloud services and customers are ontology-enriched framework for cloud-based established via reaction rules. In Maude Enterprise Interoperability. The proposed language, bigraphical nodes are defined as a framework allows knowledge, decisions, and specific sort, and reaction rules are implemented responsibilities to be exchanged about by rewrite rules. The following correspondence negotiations. It is supported by a reference table summarizes our Bigraphical Cloud ontology and uses cloud-computing as the computing architecture concepts and their paradigm to deploy services on the network. equivalent in Maude language. Chandrakumar T. and Parthasarathy S. [9] explore the available literature on cloud ERP systems, suggest factors to be considered in cloud ERP, and propose a framework for evaluating cloud ERP systems. Their framework is grounded on software engineering parameters involved in the development of cloud ERP. International Conference on Advanced Aspects of Software Engineering ICAASE, November, 2-4, 2014, Constantine, Algeria. 166 ICAASE'2014 BiCloud-2M: A Combined Bigraph Maudebased Tool for Cloud Specification and Analysis Table 1. Correspondence table Cloud / Bigraph a property to verify. Additionally, it is responsible / Maude concepts of parsing the BiCloud architecture and generating the corresponding Maude-based Cloud Computing BRS Maude Language specifications (using the defined JBigraph Parser Service and Nodes Operators and MaudeIO modules). Customer The graphical user interfaces of BiCloud-2M are Service models Controls Sorts implemented in the GUI module. Figure 2 presents a snapshot of the proposed tool. The Customers types Controls Sorts Menu Bar contains a list of shortened commands Dynamics Reaction Rewrite rules to be executed in BiCloud-2M. The left hand rules panel (area 1 in Figure 2) is a toolbar for cloud Properties LTL architecture specification. The upper right panel Specifications in area 2 of figure 2 is a toolbar for cloud execution and analysis. The lower right pane (area 3 in figure 2) is a Maude console for various The use of rewriting logic via its implementation BiCloud-2M results and outputs. language Maude, takes advantage of the model- checker tool for LTL properties verification [4]. Thus, BiCloud-2M offers a verification module for model checking some cloud inherent properties. 4. BiCloud-2M TOOL PRESENTATION 1 2 Our model is implemented in BiCloud-2M tool as system modules. Figure 1 presents a basic overview of the defined modules and their sub- module dependencies. 3 4.1. Principle Figure 2. A snapshot of BiCloud-2M Tool The current BiCloud-2M tool is composed of a JAVA-frontend for various editing tasks as 4.2. Core BiCloud-2M designing new cloud architecture and introducing The Maude-based backend component is a rewriting engine for executing BiCloud Maude Backend specifications and verifying their inherent properties. It is composed of four defined modules (see Figure 1), each one with a specific BiCloud BiCloud role: the MBigraph module includes sorts and Checking BiCloud Dyn Arch operators declaration for Bigraphs theory concepts definition. The BiCloud-Arch module defines the syntax and semantics of cloud MBigraph architecture elements. The BiCloud-Dyn module specifies Cloud system dynamics, it contains a set of rewrite rules expressing cloud architecture possible reconfigurations. Finally, the BiCloud- MaudeIO Checking module allows checking LTL formula by introducing a given initial state. GUI JBigraph Parser The proposed BiCloud-2M tool will be illustrated via the cloud health system that allows doctors to Java Frontend exchange patient’s information. At each appointment, the doctor needs to consult medical information of the patient by editing state history Figure1. BiCloud-2M modules and make sure of the performed treatments. We International Conference on Advanced Aspects of Software Engineering ICAASE, November, 2-4, 2014, Constantine, Algeria. 167 ICAASE'2014 BiCloud-2M: A Combined Bigraph Maudebased Tool for Cloud Specification and Analysis consider that the SaaS (S1) allows doctors to consult medical information of every patient. BiCloud-2M Architecture: As initial state, we consider the SaaS (S1) is started in the cloud and two customers (doctor’s) (C1 and C2) are requesting it. This initial state is edited in BiCloud- 2M using commands available in cloud architecture specification toolbar. Figure 3 shows the cloud service input-box that allows the specification of a cloud service. It takes as arguments:  a Quoted Identifier to specify its name;  a Control specifying its service delivery model; Figure 4. Cloud Customer Input-box  an Attribute specifying a service state (available, unavailable, and cloned); BiCloud-2M Dynamics: We defined a set of  a set of Edges connected to its three rewriting rules that express the cloud architecture ports. dynamics. Table 2 illustrates the proposed rewriting rules. Table 2. Cloud rewriting rules Rewriting rule Maude code Cloud service rl : service< i ; cs:Scsb ; available >[ e1 , Allocation e2 , e3 ].{ b2 } | customer< i1 ; cc1:Sccb ; i ; p:Port >[ Req ] | b1 => service< i ; cs:Scsb ; available >[ e1 , e2 , e3 ].{ b2 } | customer< i1 ; cc1:Sccb ; i ; p:Port >[ e1 ] | b1 . Cloud service rl: customer[ deallocation edge na ] | b1 => customer[ null ] | b1 . Cloud Scaling rl: service< i ; cs:Scsb ; unavailable >[ e1 , e2 , e3 ].{ b2 } | customer< i1 ; cc1:Sccb Up ; i ; p:Port >[ Req ] | b1 => service< i ; cs:Scsb ; unavailable >[ e1 , e2 , e3 ].{ b2 } | service< i ; cs:Scsb ; cloned >[ e1 Figure3. Cloud Service Input-box , e2 , e3 ].{ null } | customer< i1 ; cc1:Sccb ; i ; p:Port >[ e1 ] | b1 . Figure 4 represents the input-box to specify a cloud customer. It takes as arguments: Cloud Scaling rl : service< i ; cs:Scsb ; cloned >[ e1 , Down e2 , e3 ].{ b2 } | customer< i1 ; cc1:Sccb  a Quoted Identifier to specify its name; ; i ; p1:Port >[ null ] | b1 => customer< i1  a Control specifying its customer type; ; cc1:Sccb ; i ; p1:Port >[ null ] | b1 .  a Quoted Identifier to specify the requested service;  a Port specifying on which the requested service will be delivered. International Conference on Advanced Aspects of Software Engineering ICAASE, November, 2-4, 2014, Constantine, Algeria. 168 ICAASE'2014 BiCloud-2M: A Combined Bigraph Maudebased Tool for Cloud Specification and Analysis Allocating the cloud service (S1), is realized via Figure 8 shows model checking results. The the BiCloud-rewrite command, which is available result is that the model is concluded to possess in the cloud architecture execution toolbar. Figure the desired property. 5 shows the BiCloud-rewrite input-box that allows the execution of the underlying specifications. It takes as arguments the rewrite command type and the number of rewrites. Figure 8. BiCloud-check result 5. DISCUSSION A set of tools is proposed in the literature for BRS edition, execution and verification; BPL Tool [10] is the first implementation of BRS with binding, Figure 5. BiCloud-Rewrite Input-box Bigredit (for "bigraph editor"), Big Red [11] is a visual editor for bigraphs, and BigMC [12] is a The result will be shown in the output pane (see model-checker designed for BRS properties figure 6): model checking. However, during their exploitation, we have been confronted with several limitations, because they remain restrictive and do not correspond to our expectations. Although BigMC is the unique tool for model checking bigraphs, it remains very restrictive since it enforces designers to adapt Figure 6. BiCloud-Rewrite result their model to the desired property. BiCloud-2M Checking: One major benefit of BiCloud-2M offers the possibility to execute and adopting Maude as an implementation language formally analyze cloud bigraphical specifications, of the BiCloud-2M tool is the exploitation of by: (i) simulating the behavior from a given initial Maude model-checker for cloud system analysis. state; (ii) checking that all terminal states We deal here with a significant property such as reachable from the initial state satisfy a linear service availability. temporal logic property. Additionally, BiCloud-2M is more expressive in terms of properties Service availability is fulfilled if system model do specification and its response time is reduced not contain an unsatisfied customer request. It is considerably. Figure 9 highlights BiCloud-2M formally specified with the following LTL formula: performance, where the y-axis is the time spent “O [] not (requester)”. to rewrite the initial state, and the x-axis is the Figure 7 represents the BiCloud-check input-box number of rewrites. that takes as arguments the LTL property specification and its relevant state predicates. Figure 7. BiCloud-check Input-box Figure 9. BiCloud-2M Performance International Conference on Advanced Aspects of Software Engineering ICAASE, November, 2-4, 2014, Constantine, Algeria. 169 ICAASE'2014 BiCloud-2M: A Combined Bigraph Maudebased Tool for Cloud Specification and Analysis 6. CONCLUSION [9] Chandrakumar T. and Parthasarathy S. (2014). A Framework for Evaluating Cloud BiCloud-2M is a tool for cloud systems design Enterprise Resource Planning (ERP) and verification that supports a bigraphical Systems. Computer Communications and Networks. pp 161-175 modelling methodology for both cloud [10] Glenstrup, A.J., Damgaard, T.C., Birkedal, L., architecture elements and their interactions and jsgaard, E. H. An implementation of modelling. It has an efficient rewriting engine, bigraph matching. 2007. able to execute and analyse the cloud [11] Faithfull, AJ, Perrone, GD & Hildebrandt, T architecture specifications. 2013, 'Big Red: A Development Environment for Bigraphs' E A S S T Electronic BiCloud-2M tool is open and extensible where Communications, vol 61. new features and properties can be easily in [12] Perrone, G., Debois, S., Hildebrandt, T.T.: A traduced as generalizing its use to any bigraph model checker for bigraphs. In Ossowski, S., Lecca, P., eds.: SAC, ACM (2012) 1320– and the corresponding inherent properties. 1325. REFERENCES [1] Milner, R.: The Space and Motion of Communicating Agents. Cambridge University Press (2009). [2] Benzadri, Z., Belala F., and Bouanaka, C.: Towards a Formal Model for Cloud Computing. ICSOC workshops, 2013, (2014). [3] Benzadri, Z., Bouanaka, C., and Belala F.: Verifying Cloud Systems using A Bigraphical Maude-Based Model Checker. CLOSER workshops, 2014, (2014). [4] Clavel, M., Durn, F., Eker, S., Lincoln, P., Mart-Oliet, N., Meseguer, J., Talcott, C.L., eds.: All About Maude - A High-Performance Logical Framework, How to Specify, Program and Verify Systems in Rewriting Logic. In Clavel, M., Durn, F., Eker, S., Lincoln, P., Mart-Oliet, N., Meseguer, J., Talcott, C.L., eds.: All About Maude. Volume 4350 of Lecture Notes in Computer Science., Springer (2007). [5] Dijiang Huang; Xinwen Zhang; Myong Kang; Jim Luo. (2010). "MobiCloud: Building Secure Cloud Framework for Mobile Computing and Communication," Service Oriented System Engineering (SOSE), 2010 Fifth IEEE International Symposium on , vol., no., pp.27,34, 4-5 [6] Chang, Victor, Walters, Robert John and Wills, Gary. (2014). The development that leads to the Cloud Computing Business Framework. International Journal of Information Management, June, 33, (3), 524- 538. [7] Nattakarn P., Xiaofeng W., and Pekka A. (2013). Towards a Conceptual Framework for Assessing the Benefits of Cloud Computing, 4th International Conference, ICSOB 2013, Potsdam, Germany, June 11- 14, 2013. Proceedings [8] Ricardo J., Adina C., Carlos C, Moisés D. , Parisa G. (2013) Ontology Enriched Framework for Cloud-based Enterprise Interoperability. Concurrent Engineering Approaches for Sustainable Product Development in a Multi-Disciplinary Environment International Conference on Advanced Aspects of Software Engineering ICAASE, November, 2-4, 2014, Constantine, Algeria. 170