A Formal Approach for Correct Elastic Package-Based Free and Open Source Software Composition in Cloud Imed Abbassi1(B) , Mohamed Graiet2 , Sindyana Jlassi1 , Abir Elkhalfa1 , and Layth Sliman3 1 ENIT, University of Tunis El Manar, Tunis, Tunisia abbassi.imed@gmail.com, sindyana.jlassi@gmail.com, abir.elkhalfa@gmail.com 2 INSA Centre-Val de Loire, Blois, France mohamed.graiet@insa-cvl.fr 3 Efrei, Paris, France layth.sliman@efrei.fr Abstract. Cloud environments have been increasingly used to deploy and run software while providing a high level performance with a low operating cost. Most of the existing software applications are nowadays distributed as Package-based Free and Open Source (PFOS) applications. Diﬀerent requirements must be considered while conﬁguring PFOS software. These requirements can be classiﬁed into two classes: dependency and capacity requirements. In this paper, we proposed a novel approach to ensure the correctness of elastic composite PFOS applications. Our approach is based on Event-B and combines proof-based models with model checking to provide a more complete veriﬁcation. It starts by abstractly specifying the main concepts of PFOS software, and then reﬁning them through multiple steps to model the elastic composite PFOS software and its correctness requirements. The consistency of each model and the relationship between an abstract model and its reﬁnements are obtained by formal proofs. Finally, we used the ProB model-checker to trace possible design errors. Keywords: Free and open source software Elasticity · Event-B · Veriﬁcation 1 · Composition · Cloud · Introduction Cloud environments are used nowadays to deploy and run software applications [1]. These software applications use cloud components (databases, containers, Virtual machines, and so on) which in turn use cloud resources (CPU, memory, network, and so on). One of the most interesting properties provided by Cloud environments is the horizontal and vertical elasticity at diﬀerent levels and particularly the software as a service (SaaS) level [2,3]. Vertical elasticity allows to c Springer International Publishing AG 2017 H. Panetto et al. (Eds.): OTM 2017 Conferences, Part I, LNCS 10573, pp. 732–750, 2017. https://doi.org/10.1007/978-3-319-69462-7_46 A Formal Approach for Correct Elastic PFOS Composition in Cloud 733 increase or decrease the software resources, while the horizontal elasticity is used to replicate or remove software instances [3,4]. Most of the existing software are nowadays distributed as Package-based Free and Open Source (PFOS) applications [5]. In this work, we focus on this type of software. The PFOS software can be installed, run or uninstalled automatically. They provide a collection of functional capabilities [6]. A functional capability is deﬁned either as a required port, or as a provided port. Reusability is a central concept of software design [7]. For instance, it allows the construction of composite PFOS software. These composite PFOS software can be automatically extended by adding new components or removing others [8]. For example, the Rodin [9] and Eclipse platforms [10,11] are well-known extensible composite PFOS applications. Diﬀerent requirements must be considered while conﬁguring composite PFOS software [5]. These requirements can be classiﬁed into two classes: dependency and capacity requirements. The dependency requirements are deﬁned as a set of constraints between components [5]. An example of dependency requirement is that the installation of some components requires the installation of others. The capacity requirements are deﬁned as a set of upper and lower bound constraints on the number of ports’ bindings [5]. For instance, the provided ports shall satisfy a maximum number of bindings [5]. The required ports shall satisfy a minimum number of bindings [5]. The main objective of our work concerns mainly the correctness veriﬁcation problem of the horizontal and vertical elasticity properties for composite PFOS applications. To meet such an objective, we propose a novel approach for the formal modeling and veriﬁcation of such applications based on the EventB formal method [12] and combining proof-based models with model checking to provide a more complete veriﬁcation. Event-B is chosen because of its capability to eﬀectively master the complexity of the system design using stepwise reﬁnement. The step-wise reﬁnement method produces a correct speciﬁcation by construction since at each step the diﬀerent properties of the system are formally proven. Moreover, Event-B tools can be used to perform an incremental veriﬁcation by checking the deﬁned properties and constraints at each PFOS software execution step. These execution steps are ensured by events. In order to guarantee the invariants/constraints preservation by these events, Event-B deﬁnes proof obligations. Hence, using our approach we check and prove the correctness of the PFOS software composition and its requirements and elasticity properties. Then, once the composite PFOS applications are veriﬁed, our formal model guarantees that their execution does not face failures and inconsistencies related to the violation of dependency and capacity requirements. The rest of this paper is organized as follows: Sect. 2 presents a motivating example and the basic concept of the Event-B method and its proof procedure. In Sect. 3, we propose an Event-B formal model for the composite PFOS software. In Sect. 4, we reﬁne this model through several steps to model the (horizontal and vertical) properties and their correctness requirements. The consistency veriﬁcation process of such a model is described in Sect. 5. Section 7 concludes this paper and presents some future works. 734 2 I. Abbassi et al. Motivation and Background In this section, we ﬁrst introduce a motivating example that will be used throughout the paper. Finally, we describe the basic knowledge of Event-B. 2.1 Motivating Example Let’s consider a Wordpress application to illustrate our approach. This application is composed of the following three software components: – apache2: a PFOS software providing an httpd port. – mysql: a PFOS software providing mysql up and mysql ports. – wordpress: a PFOS software providing wordpress port, while requiring httpd and mysql up ports. The internal behavior of these software components is described as a ﬁnite state automaton composed of the following three states, namely installed, uninstalled and running (see Fig. 1). Fig. 1. The Wordpress application [5]. All of the Wordpress application components are initially set to the uninstalled state. Then, its execution state can be changed according a set of dependency requirements. Indeed, wordpress can be installed only when apache2 is already installed or is running. The running or installation process of the apache2 is required in order to activate the provided httpd port that is required by wordpress software. Once installed, wordpress can either be run when mysql software is running, or be uninstalled. When running, it can be stopped and rolled back to the installed state. When in use by wordpress, apache2 and mysql can neither be stopped nor uninstalled. The only way to stop them is to release their dependency with the wordpress component. This is done by stopping and uninstalling the wordpress component. When all their dependencies are correctly released, apache2 and mysql can be securely stopped or uninstalled. A Formal Approach for Correct Elastic PFOS Composition in Cloud 2.2 735 Event-B Method Event-B [12] is a formal method based on set theory and ﬁrst order logic. It provides a correct-by-construction design methodology and covers the whole software’s life-cycle. Indeed, the designers start by abstractly specifying the requirements of the whole system and then reﬁning them through several steps to reach a detailed description of the system that can be translated into executable code (C, JAVA, etc.) via additional tools such as EB2C [13] and EB2J [14]. An Event-B model includes two types of entities to describe a system: machines and contexts. A machine represents the dynamic parts of a model. It may contain variables, invariants, theorems, variants and events. On the other hand, a context represents the static parts of a model. It may contain carrier/enumerate sets, constants, axioms and theorems. Those constructs appear on Fig. 2. Fig. 2. Machine and context relationships A machine is organized in clauses: the ﬁrst clause, VARIABLES, represents the deﬁned variables of the model. The INVARIANTS clause represents the invariant properties of the system and must at least include the typing of the variables declared in the VARIABLES clause. The EVENTS clause contains the list of events of the model. An event is modeled with a guarded substitution and ﬁred when its guards is evaluated to true. The events occurring in an Event-B model aﬀect the state described in the VARIABLES clause. An Event-B model may refer to a context or machine. A context consists of the following clauses: the SETS clause describes a set of abstract and enumerated types. The CONSTANTS clause represents the constants of the model, whereas the AXIOMS clause contains all the properties of the constants and their types. The concept of reﬁnement is the main feature of Event-B. It allows an incremental design of systems. At each level of abstraction we introduce further details of the modeled system. Correctness of Event-B machines is ensured by establishing proof obligations (POs); they are generated by a RODIN platform tool called proof obligations generator to check the consistency of the model. Let M be an Event-B model with v as variables. The invariants are denoted by I(v) 736 I. Abbassi et al. and E is an event with an input parameter p, a guard G(v, p) and a before-after predicate R(v, p, v). The initialization event is a generalized substitution of the form v : IN IT (v). The initial proof obligation guarantees the satisfaction of the initialization invariants: IN IT (v) ⇒ I(v). The second proof obligation is related to events. The event E should preserve the invariants after its triggering. The Feasibility statement (FIS) and the invariant preservation (INV) are given in the following predicates: – FIS: I(v) ∧ G(v, p) ⇒ ∃v·R(v, p, v) – INV: I(v) ∧ G(v, p) ∧ R(v, p, v) ⇒ I(v) An Event-B model M with invariants I is well-formed, denoted by M I, only if M satisﬁes all of the proof obligations. 3 Composite PFOS Software Model In this section, we propose an Event-B model for the composite PFOS software. This model explores two abstraction levels. At the ﬁrst level, we abstractly specify the basic concepts of PFOS software. At the second level, we reﬁne such an abstract model by introducing the software dependency concept in order to formally deﬁne the composition process. 3.1 PFOS Software Model Software applications are nowadays distributed as Package-based Free and Open Source (PFOS) applications [6,15]. The package includes the current software artifact and its default conﬁguration. Fig. 3. State transition diagram of PFOS software A PFOS software can be associated to a life-cycle statechart. A set of states (uninstalled, installed, running) and a set of transitions (install(), uninstall(), run(), stop()) are used to describe the PFOS software status and behavior (see Fig. 3). When being created, a software is initially set to the uninstalled state. Then, it can transit to the installed state. Once installed, it can either be uninstalled, or transited to the running state. A Formal Approach for Correct Elastic PFOS Composition in Cloud 737 Fig. 4. The PFOSScontext and PFOSSmachine description Fig. 5. The formalization of the installation, uninstallation, run and stop processes of software using Event-B notation We formalize the PFOS software using an Event-B model that includes a machine and a context. The context, P F OSScontext (see Fig. 4), describes the static part of PFOS software. By SOF T W ARE, we denote the set of PFOS software. The enumerated set ST AT E represents all possible states of PFOS components, namely uninstalled, installed and running. The machine, P F OSSmachine (see Fig. 4), formally models the behavior of PFOS software using variables and a set of events. The variable, states (formalized as a partial function from the set SOF T W ARE to ST AT E), speciﬁes the current state of each PFOS software. Figure 5 presents the formalization of the install, uninstall, run and stop processes of a software s. The guard grd2 of each event deﬁnes the current state of the input parameter. The events install and uninstall are behaviorally opposite. Similarly, the run event has the inverse behavior of stop. 3.2 Composite PFOS Software Model Reusability constitutes the main feature of software design [7]. It allows the construction of a new value-added software by combining a set of existing software. The composite PFOS software are the results of the combination of a set of existing PFOS software [5]. They describe the preconditions for installing, running and uninstalling components. These preconditions express dependency relations. The dependencies between the components are deﬁned through ports as a set of bindings [5]. A port represents a functional capability that can be either provided 738 I. Abbassi et al. or required by software components. A binding is a relation deﬁned through a port between two software components. This port shall be provided by one of them and required by the other. For the sake of simplicity, we assume two components can be bound through only one port. Diﬀerent requirements shall be satisﬁed while executing composite PFOS software. In this paper, we consider the following requirements: – REQ1: the installation of a software requires the installation of all the required software [5]. – REQ2: the software that are running or having provided ports under use by others cannot be uninstalled [5]. – REQ3: running a software requires running all of the required software [5]. – REQ4: the provided ports shall satisfy a maximum number of bindings [5]. – REQ5: the required ports shall satisfy a minimum number of bindings [5]. These requirements shall always be satisﬁed by the composite PFOS software. The ﬁrst three requirements deﬁne dependency constraints between software components. The requirement REQ4 deﬁnes a set of upper-bound capacity constraints on the provided software ports. The last one deﬁnes a set of lower-bound capacity constraints on the required software ports. According to our motivating example, the installation of the Wordpress component requires the installation of the apache2 and mysql components. The mysql component provides two ports, namely mysql up and mysql (see Fig. 1). The mysql port, is provided in the running and installed states. The mysql up port is required by the W ordpress component in the running state. Fig. 6. The CPFOSScontext description To formally model composite PFOS software, we ﬁrst extend the PFOSScontext (see Fig. 6). We introduced a ﬁnite set, P ORT , to denote all the ports that are provided or required by software. The requiredP orts function deﬁnes the set of ports that are required by a component in a given state. The providedP orts function deﬁnes the set of ports that are provided by a component in a given state. The portsCapacity function deﬁnes a set of capacity constraints on the required and provided ports of components. A Formal Approach for Correct Elastic PFOS Composition in Cloud 739 Fig. 7. The CPFOSSmachine description Second, we reﬁne the P F OSSmachine (see Fig. 7) in order to specify the dynamic aspect of composite PFOS software such as behavior and composition requirements (REQ1, REQ2, REQ3, REQ4, REQ5). The CS variable represents the set of PFOS software components. We use the SB variable to deﬁne the set of binding relations between software components. The ports variable denotes the set of ports with which the software components are bound. The types of these variables are deﬁned using two invariants, namely type2 and type3 (see Fig. 7). For the sake of clarity, the invariants, deﬁned in CPFOSSmachine and modeling the PFOS software composition requirements, are separately presented in Fig. 8. Fig. 8. The Event-B invariants modeling the PFOS software composition requirements 4 Extending the Composite PFOS Software Model with Elasticity Properties As we stated in the introduction, the main goal of this paper is the correctness veriﬁcation of the (vertical and horizontal) elasticity properties of composite PFOS software. To achieve this goal, we extend the composite PFOS software model described in the previous section. This extension comprises two steps: – Step 1: Modeling the vertical elasticity property – Step 2: Modeling the horizontal elasticity property In the following subsections, we present a detailed description of these steps. 740 4.1 I. Abbassi et al. Modeling the Vertical Elasticity Property As stated in [4], the vertical elasticity is a rename of scalability. In fact, it is used to scale-up or down software applications deployed in Cloud by adding new resources and removing already used ones. The resources can be deplored in the Cloud such as (PFOS) software, hardware, database, and so on. In this work, we focus on the software resources. As claimed in [8], composite PFOS software can be scaled up and down automatically using the following operations: – create: an operation for the creation of a new PFOS software. – destroy: an operation for the deletion of an existing PFOS software. – bind: an operation for the deﬁnition of a binding between two exiting PFOS software. – unbind: an operation for the deletion of an existing binding. The bind operation is used to deﬁne the binding relation between created software. The main purpose behind the use of the unbind operation is to release (delete) all of the binding relations of an uninstalled software to be removed later. Fig. 9. The VElasticityMachine description To formally specify the vertical elasticity property for composite PFOS software, we created the new Event-B machine VElasticityMachine. This new machine sees the CP F OSScontext context. It reﬁnes the CPFOSSmachine machine by introducing a set of new events and variables (see Fig. 9). The abstract variables of CPFOSSmachine, CS, states, SB and ports, are respectively replaced in the reﬁned VElasticityMachine machine with the following ones: CS1, states, SB1 and ports1. This replacement process is strongly required because the newly created events of the VElasticityMachine machine are not able to modify the variables of CPFOSSmachine. In addition to typing invariants (used to specify the type of each variable in the VElasticityMachine), a set of gluing invariants are also deﬁned. These particular gluing invariants deﬁne an A Formal Approach for Correct Elastic PFOS Composition in Cloud 741 Fig. 10. The formalization of the vertical elasticity operations with Event-B. equality relation between the abstract and concrete variables (glu1, glu2, glu3, and glu4). The vertical elasticity operations are formally speciﬁed as events (see Fig. 10). These events are deﬁned while reﬁning the CPFOSSmachine. The create event allows to add new components to the composite software. The added components are initially set to the uninstalled state. The bind event is used to deﬁne the required bindings between the new added components and some existing ones. In some cases, it is necessary to remove some components and their associated bindings using the unbind and the destroy events. The guards grd1 and grd2 of destroy event state that the only way to destroy a software is to uninstall it while releasing all of its binding relations using the unbind event. 4.2 Modeling the Horizontal Elasticity Property As we explained in the introduction, the horizontal elasticity is another fundamental property provided by the Cloud paradigm. Such a property is used basically to increase or decrease the capacity of the deployed software applications by adding new copies of existing components, while removing unnecessary ones. More precisely, it is implemented using two operations: duplication and consolidation. 742 I. Abbassi et al. The duplication operation allows to increase the capacity of the composite softwares by duplicating some of its components. It can be considered as a special form of creating a component that is a copy of an existing one. The duplication of a given component implies the automatic duplication of all its bindings. The consolidation operation allows to decrease the capacity of the composite softwares through the deletion of unnecessary components copies. It can be considered as a special form of destroying a component, which is a copy of an existing one. The consolidation of a given component implies the consolidation of all its bindings. Fig. 11. The formalization of the duplication operation. To formally specify the horizontal elasticity property for composite PFOS software, we created the new Event-B machine HElasticityM achine. This new machine sees the CP F OSScontext context. It reﬁnes the VElasticityMachine machine by introducing a variable named copies and reﬁning the create and destroy events. This new variable is deﬁned as a function from the set CS1 in P(CS1). It determines the set of all the copies of the exiting components. The purpose behind the reﬁnement of the create and destroy events is to model the duplication and consolidation operations. It should be emphasized that the events create and destroy are already deﬁned in the HElasticityM achine. The grd3 and grd4 guards of the duplicate event (see Fig. 11) express that the component to be duplicated (component) and the one to be created (T oBeCreated) shall provide and require exactly the same ports. The substitution action act3 of the duplication event adds a new copy (T oBeCreated) of component. The binding relations of such an added copy are those of duplicated component (see act4, Fig. 11). The grd3 guard of the consolidate event (see Fig. 12) states that the component (speciﬁed by the input parameter component) to be removed is a copy of another existing one (denoted by the parameter original). The substitution actions of the consolidation event are those of the destroy event. A Formal Approach for Correct Elastic PFOS Composition in Cloud 743 Fig. 12. The formalization of the consolidation operation. 5 Correctness Verification and Validation In the previous two sections, we ﬁrst proposed an Event-B model for verifying PFOS software composition correctness. Then, we have extended this model to cover the correctness of elasticity properties. The consistency of our PFOS software composition model and its extended version is mandatory in order to meet the attended correctness veriﬁcation needs of the PFOS software composition and its elasticity properties. The adopted veriﬁcation approach comprises two steps: – Step 1: we use a proof-based veriﬁcation. – Step 2: we use an animation-based veriﬁcation using ProB model-checker. The following subsections expose a detailed description of these steps. 5.1 Proof-Based Verification We have succeeded to combine the modeling and the proof-based veriﬁcation to ensure the consistency of the Event-B models of PFOS software composition and the elasticity properties. The veriﬁcation activity is based on the integrated proof of the Rodin platform. The proof-based veriﬁcation consists in discharging a set of proof obligations (PO). It guarantees that: – The initialization of a machine leads to a state where the invariant is valid. – Assuming that the machine is in a state where the invariants are preserved, every enabled event leads to a state where the invariants are still preserved. Rodin generates a set of proof obligations for every invariant that can be aﬀected by an event, i.e. the invariant contains variables that can be changed by an event. The name of the proof obligation is then “evt/label/INV”. It can be either automatically/interactively discharged (marked with ), or undischarged (marked with ). The symbol “A” means that the PO is automatically discharged. The goal of such a proof is to assert that when all aﬀected variables are replaced by new values from the actions, the invariant still holds. Figure 13 reports the POs that are generated while proving the consistency of the CP F OSSmachine. All of these POs are discharged using the Rodin provers. 744 I. Abbassi et al. Fig. 13. All of the proof obligations of the CP F OSSmachine machine are discharged We used the concept of reﬁnement to model the elasticity properties by reﬁning the composite PFOS software formalization. The concept of reﬁnement allowed us to gradually introduce more details into a model. In order to ensure a correct reﬁnement of the CP F OSSmachine, we must prove two things: – The concrete events can only occur when the abstract ones occur. – If a concrete event occurs, the abstract event can occur in such a way that the resulting states correspond again, i.e. the gluing invariant remains true. The ﬁrst condition concerns the guard strengthening of the V Elasticity M achine. The goal of such a condition is to check if the V Elasticity M achine behaves in a way that corresponds to the behavior of the CP F OSSmachine. Consequently, several POs are generated with the following form: cEvent/aGrd/GRD where aGrd is an abstract guard. For instance, the POs shown in Fig. 14a state that the concrete events install and uninstall of the V ElasticityM achine can only occur when the abstract ones occur. The second condition is related to the gluing invariant preservation by concretes. The goal of such a condition is to prove that the invariant of the concrete machine is valid when each occurrence of a modiﬁed variable is replaced by its new value. The resulting proof obligations have the following label form: cEvt/cInv/INV where cEvt is a concrete event and cInv is a concrete invariant (deﬁned on the concrete variables). For instance, the proof obligations “destroy/glu1/INV” and “destroy/glu2/INV” (Fig. 14b) state that when the concrete event “destroy” of the V ElasticityM achine machine occurs, the gluing invariants “glu1” and “glu2” can remain false. Similarly, the gluing invariants “glu1” and “glu2” can remain false when the create event of the V ElasticityM achine is executed. This is justiﬁed by the fact that the proof obligations “create/glu1/INV” and “create/glu2/INV” are discharged neither automatically nor interactively (see Fig. 14b). This means that the V ElasticityM achine is not correct. A Formal Approach for Correct Elastic PFOS Composition in Cloud 745 Fig. 14. Some proof obligations of the VElasticityMachine machine Table 1. Summary of the results of the proof-based veriﬁcation Machines/contexts POs Proved Unproved PFOSSmachine 9 9 PFOSScontext 0 0 0 0 CPFOSSmachine 39 39 0 CPFOSScontext 0 0 0 VElasticityMachine 51 47 4 HElasticityMachine 11 11 0 Summarizing, the provers generate 110 POs (see Table 1). We notice that the work on POs is in progress: at this time, 95 of them are automatically or interactively discharged. The proof of 4 POs remains to be done. That does not mean that they are false, but that the Rodin provers simply don’t succeed in demonstrating the rule: it may be due to the fact that some events are not handled in an eﬃcient manner by the provers, or due to the fact that the heuristics used for the proof are not eﬃcient enough in this case. An eﬀort remains to be done to manually demonstrate the unproved POs. 5.2 Animation-Based Verification As shown in the previous section, the provers fail to discharge automatically and interactively several POs. For this purpose, we complement the proof-based veriﬁcation with an animation process by using ProB [16]. Overview of ProB. ProB is basically a PFOS software that can be composed with the Rodin platform to assist the designers in tracing possible speciﬁcation errors causing the failure of the provers and then prove those POs. The counterexample generated by ProB that shows situations where the invariant is not 746 I. Abbassi et al. satisﬁed was used as a guide to correct our model and then discharge some proof obligations. The constraint-solving capabilities of ProB can also be used for model ﬁnding, deadlock checking and test-case generation. Depending on the situation in hand, we have made several modiﬁcations on the Event-B model related to the invariant, guard or to the event’s action. Animation. The animation is performed on a concrete Event-B model. For this purpose, we substantiate our abstract model with the Wordpress application. This is done by reﬁning the HElasticityM achine machine and extending the CP F OSScontext context in order to specify the main elements of such a particular application. The extended context, WordPressContext, is shown in Fig. 15. It is seen by the reﬁned Machine (W ordP ressM achine). Fig. 15. The WordPressContext description We start the animation step by executing the INITIALISATION event. Afterward, we can interact with the model by triggering events. This is done by double-clicking on an enabled event or by right-clicking it and selecting a set of parameters, if applicable. We ﬁrst trigger the event create with the parameter: Apache2. Figure 16 reports the results of triggering creation event. These results indicate that gluing invariants glu1 and glu2 are violated. This conﬁrms the failure of the Rodin Provers while discharging the following POs: “create/glu1/INV” and “create/glu2/INV”. To repair these speciﬁcation errors, we modify the gluing invariants as follows: – – – – glu1: glu2: glu3: glu4: CS ⊆ CS1 states ⊆ states1 ports ⊆ ports1 SB ⊆ SB1 With these redeﬁnitions, we succeeded to discharge the four undischarged POs related to the reﬁnement of the CP F OSSmachine. A Formal Approach for Correct Elastic PFOS Composition in Cloud 747 Fig. 16. ProB signals invariants violation 6 Related Work Diﬀerent approaches have been proposed to solve the conﬁguration problem of software. The authors of [17] propose empirical data for the real power of open source style of software development. They mainly investigate the beneﬁts of the structural code analysis. As claimed in [17], the quality of the code produced by an open source is lower than that expected from an industrial standard. In [6], the authors developed a modular package management allowing for pluggable dependency solvers. They claim that this is the path that leads to the next generation of package managers that will deliver better results, accept more expressive input languages, and can be easily adaptable to new platforms. In [5,8,18], the authors focus on studying the deployment problem and the automatic reconﬁguration of software in cloud environment. First, they propose a component-based model for cloud, called Aeolus, slightly inspired from the Fractal model. Then, they propose an algorithm for the veriﬁcation and the construction of a correct conﬁguration of PFOS software to be deployed in the cloud environment. The veriﬁcation strategy conducted by such an algorithm is based on constructing all possible correct conﬁgurations of the PFOS software by applying a set of operators, namely create, destroy, bind, unbind and stateChange (an operation used to change the state of software). Then, it veriﬁes whether the conﬁguration to be checked is one of the constructed conﬁgurations. If so, the conﬁguration is valid, otherwise it is invalid. In [19], the authors propose an open-source toolkit tool, called CPAchecker, for the veriﬁcation of conﬁgurable software. They evaluated the eﬃciency of the CPAchecker tool for 748 I. Abbassi et al. software-veriﬁcation benchmarks coming from literature. The main weak point of the CPAchecker tool is that it is based on model-checking. In [20], a Vienna Platform for Elastic Processes (ViePEP) is proposed. This platform allows to construct elastic processes in cloud environments. Moreover, it can be used for resources consumption optimization by using a set of elasticity actions. Extensions of the ViePEP platform are proposed by [21,22]. These extensions are knowledge-based prediction, scheduling and resources-allocation algorithms. The authors of [4] proposed the elasticity as a service (ElaaS) concept that is implemented as a SaaS application. This concept can be used in cloud environments. The work presented in [23] considers the elasticity at both the service and application levels. Nevertheless, the correctness of the proposed elasticity mechanisms is not proved since the approach is not based on a formal model. More recently, the authors of [24] proposed an approach for verifying and deploying elastic service component architecture (SCA)-based applications using the Event-B formal method. In fact, they formally model the component artifacts using Event-B and they deﬁne the Event-B events that model the elasticity mechanisms (scaling up and down) for component-based applications. The main shortcoming of [24] is that it basically does not support the port capacity requirements. The work we proposed in this paper is new in the sense that it (1) tackles the problem of elasticity of the PFOS software applications at the SaaS level, (2) is based on a formal model and (3) proposes a formal veriﬁcation of the elasticity mechanisms. 7 Conclusion In this paper, we proposed a novel approach to ensure the correctness of elastic composite PFOS applications. The approach consists in a correct-byconstruction elastic composite PFOS applications model built on Event-B. This formal model explores four abstraction levels. At a ﬁrst level, we deﬁned an abstract model for the PFOS software. At a second level, we reﬁned this abstract model for the deﬁnition of the PFOS software composition process and its correctness requirements (capacity and dependency requirements). At a third level, we formally deﬁned the vertical elasticity mechanisms by reﬁning the composite PFOS software model further. The vertical elasticity mechanisms allow to scaleup and down a composite PFOS application by adding and removing components and bindings. At a fourth level, we extended the formalization of vertical elasticity capabilities with horizontal elasticity mechanisms that consist in duplication and consolidation operations. We have succeeded to combine the modeling and veriﬁcation activities to ensure the consistency of the Event-B models of PFOS software composition and the elasticity properties. The veriﬁcation activity is based on the integrated proof of the Rodin platform. We complemented this veriﬁcation activity with an animation process using the ProB model-checker to trace possible modeling errors. A Formal Approach for Correct Elastic PFOS Composition in Cloud 749 We are currently working on developing a tool that automates the Event-B based veriﬁcation process and an automatic deployment framework of elastic composite PFOS software applications. The proposal of a PFOS software selection method could be interesting extension to the proposed approach. References 1. Fox, A., Griﬃth, R., Joseph, A., Katz, R., Konwinski, A., Lee, G., Patterson, D., Rabkin, A., Stoica, I.: Above the clouds: a Berkeley view of cloud computing. Report UCB/EECS 28(13) 2009, Department of Electrical Engineering and Computer Science, University of California, Berkeley (2009) 2. Rimal, B.P., Choi, E., Lumb, I.: A taxonomy and survey of cloud computing systems. NCM 9, 44–51 (2009) 3. Dustdar, S., Guo, Y., Satzger, B., Truong, H.L.: Principles of elastic processes. IEEE Internet Comput. 15(5), 66–71 (2011) 4. Kranas, P., Anagnostopoulos, V., Menychtas, A., Varvarigou, T.: ElaaS: an innovative elasticity as a service framework for dynamic management across the cloud stack layers. In: 2012 Sixth International Conference on Complex, Intelligent and Software Intensive Systems (CISIS), pp. 1042–1049. IEEE (2012) 5. Di Cosmo, R., Mauro, J., Zacchiroli, S., Zavattaro, G.: Aeolus: a component model for the cloud. Inf. Comput. 239, 100–121 (2014) 6. Abate, P., Di Cosmo, R., Treinen, R., Zacchiroli, S.: MPM: a modular package manager. In: 14th International ACM SIGSOFT Symposium on Component Based Software Engineering (CBSE 2011) (2011) 7. Krueger, C.W.: Software reuse. ACM Comput. Surv. 24(2), 131–183 (1992) 8. Di Cosmo, R., Zacchiroli, S., Zavattaro, G.: Towards a formal component model for the cloud. In: Eleftherakis, G., Hinchey, M., Holcombe, M. (eds.) SEFM 2012. LNCS, vol. 7504, pp. 156–171. Springer, Heidelberg (2012). doi:10.1007/ 978-3-642-33826-7 11 9. Abrial, J.-R., Butler, M., Hallerstede, S., Voisin, L.: An open extensible tool environment for Event-B. In: Liu, Z., He, J. (eds.) ICFEM 2006. LNCS, vol. 4260, pp. 588–605. Springer, Heidelberg (2006). doi:10.1007/11901433 32 10. Smith, D., Milinkovich, M.: Eclipse: a premier open source community. Open Source Business Resource, July 2007 11. Wiegand, J., et al.: Eclipse: a platform for integrating development tools. IBM Syst. J. 43(2), 371–383 (2004) 12. Abrial, J.: Modeling in Event-B: System and Software Engineering. Cambridge University Press, Cambridge (2010) 13. Méry, D., Singh, N.K.: EB2C: a tool for Event-B to C conversion support. In: 8th IEEE International Conference on Software Engineering and Formal Methods (SEFM) Poster and Tool Demo submission. Published in a CNR Technical Report (2010) 14. Méry, D., Singh, N.K.: EB2J: code generation from Event-b to Java. In: SBMF - Brazilian Symposium on Formal Methods, CBSoft - Brazilian Conference on Software: Theory and Practice, Sao Paulo, Brazil (2011) 15. Di Cosmo, R., Zacchiroli, S., Trezentos, P.: Package upgrades in FOSS distributions: details and challenges. In: Proceedings of the 1st International Workshop on Hot Topics in Software Upgrades, p. 7. ACM (2008) 750 I. Abbassi et al. 16. Leuschel, M., Butler, M.: ProB: a model checker for B. In: Araki, K., Gnesi, S., Mandrioli, D. (eds.) FME 2003. LNCS, vol. 2805, pp. 855–874. Springer, Heidelberg (2003). doi:10.1007/978-3-540-45236-2 46 17. Stamelos, I., Angelis, L., Oikonomou, A., Bleris, G.L.: Code quality analysis in open source software development. Inf. Syst. J. 12(1), 43–60 (2002) 18. Di Cosmo, R., Mauro, J., Zacchiroli, S., Zavattaro, G.: Component reconﬁguration in the presence of conﬂicts. In: Fomin, F.V., Freivalds, R., Kwiatkowska, M., Peleg, D. (eds.) ICALP 2013. LNCS, vol. 7966, pp. 187–198. Springer, Heidelberg (2013). doi:10.1007/978-3-642-39212-2 19 19. Beyer, D., Keremoglu, M.E.: CPAchecker: a tool for conﬁgurable software veriﬁcation. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 184–190. Springer, Heidelberg (2011). doi:10.1007/978-3-642-22110-1 16 20. Schulte, S., Hoenisch, P., Venugopal, S., Dustdar, S.: Introducing the Vienna platform for elastic processes. In: Ghose, A., Zhu, H., Yu, Q., Delis, A., Sheng, Q.Z., Perrin, O., Wang, J., Wang, Y. (eds.) ICSOC 2012. LNCS, vol. 7759, pp. 179–190. Springer, Heidelberg (2013). doi:10.1007/978-3-642-37804-1 19 21. Hoenisch, P., Schulte, S., Dustdar, S., Venugopal, S.: Self-adaptive resource allocation for elastic process execution. In: 2013 IEEE sixth International Conference on Cloud Computing (CLOUD), pp. 220–227. IEEE (2013) 22. Hoenisch, P., Schulte, S., Dustdar, S.: Workﬂow scheduling and resource allocation for cloud-based execution of elastic processes. In: 2013 IEEE 6th International Conference on Service-Oriented Computing and Applications (SOCA), pp. 1–8. IEEE (2013) 23. Tsai, W.T., Sun, X., Shao, Q., Qi, G.: Two-tier multi-tenancy scaling and load balancing. In: 2010 IEEE 7th International Conference on e-Business Engineering (ICEBE), pp. 484–489. IEEE (2010) 24. Graiet, M., Hamel, L., Mammar, A., Tata, S.: A veriﬁcation and deployment approach for elastic component-based applications. Formal Aspects Comput. 1–25 (2017)

1/--страниц