close

Вход

Забыли?

вход по аккаунту

?

978-3-319-69462-7 46

код для вставкиСкачать
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.
Different requirements must be considered while configuring PFOS software. These requirements can be classified 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 verification. It starts by abstractly specifying the
main concepts of PFOS software, and then refining 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 refinements 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 · Verification
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 different 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 defined 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.
Different requirements must be considered while configuring composite PFOS
software [5]. These requirements can be classified into two classes: dependency
and capacity requirements. The dependency requirements are defined 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 defined 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 verification 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 verification of such applications based on the EventB formal method [12] and combining proof-based models with model checking
to provide a more complete verification. Event-B is chosen because of its capability to effectively master the complexity of the system design using stepwise
refinement. The step-wise refinement method produces a correct specification by
construction since at each step the different properties of the system are formally
proven. Moreover, Event-B tools can be used to perform an incremental verification by checking the defined 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 defines
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 verified, 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 refine this model through several steps to model the (horizontal
and vertical) properties and their correctness requirements. The consistency verification 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 first 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 finite 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 first 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 refining 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 first clause, VARIABLES, represents
the defined 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
fired when its guards is evaluated to true. The events occurring in an Event-B
model affect 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 refinement 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 satisfies 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 first level, we abstractly specify the basic concepts of PFOS software. At the second level, we refine such
an abstract model by introducing the software dependency concept in order to
formally define 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 configuration.
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), specifies 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 defines
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 defined 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 defined 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. Different requirements shall be
satisfied 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 satisfied by the composite PFOS software.
The first three requirements define dependency constraints between software
components. The requirement REQ4 defines a set of upper-bound capacity constraints on the provided software ports. The last one defines 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 first extend the PFOSScontext (see Fig. 6). We introduced a finite set, P ORT , to denote all the ports that
are provided or required by software. The requiredP orts function defines the set
of ports that are required by a component in a given state. The providedP orts
function defines the set of ports that are provided by a component in a given
state. The portsCapacity function defines 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 refine 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 define 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 defined using two invariants, namely type2 and type3 (see
Fig. 7). For the sake of clarity, the invariants, defined 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
verification 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 definition of a binding between two exiting PFOS
software.
– unbind: an operation for the deletion of an existing binding.
The bind operation is used to define 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 refines 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 refined 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 defined. These particular gluing invariants define 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 specified as events (see Fig. 10).
These events are defined while refining 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 define 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 refines the VElasticityMachine
machine by introducing a variable named copies and refining the create and
destroy events. This new variable is defined 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 refinement 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 defined 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 (specified 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 first 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 verification needs of the PFOS software composition
and its elasticity properties. The adopted verification approach comprises two
steps:
– Step 1: we use a proof-based verification.
– Step 2: we use an animation-based verification 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 verification
to ensure the consistency of the Event-B models of PFOS software composition
and the elasticity properties. The verification activity is based on the integrated
proof of the Rodin platform. The proof-based verification 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 affected
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 affected 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 refinement to model the elasticity properties by
refining the composite PFOS software formalization. The concept of refinement
allowed us to gradually introduce more details into a model. In order to ensure
a correct refinement 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 first 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 modified 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 (defined 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 justified 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 verification
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 efficient manner by the provers, or due to the fact that the heuristics
used for the proof are not efficient enough in this case. An effort 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
verification 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 specification
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.
satisfied 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 finding, deadlock checking and test-case generation. Depending on the
situation in hand, we have made several modifications 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 refining 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 refined 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 first 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 confirms the failure of the Rodin Provers while discharging the following POs: “create/glu1/INV”
and “create/glu2/INV”. To repair these specification errors, we modify the gluing invariants as follows:
–
–
–
–
glu1:
glu2:
glu3:
glu4:
CS ⊆ CS1
states ⊆ states1
ports ⊆ ports1
SB ⊆ SB1
With these redefinitions, we succeeded to discharge the four undischarged POs
related to the refinement 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
Different approaches have been proposed to solve the configuration 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 benefits 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 reconfiguration 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 verification and the
construction of a correct configuration of PFOS software to be deployed in the
cloud environment. The verification strategy conducted by such an algorithm is
based on constructing all possible correct configurations 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 verifies
whether the configuration to be checked is one of the constructed configurations. If so, the configuration is valid, otherwise it is invalid. In [19], the authors
propose an open-source toolkit tool, called CPAchecker, for the verification of
configurable software. They evaluated the efficiency of the CPAchecker tool for
748
I. Abbassi et al.
software-verification 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 define 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 verification 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 first level, we defined an
abstract model for the PFOS software. At a second level, we refined this abstract
model for the definition of the PFOS software composition process and its correctness requirements (capacity and dependency requirements). At a third level,
we formally defined the vertical elasticity mechanisms by refining 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
verification activities to ensure the consistency of the Event-B models of PFOS
software composition and the elasticity properties. The verification activity is
based on the integrated proof of the Rodin platform. We complemented this
verification 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 verification 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., Griffith, 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 reconfiguration
in the presence of conflicts. 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 configurable software verification. 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.: Workflow 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 verification and deployment approach for elastic component-based applications. Formal Aspects Comput. 1–25
(2017)
Документ
Категория
Без категории
Просмотров
0
Размер файла
3 424 Кб
Теги
978, 69462, 319
1/--страниц
Пожаловаться на содержимое документа