Stéphanie Challita

Faiez Zalila

Philippe Merle

Specifying Semantic Interoperability between Heterogeneous Cloud Resources with the FCLOUDS Formal Language

Keywords: Multi-Clouds, OCCI, Formal Language, Formal Verification, Alloy, Interoperability

With the advent of cloud computing, different cloud providers with heterogeneous services and Application Programming Interfaces (APIs) have emerged. Hence, building an interoperable multi-cloud system becomes a complex task. Our idea is to design FCLOUDS framework to achieve semantic interoperability in multi-clouds, i.e., to identify the common concepts between cloud APIs and to reason over them. In this paper, we propose to take advantage of the Open Cloud Computing Interface (OCCI) standard and the Alloy formal specification language to define the FCLOUDS language, which is a formal language for specifying heterogeneous cloud APIs. To do so, we formalize OCCI concepts and operational semantics, then we identify and validate five properties (consistency, sequentiality, reversibility, idempotence and safety) that denote their characteristics. To demonstrate the effectiveness of our cloud formal language, we present thirteen case studies where we formally specify infrastructure, platform, Internet of Things (IoT) and transverse cloud concerns. Thanks to the Alloy analyzer, we verify that these heterogeneous APIs uphold the properties of FCLOUDS and also validate their own specific properties. Then, thanks to formal transformation rules and equivalence properties, we draw a precise alignment between our case studies, which promotes semantic interoperability in a multi-cloud system.

I. INTRODUCTION

The "Multi-cloud" computing, which aims to combine different offerings or migrate applications between different cloud providers, is becoming trendy. Multi-clouds improve cloud application performance and costs, and ensure their resiliency in case of outages [START_REF] Petcu | Multi-Cloud: Expectations and Current Approaches[END_REF]. But with the advent of cloud computing, different cloud providers with heterogeneous services and Application Programming Interfaces (APIs) have emerged. This is quite challenging for the implementation of multi-cloud systems. Several multi-cloud interoperability solutions have emerged to address this challenge. We mainly identify four strategies from the literature [START_REF] Challita | Towards Formal-based Semantic Interoperability in Multi-Clouds: The fclouds Framework[END_REF]: i) services such as Kaavo and RightScale, ii) programming libraries such as jclouds and fog, iii) modeling languages such as CloudML [START_REF] Ferry | CloudMF: Model-Driven Management of Multi-Cloud Applications[END_REF] and SALOON [START_REF] Quinton | SALOON: A Platform for Selecting and Configuring Cloud Environments[END_REF] and iv) standards such as Open Cloud Computing Interface (OCCI 1 ) and Topology and Orchestration Specification for Cloud Applications (TOSCA 2 ). Regardless of its abstraction level, a solution for multi-cloud interoperability 1 http://occi-wg.org/ 2 https://www.oasis-open.org/committees/TOSCA must achieve a compromise between defining the common cloud principles and supporting any kind of cloud resources. This frustrating situation calls for more depth about the cloud providers' semantics to reason about the common principles that interoperability solutions must adhere to.

Our vision is to build FCLOUDS, a framework for semantic interoperability in a multi-cloud context [START_REF] Challita | Towards Formal-based Semantic Interoperability in Multi-Clouds: The fclouds Framework[END_REF]. By semantic interoperability we mean to identify the similarities and differences between cloud APIs concepts and to reason over them. Our framework contains a catalog of cloud APIs that are precisely described. It will help the cloud customer to understand how to migrate from one API to another, thus to promote semantic interoperability. To implement the formal language that will encode all the APIs of our FCLOUDS framework, we advocate the use of formal methods, i.e., techniques based on mathematical notations. They will allow us to rigorously encode cloud concepts and behaviour, validate desired and/or imposed cloud properties and finally define formal transformation rules between cloud concepts. We adopt the concepts of the OCCI common standard to define the formal language of the FCLOUDS framework. We choose to formalize OCCI with Alloy, a lightweight promising formal specification language designed by Daniel Jackson from the Massachusetts Institute of Technology (MIT) [START_REF] Jackson | Software Abstractions: logic, language, and analysis[END_REF].

The key contribution of this paper is specifying semantic interoperability between heterogeneous cloud resources using the FCLOUDS formal language. The remainder of this paper is structured as follows. In Section II we explain the motivations behind our contribution. In Section III, we present our contribution, the FCLOUDS language that specifies OCCI core concepts and operational semantics, and verifies properties on how OCCI should work. In Section IV, we illustrate the use of our formal language with a series of thirteen examples. Finally, we discuss related work in Section V and we conclude in Section VI.

II. MOTIVATIONS

Multi-cloud applications exist for several reasons. Among them we mention the optimization of the resource provisioning costs and the enhancement of the application quality of service. Apart from these two goals, the cloud developer should also comply to the different requirements of each service of the application. For instance, a web server interface should be made available 24/7 for users, so it is highly recommended that the cloud developer provisions cloud resources from at least two heterogeneous providers to maintain the availability of the web server interface in case of an outage. Unfortunately, this is not a straightforward task. To illustrate the complexity faced when building a multi-cloud system, we introduce an example scenario of a developer who would like to provision virtual machines from two clouds, Google Cloud Platform (GCP) and DigitalOcean. Each of these two cloud providers is based on its own REpresentational State Transfer (REST) API, so the developer is faced to two heterogeneous APIs implementing different concepts. For instance, GCP refers to its compute service as "instance", whereas DigitalOcean calls it "droplet".

To address the problem of interoperability in multi-clouds, we identified four strategies that were used in the literature:

1) services to offer a unique interface that handles the heterogeneity of different APIs, i.e., that only masks the problem but does not semantically resolve it, 2) programming libraries to allow developers to achieve interoperability at their code level, without necessarily understanding the underlying concepts of the API, 3) modeling languages to describe with an appropriate abstraction, a part of the cloud domain that was relevant at the moment of the definition of the modeling language. However, the designers require changing their modeling language, i.e., the metamodel, at each time they want to support more cloud concepts. As for the user, he/she is unable to add the missing concepts that he/she needs, 4) and standards to provide some concepts to be commonly used by cloud providers. However, standards may forget to define some useful concepts or may be overcrowded by useless concepts. Moreover, standards are accompanied by ambiguous documentations written in natural language.

Regardless of their strategy, the heterogeneity and the lack of formalization of multi-cloud interoperability solutions complicate the understanding of the cloud common principles. Our vision is to build a framework for semantic interoperability in a multi-cloud context. We refer to this framework as the FCLOUDS framework and we previously introduced it in [START_REF] Challita | Towards Formal-based Semantic Interoperability in Multi-Clouds: The fclouds Framework[END_REF]. To implement FCLOUDS, we advocate the use of a formal language that provides the formal specifications of the FCLOUDS cloud APIs. Formal methods are techniques that are based on mathematical notations and they will allow us to rigorously encode the underlying semantics of cloud APIs concepts through formal specifications. Formal specifications remove ambiguities, since unlike natural language statements, mathematical specifications are only interpreted in one way, the correct one. Formal methods allows us to effectively reason on the structure and behaviour of the encoded concepts, by using a model checker verifying cloud properties, i.e., constraints denoting characteristics of cloud configurations and/or operations. This focuses on what a system should do rather than how to accomplish it. Being precisely specified, verified and correctly understood, the cloud APIs can be correctly compared. For this, we will define formal transformation rules between their concepts, and verify equivalence properties. The developers will hence be able to achieve semantic interoperability in a multi-cloud system.

We argue it is more advantageous and reliable to adopt an open standard to define the formal specification language of all FCLOUDS APIs, instead of writing a language from scratch. The most popular standard is OCCI since it is used by the private European Grid Infrastructure Federated Cloud (EGI FC) and it was successfully extended to support heterogeneous aspects of the cloud domain, through OCCI Infrastructure [START_REF] Nyrén | Open Cloud Computing Interface -Infrastructure[END_REF], OCCI Platform [START_REF] Metsch | Open Cloud Computing Interface -Platform[END_REF], etc. In fact, OCCI defines a generic and extensible model for cloud resources and a RESTful API for efficiently accessing and managing resources. This facilitates interoperability between clouds that are implemented as OCCI extensions, i.e., specified by the same OCCI resource model, and accessed by the same REST API. Today, there are several schools for formal methods like Petri nets, languages based on logic, semantics programs, automata theory, etc. Choosing the appropriate notation is critical in order to find the right compromise between formalization and complexity. Meanwhile, Alloy is becoming increasingly popular among formal methods, as it is a relational, first-order logic language, with well-thought out syntax and model visualization features. It allows us to specify complex systems in a streamlined way, by describing concepts and constraints. The specifications are translated into first-order logic expressions that can be automatically solved by the Alloy analyzer, a model checker using SATisfiability (SAT) solvers. The latter allows automatic verification of a system model, to ensure its consistency and other desired properties, thus to guarantee its correctness. Therefore, we choose to formalize OCCI using a lightweight promising formal language, the Alloy specification language [START_REF] Jackson | Software Abstractions: logic, language, and analysis[END_REF]. We refer to this formal specification as the FCLOUDS language.

III. THE FCLOUDS FORMAL LANGUAGE

The present contribution aims to define the formal language of the FCLOUDS framework. Therefore, we propose the FCLOUDS language, an Alloy-based formal language which makes explicit OCCI core concepts [START_REF] Nyrén | Open Cloud Computing Interface -Core[END_REF] and OCCI REST operations [START_REF] Nyrén | Open Cloud Computing Interface -HTTP Protocol[END_REF], as well as the underlying properties. In this section, we present a subset of the FCLOUDS static and operational semantics. For more details, the entirety of this language is available in the OCCIware official website [START_REF] Ahmed-Nacer | OCCI Behavioural Model[END_REF] and in the OCCIware GitHub repository (see AVAILABILITY section).

A. Specifying FCLOUDS static semantics

The static semantics of FCLOUDS correspond to the formalization of the OCCI core concepts [START_REF] Nyrén | Open Cloud Computing Interface -Core[END_REF] in Alloy. We use a strategy based on Time dimension [START_REF] Jackson | Software Abstractions: logic, language, and analysis[END_REF]. It allows us to distinguish between mutable fields, i.e., those that are related to Time, and immutable ones, i.e., those that are not related to Time. Table I presents a summary of the FCLOUDS language concepts and due to space limitations, we detail in the following only four of these concepts in Alloy:

• ENTITY represents an abstract type defining the set of all resources and links. The keyword extends in Alloy indicates that a set is declared as a subset of another one and that it will form, with other subsets similarly declared, a partition of the set it extends. • CONFIGURATION is the abstraction of an OCCI-based running system. Modeling a configuration offline allows designers to think and analyze their cloud systems without having to deploy them concretely in the clouds [START_REF] Merle | A Precise Metamodel for Open Cloud Computing Interface[END_REF].

The use field, which is the set of extensions used in a configuration, is immutable because the extensions cannot be added on removed at runtime. Please refer to [START_REF] Ahmed-Nacer | OCCI Behavioural Model[END_REF] for the specification of the EXTENSION concept. The resources field is mutable.

B. Specifying FCLOUDS operational semantics

The operational semantics of FCLOUDS correspond to the formalization of the informal OCCI behavioural specification detailed in [START_REF] Nyrén | Open Cloud Computing Interface -HTTP Protocol[END_REF]. It mainly includes different REST operations, i.e., CREATE, RETRIEVE, UPDATE, DELETE. In this idiom, these operations are modeled as predicates that specify the relationship between pre-state, i.e., the state before the operation is called and post-state, i.e., the state after the operation is completed. To do so, Time is added at the end of each mutable field to represent the state concept. To be more specific, an operation op will be specified using a predicate: pred op[...,t,t':Time] ..., with two special parameters t and t' denoting, respectively, the pre-and post-states [START_REF] Garis | Specifying UML Protocol State Machines in Alloy[END_REF]. The core of each predicate is carried out by defining explicitly pre-and post-conditions, which are constraints that must be satisfied before executing the operation and after the operation is finished respectively. The following predicate shows how we formally specify the creation of a resource. At time t, we specify that our configuration, passed as argument to the predicate, does not have a resource with the id passed as a predicate argument (cf. line 3). The no keyword expresses the null cardinality of the empty resource set that satisfies the constraint resource.id = resourceId. The dot in resource.id is the standard notation for accessing a feature, or attribute, of an instance of a class. As well, we specify that the kind and the mixins of the resource we want to create, are contained in our configuration extensions (cf. lines 4 and 5). At time t', we add to our configuration resources, one resource with the id, kind and mixins, passed as argument to the predicate (cf. lines 7 to 11). Eight operations were defined to the CONFIGURATION concept of FCLOUDS, as depicted in Table II.

C. Identifying & validating FCLOUDS properties

Using formal languages has the advantage of allowing reasoning over concepts and operational semantics for a better understanding of their semantics and how they work. Therefore, once the FCLOUDS formal language has been specified, we proceed by the definition of some structural and behavioural properties to ensure its correctness and to express its desired/required behaviour. We formally encode the consistency, sequentiality, reversibility, idempotence and safety. The last two properties are classified into a broader property which is the conformance to HTTP 2 protocol [START_REF] Belshe | Hypertext Transfer Protocol Version 2 (HTTP/2)[END_REF]. Then, using Alloy analyzer, we validate that these properties adequately hold in our FCLOUDS static and operational semantics. We specify a big scope, i.e., we bound the number of atoms allowed for each signature to 10, in order to be confident that the assertion holds. If no counterexamples are returned with such big scope, we can be confident that our language reflects the desired semantics.

1) Consistency: FCLOUDS language is consistent if it does not contain any contradictory constraints, so its concepts can be instantiated and each cloud API operation can be executable. We can also analyze what could not be instantiated, thus can't be deployed in real-world. In these cases, our formal language might be over-constraining so we deem necessary to relax some constraints. The CreateResourceIsConsistent assertion below can't be shown to have a counterexample. Hence, it asserts the existence of a valid configuration that meets the pre-and post-conditions of Create Resource, i.e., it is consistent and expresses the desired behaviour. Note that to model finite execution traces, Alloy defines a library util/ordering that provides useful relations to manipulate the total order of Time concept, namely first to denote the first time, and next, a binary relation that, given a time returns the following time in the order.

The FCLOUDS static semantics and all OCCI REST operations were proven to be consistent, as shown in Table II. However, the notion of consistency is basic and does not suffice in order to validate our FCLOUDS language. There are other examples of reliable verification and validation tasks that can be performed on pairs of operations such as sequentiality and/or reversibility of operations:

2) Sequentiality: two cloud API operations are sequential when one cannot happen if the other one did not happen at the time before. For example, the developer can adapt the performance of a virtual machine only if it was created before.

It is explicitly stated in the informal specification of OCCI that Update Resource operation should be preceded by Retrieve Resource operation: "Before updating a resource instance it is RECOMMENDED that the client first retrieves the resource instance" [START_REF] Nyrén | Open Cloud Computing Interface -HTTP Protocol[END_REF]. We also explicitly specify in FCLOUDS that Retrieve Resource operation must be preceded by Create Resource operation (as shown in the following assertion), Update Link by Retrieve Link and Retrieve Link by Create Link. 3) Reversibility: two cloud API operations are reversible when they contain inverse mathematical logic. For example, de-provisioning a virtual machine reverses the operation of provisioning it. In OCCI, Create Resource and Delete Resource, Create Link and Delete Link are reversible. The following assertion, which is checking that Create Resource is reversed by Delete Resource, was proven to be valid. 4) Conformance to HTTP 2 protocol: as OCCI is a REST architecture that conforms to the HTTP protocol, it must conform to its specification too. Therefore, there are some imposed properties we must have in any REST-based systems so they must be checked in the FCLOUDS language. According to the request for comments (RFC) HTTP 2 [START_REF] Belshe | Hypertext Transfer Protocol Version 2 (HTTP/2)[END_REF], we identified two properties of the HTTP methods and we verified in our formal language that the appropriate pairs of operations respect these properties.

• Idempotence: a method is idempotent when it always produces the same server external state even if applied several times [START_REF] Belshe | Hypertext Transfer Protocol Version 2 (HTTP/2)[END_REF]. In HTTP, GET, PUT and DELETE methods are idempotent. In OCCI, Retrieve operation is associated with a GET HTTP method, Create operation is a PUT HTTP method and Delete operation is a DELETE HTTP method. So we verify in our formal language that Retrieve Resource, Retrieve Link, Create Resource, Create Link, Delete Resource and Delete Link are idempotent. For example, as a result, the following assertion is valid: This assertion checks if creating a resource induces the same configuration at times t.next and t.next.next. In contrast, an Update operation, referred to as a POST in HTTP, is not idempotent.

• Safety: a method is safe when it does not change the external server state [START_REF] Belshe | Hypertext Transfer Protocol Version 2 (HTTP/2)[END_REF]. It mainly concerns the retrieval of information. A safe method is necessarily an idempotent method, but not the reverse way. In HTTP, a GET method is safe. Therefore, in FCLOUDS, we check that Retrieve Resource, Retrieve Link and Retrieve Collection 3 respect this property, so they do not change the cloud configuration. An example of a safe operation is detailed below: This assertion checks if a configuration remains the same at time t, i.e., before retrieving the resource, and at time t.next, i.e. after retrieving the resource. Table II lists all the operations that we have modeled, as well as all the properties that have been checked. The "+" symbol represents the operations or the pairs of operations that should fulfill a property, while the "-" represents the operations or the pairs of operations that they should not fulfill this property. By using the Alloy analyzer, we check that the FCLOUDS language, the core language of our FCLOUDS framework, correctly reflects these properties, so we guarantee that it is valid and that we implemented the desired behaviour.

IV. VALIDATION

To validate the effectiveness of our formal language, we demonstrate how it can be easily adapted to different concerns by providing formal specifications in Alloy for OCCI extensions from different cloud application domains. Therefore, we have surveyed the literature to find all the already published OCCI extensions. We have identified thirteen works that belong to IaaS, PaaS and Internet of Things (IoT) domains, as well as to transverse cloud concerns. As a working hypothesis, we have assumed that all these extensions are correct as they were already accepted through a peer review process. Our validation allows us to confirm:

1) the power of expression of our FCLOUDS language (Subsection A), 2) the validity of the FCLOUDS behaviour we defined, on all of the OCCI extensions (Subsection B), 3) the ability of our language to define domain-specific properties (Subsection C), and, 4) its ability to encode equivalence predicates, i.e., transformation rules between heterogeneous concepts, and to define properties of the equivalence (Subsection D).

A. Catalog of cloud formal specifications

Thanks to our proposed formal language, we succeeded to precisely encode thirteen heterogeneous APIs, as shown in Table III that gives a summary of our FCLOUDS framework dataset. For each concept of our language, Table III provides the number (#) of instances of this concept present in the dataset. The last line provides the total of FCLOUDS concepts present in the dataset. Due to space constraints, we give only excerpts of the formal APIs' specifications, implemented beforehand as OCCI extensions. Full specifications for each of these thirteen extensions can be found in the supplemental material (see AVAILABILITY section). 1) OCCI INFRASTRUCTURE [START_REF] Nyrén | Open Cloud Computing Interface -Infrastructure[END_REF] 2) OCCI CRTP [START_REF] Drescher | Open Cloud Computing Interface -Compute Resource Template Profile[END_REF] is an OCCI-based extension that defines a set of preconfigured instances of the OCCI COMPUTE resource type. 3) DOCKER is a lightweight container for deploying and managing applications. Docker is implemented as an extension of OCCI in [START_REF] Paraiso | Model-Driven Management of Docker Containers[END_REF]. It defines generic and specific container and machine resource types and associated links. 4) GCP is one of the leaders among cloud providers. It offers several service such as Compute, Storage, Network, Management, Big Data and Security. GCP was implemented as OCCI extension in [START_REF] Challita | A Precise Model for Google Cloud Platform[END_REF]. We present in the following the formal specification of the INSTANCE resource type, which represents a virtual machine in GCP. [START_REF] Merle | Mobile Cloud Robotics as a Service with OCCIware[END_REF] is an application of OCCI for Robot-as-a-Service domain.

The OMCRI extension defines generic and specific robot resource types. 9) COT is an application of OCCI for seamlessly provisioning cloud and IoT resources [START_REF] Rachkidi | Cloud of Things Modeling for Efficient and Coordinated Resources Provisioning[END_REF]. 10) OCCI SLA [START_REF] Katsaros | Open Cloud Computing Interface -Service Level Agreements[END_REF] defines OCCI types for modeling service level agreements. 11) OCCI MONITORING [START_REF] Ciuffoletti | Open Cloud Computing Interface -Monitoring Extension[END_REF] is a draft specification of OCCI that defines sensor and collector types for monitoring cloud systems. 12) CLOUD SIMULATION [START_REF] Ahmed-Nacer | OCCI-Compliant Cloud Configuration Simulation[END_REF] is an application of OCCI to simulate cloud systems. The CLOUD SIMULATION extension defines two notions: (i) a resource to simulate that represents the resource to be simulated, and (ii) a simulation resource that represents the resource which performs the simulation activity. 13) CLOUD ELASTICITY [START_REF] Zalila | OCCI Extension Models[END_REF] is an application of OCCI that defines a controller resource type to provide strategies for automatically provisioning and de-provisioning compute resources such as memory and cores.

B. Verification of FCLOUDS properties

Being rigorously encoded using the same formal language, i.e., FCLOUDS, our thirteen case studies can be now accessed by the same OCCI RESTful interface. Therefore, it is important to make sure that they correctly reflect the behaviour of FCLOUDS. Using Alloy analyzer, we verify that our thirteen formal specifications satisfy all the assertions, i.e., properties, that we formulated in our FCLOUDS language (cf. Table II). For instance, we verify that Create Compute operation of OCCI INFRASTRUCTURE is idempotent and that Update Instance operation of GCP is not safe.

C. Definition & validation of domain-specific properties

Our framework allows us to verify some domain-specific properties. For instance, in the following listing, we check whether creating a NETWORKINTERFACE between two OCCI resources only occurs between one COMPUTE resource type and one NETWORK resource type. This assertion is validated so our formal specification respects and implements the following requirement of OCCI INFRASTRUCTURE specification: "NetworkInterface connects a Compute instance to a Network instance" [START_REF] Nyrén | Open Cloud Computing Interface -Infrastructure[END_REF].

D. Formal transformation rules & equivalence properties

The last step for achieving semantic interoperability between heterogeneous domains is to define predicates that implement bidirectional formal transformation rules between resources with similar semantics. In the following example, we show how we can migrate from an OCCI INFRASTRUC-TURE virtual machine at to a GCP virtual machine. We map the attributes of a given COMPUTE resource to those of an INSTANCE resource. Also, since we learned from the OCCI INFRASTRUCTURE and GCP documentations that the memory in OCCI is expressed in gigabytes, whereas it is in megabytes in GCP, we applied the multiplication operator for the conversion. Such formal equivalence rules and properties are capable of gaining huge time and development costs. The cloud developer can now verify a priori the feasibility of his/her multi-cloud system, before embarking on error-prone implementations. Thanks to our transformation rules and to Model-Driven Engineering (MDE) principles, we can later imagine a model that factorizes common attributes for re-usability between OCCI INFRASTRUCTURE and GCP.

V. RELATED WORK

Only few works from the literature applied formal methods for the cloud, which proves the novelty of this domain. Di Cosmo et al. [START_REF] Di Cosmo | Towards a Formal Component Model for the Cloud[END_REF] adopted automata to define the Aeolus formal component model that captures cloud resources. Benzadri et al. [START_REF] Benzadri | Towards a Formal Model for Cloud Computing[END_REF] proposed a formal model for cloud computing using Bigraphical Reactive Systems (BRS). Amazon Web Services (AWS) [START_REF] Newcombe | How Amazon Web Services Uses Formal Methods[END_REF] used TLA+ specification language in their complex systems such as S3 and DynamoDB. Brogi et al. [START_REF] Brogi | A Petri Net-based Approach to Model and Analyze the Management of Cloud Applications[END_REF] used Petri nets to formally model the behaviour of TOSCA operations, requirements and capabilities. Bobba et al. [START_REF] Bobba | Design, Formal Modeling, and Validation of Cloud Storage Systems Using Maude[END_REF] specified and validated Google' Megastore, Apache Cassandra, Apache ZooKeeper, and RAMP using Maude language and model checker. Besides using different techniques to reason over the cloud, these five works differ in their objectives too. [START_REF] Di Cosmo | Towards a Formal Component Model for the Cloud[END_REF] studies the complexity of finding a deployment plan in the cloud. [START_REF] Benzadri | Towards a Formal Model for Cloud Computing[END_REF] also reasons over cloud concepts for deployment and adaptation purposes. [START_REF] Newcombe | How Amazon Web Services Uses Formal Methods[END_REF] aims at finding subtle bugs in their internal distributed algorithms, which helps optimizing their systems. [START_REF] Brogi | A Petri Net-based Approach to Model and Analyze the Management of Cloud Applications[END_REF] analyzes the validity of the deployment plan. [START_REF] Bobba | Design, Formal Modeling, and Validation of Cloud Storage Systems Using Maude[END_REF] verifies the performance and correctness of cloud storage systems. Our work focuses on the interoperability concern by formalizing the static and operational semantics of the cloud domain.

VI. CONCLUSION

To promote multi-cloud systems, we advocate exploring the semantics of each cloud API and reason about them in order to understand their similarities and differences, hence to achieve semantic interoperability. This work occurs in the context of the FCLOUDS framework, where we advocate the use of formal specification techniques, specifically the Alloy language, to rigorously and clearly describe the requirements of cloud APIs. We formalize the OCCI open standard in order to implement our formal language for the clouds. Our formal specification of OCCI was checked for validity thanks to the Alloy analyzer that provides a verification backbone for OCCI properties. To demonstrate the usefulness of our approach, we conducted thirteen case studies to show how our approach is applied on OCCI extensions and that these thirteen APIs with different functionality verify the OCCI properties so they correctly comply to the OCCI standard. Also, applying Alloy to these APIs allowed us to reflect the proper behavior of each API by identifying and validating its specific properties. Finally, having rigorously specified the static and operational semantics of each cloud API, we define formal transformation rules between their formal specifications, thus ensure semantic interoperability between them.

For future work, we will extend our catalog of formal cloud APIs in order to achieve our vision of building FCLOUDS, the first framework for semantic interoperability in multi-clouds. Using the FCLOUDS language, we will formally specify Amazon Web Services, OpenStack, etc. We will also enrich the FCLOUDS language, which is the backbone of all the FCLOUDS precise models, with additional properties such as Reachability, i.e., when executing operations on cloud resources through APIs, there is always a transition from a resource state to another. To do so, we might require to use widespread formal techniques other than Alloy and which are more suitable for expressing such property, like the TLA+ specification language and TLC, its model checker [START_REF] Lamport | Specifying Systems: the TLA+ Language and Tools for Hardware and Software Engineers[END_REF]. Furthermore, although model checkers verify that the properties are valid within a big scope of research, we need to prove it in the absolute through a convincing argument. Hence, we will use automated proof assistants [START_REF] Loveland | Automated Theorem Proving: a logical basis[END_REF], namely Coq [START_REF] Barras | The Coq Proof Assistant Reference Manual: Version 6[END_REF], which implements algorithms and heuristics to build a proof describing the sequence of needed moves in order to solve a property. Finally, we will allow the FCLOUDS framework to be executable inside the first formal-based real-world interoperability bridge.

  s i g R e s o u r c e e x t e n d s E n t i t y { l i n k s : s e t L i n k -> Time }

  s i g L i n k e x t e n d s E n t i t y { s o u r c e : R e s o u r c e one -> Time , t a r g e t : R e s o u r c e one -> Time }

1 p 2 / 6 /

 126 r e d C r e a t e R e s o u r c e [ c o n f i g : C o n f i g u r a t i o n , r e s o u r c e I d : S t r i n g , k i n d : Kind , m i x i n s : s e t Mixin , t , t ' : Time ] { / p r e c o n d i t i o n s a t i n s t a n t t 3 no r e s o u r c e : c o n f i g . r e s o u r c e s . t | r e s o u r c e . i d = r e s o u r c e I d 4 k i n d i n c o n f i g . u s e . k i n d s 5 m i x i n s i n c o n f i g . u s e . m i x i n s / p o s t c o n d i t i o n s a t i n s t a n t t ' 7 one r e s o u r c e : R e s o u r c e { 8 r e s o u r c e . i d = r e s o u r c e I d 9 r e s o u r c e . k i n d = k i n d 10 r e s o u r c e . m i x i n s . t ' = m i x i n s 11 c o n f i g . r e s o u r c e s . t ' = 12 c o n f i g . r e s o u r c e s . t + r e s o u r c e } }

  a s s e r t C r e a t e R e s o u r c e I s C o n s i s t e n t { one c o n f i g : C o n f i g u r a t i o n , s e t r e s o u r c e I d : S t r i n g , k i n d : Kind , m i x i n s : Mixin , t : Time | C r e a t e R e s o u r c e [ c o n f i g , r e s o u r c e I d , k i n d , m i x i n s , t , t . n e x t ] }

  a s s e r t C r e a t e R e s o u r c e T h e n R e t r i e v e R e s o u r c e { a l l c o n f i g : C o n f i g u r a t i o n , r e s o u r c e I d : S t r i n g , k i n d : Kind , m i x i n s : s e t Mixin , t : Time | C r e a t e R e s o u r c e [ c o n f i g , r e s o u r c e I d , k i n d , m i x i n s , t , t . n e x t ] and R e t r i e v e R e s o u r c e [ c o n f i g , r e s o u r c e I d , t . n e x t , t . n e x t . n e x t ] i m p l i e s r e s o u r c e . i d = r e s o u r c e I d and r e s o u r c e . k i n d = k i n d and r e s o u r c e . m i x i n s . ( t . n e x t . n e x t ) = m i x i n s }

  a s s e r t C r e a t e R e s o u r c e R e v e r s e D e l e t e R e s o u r c e { a l l c o n f i g : C o n f i g u r a t i o n , r e s o u r c e I d : S t r i n g , k i n d : Kind , m i x i n s : Mixin , t : Time { C r e a t e R e s o u r c e [ c o n f i g , r e s o u r c e I d , k i n d , m i x i n s , t , t . n e x t ] i m p l i e s D e l e t e R e s o u r c e [ c o n f i g , r e s o u r c e I d , t . n e x t , t ] } }

a s s e

  r t C r e a t e R e s o u r c e I s I d e m p o t e n t { a l l c o n f i g : C o n f i g u r a t i o n , r e s o u r c e I d : S t r i n g , k i n d : Kind , m i x i n s : Mixin , t : Time | C r e a t e R e s o u r c e [ c o n f i g , r e s o u r c e I d , k i n d , m i x i n s , t , t . n e x t ] and C r e a t e R e s o u r c e [ c o n f i g , r e s o u r c e I d , k i n d , m i x i n s , t . n e x t , t . n e x t . n e x t ] i m p l i e s c o n f i g . r e s o u r c e s . ( t . n e x t ) = c o n f i g . r e s o u r c e s . ( t . n e x t . n e x t ) }

a s s e

  r t R e t r i e v e R e s o u r c e I s S a f e { a l l c o n f i g : C o n f i g u r a t i o n , r e s o u r c e I d : S t r i n g , t : Time | R e t r i e v e R e s o u r c e [ c o n f i g , r e s o u r c e I d , t , t . n e x t ] i m p l i e s c o n f i g . r e s o u r c e s . t = 3 A collection is a set of resources with the same kind. c o n f i g . r e s o u r c e s . ( t . n e x t ) and one r e s o u r c e : c o n f i g . r e s o u r c e s . ( t . n e x t ) { r e s o u r c e . i d = r e s o u r c e I d } }

s i g

  Compute e x t e n d s f c l o u d s / R e s o u r c e { o c c i c o m p u t e a r c h i t e c t u r e : l o n e A r c h i t e c t u r e , o c c i c o m p u t e c o r e s : l o n e Core , o c c i c o m p u t e h o s t n a m e : l o n e S t r i n g , o c c i c o m p u t e s h a r e : l o n e S h a r e , o c c i c o m p u t e s p e d : l o n e GHz , occi compute memory : l o n e GiB , o c c i c o m p u t e s t a t e : one C o m p u t e S t a t u s , o c c i c o m p u t e s t a t e m e s s a g e : l o n e S t r i n g }

  a s s e r t N e t w o r k I n t e r f a c e B e t w e e n C o m p u t e A n d N e t w o r k { a l l c o n f i g : C o n f i g u r a t i o n , l i n k I d : URI , l i n k K i n d : n e t w o r k i n t e r f a c e , l i n k S o u r c e : f c l o u d s / R e s o u r c e , l i n k T a r g e t : f c l o u d s / R e s o u r c e , t : Time | C r e a t e i n k [ c o n f i g , l i n k I d , l i n k K i n d , l i n k S o u r c e , l i n k T a r g e t , t , t . n e x t ] i m p l i e s one c o n f i g : C o n f i g u r a t i o n { one r e s o u r c e C o m p u t e : c o n f i g . r e s o u r c e s . t { r e s o u r c e C o m p u t e . h a s K i n d [ compute ] one l i n k : f c l o u d s / L i n k { l i n k . i d = l i n k I d l i n k i n r e s o u r c e C o m p u t e . l i n k s . ( t . n e x t ) } } one r e s o u r c e N e t w o r k : c o n f i g . r e s o u r c e s . t { r e s o u r c e N e t w o r k . h a s K i n d [ n e t w o r k ] one l i n k : f c l o u d s / L i n k { l i n k . i d = l i n k I d l i n k i n r e s o u r c e N e t w o r k . l i n k s . ( t . n e x t ) } } } }

  p r e d C o m p u t e M a p I n s t a n c e [ c : one Compute , i : one I n s t a n c e ] { i . m a c h i n e t y p e . g u e s t C p u s = c . o c c i c o m p u t e c o r e s i . name = c . o c c i c o m p u t e h o s t n a m e i . m a c h i n e t y p e . i s S h a r e d C p u = c . o c c i c o m p u t e s h a r e i . m a c h i n e t y p e . memoryMb = mul [ 1 0 2 4 , c . occi compute memory ] i . s t a t u s = c . o c c i c o m p u t e s t a t e i . s t a t u s M e s s a g e = c . o c c i c o m p u t e s t a t e m e s s a g e }

  A signature (sig) in Alloy defines a set of atoms. An atom is an indivisible, immutable and uninterpreted unity. Signature declarations can introduce fields. A field represents a relation among signatures. For example, ENTITY declares three fields: id, kind and mixins. Each entity has a unique identifier (id). A declaration of the form id : one String can be read as declaring a feature of the set Entity; formally, it declares a binary relation between the set of entities, Entity, and the set of Strings, String. The one keyword signifies that the relation between a tuple from id and a tuple from String has a 1..1 cardinality. Kind is the Entity type, for example the kind of a resource can

	a b s t r a c t s i g E n t i t y {
	i d : one S t r i n g ,
	k i n d : one Kind ,
	m i x i n s : s e t Mixin -> Time }

be compute, application, etc. The mixins field is used to add additional features such as location and price. The id and kind are immutable. As for the mixins field, it is mutable and it identifies the association between MIXIN atoms and their Time. The arrow product Mixin → Time is the relation we get by taking every combination of a tuple from MIXIN and a tuple from Time and concatenating them. Due to space restrictions in this paper, please refer to

[START_REF] Ahmed-Nacer | OCCI Behavioural Model[END_REF]

for the specification of KIND and MIXIN concepts.

• RESOURCE represents any cloud computing resource, which refers to any entity hosted in a cloud, e.g., Compute, Network, Storage, etc. RESOURCE owns a set of mutable links.

TABLE I :

 I FCLOUDS Static Semantics.

	FCLOUDS Concepts	Description
		a concrete cloud computing domain,
	EXTENSION	such as Infrastructure as a Service (IaaS), Platform as a Service (PaaS), Software as a Service (SaaS), cloud robotics,
		etc.
	CONFIGURATION	a running OCCI system
	ENTITY	an abstract type defining the set of all resources and links
	RESOURCE	represents any cloud computing resource, such as a virtual machine
	LINK	a relation between two resources
	ATTRIBUTE	a resource property, such as the hostname of a virtual machine
	DATATYPE	an abstract type defining enumerations, lists, records, etc.
	CATEGORY	the abstract base class inherited by KIND, MIXIN and ACTION
	KIND	immutable type of OCCI entities
	MIXIN	represents crosscutting attributes and actions that can be dynamically added to an OCCI entity
	ACTION	domain specific behavior, such as start/stop a virtual machine
	s i g C o n f i g u r a t i o n {
		u s e : s e t E x t e n s i o n ,

r e s o u r c e s : s e t R e s o u r c e -> Time }

TABLE II :

 II Properties of the FCLOUDS Language.

	Properties	Consistency	Idempotence	Safety
	Static Semantics	+	N/A		N/A
	Operational Semantics
	(OCCI REST Operations)
	Create Resource	+	+		-
	Retrieve Resource	+	+		+
	Update Resource	+	-		-
	Delete Resource	+	+		-
	Create Link	+	+		-
	Retrieve Link	+	+		+
	Update Link	+	-		-
	Delete Link	+	+		-
	Properties	Sequentiality	Reversibility
	Pairs of OCCI REST Operations
	Create Resource & Retrieve Resource	+		-
	Retrieve Resource & Create Resource	-		-
	Retrieve Resource & Update Resource	+		-
	Update Resource & Retrieve Resource	-		-
	Update Resource & Delete Resource	-		-
	Delete Resource & Update Resource	-		-
	Delete Resource & Create Resource	-		+
	Create Resource & Delete Resource	+		+
	Create Link & Retrieve Link	+		-
	Retrieve Link & Create Link	-		-
	Retrieve Link & Update Link	+		-
	Update Link & Retrieve Link	-		-
	Update Link & Delete Link	-		-
	Delete Link & Update Link	-		-
	Delete Link & Create Link	-		+
	Create Link & Delete Link	+		+

TABLE III :

 III Summary of the FCLOUDS Framework Dataset. It inherits the RESOURCE kind defined in the OCCI core model. COMPUTE has a set of OCCI attributes that we declare as fields to our COMPUTE signature, such as occi.compute.architecture to specify the CPU architecture of the instance, occi.compute.core to define the number of virtual CPU cores assigned to the instance, occi.compute.memory to define the maximum RAM in gigabytes allocated to the instance, etc. The lone keyword signifies that the relation between two tuples from two sets, such as occi.compute.architecture and Architecture, has a 0..1 cardinality.

	Extension	#Kind	#Mixin	#Attribute	#Action	#DataType
	IaaS
	OCCI INFRASTRUCTURE	5	6	31	9	20
	OCCI CRTP	0	6	18	0	0
	DOCKER	24	0	251	7	2
	GCP	150	0	2348	985	398
	VMWARE	6	7	19	0	1
	PaaS
	OCCI PLATFORM	3	4	11	4	3
	MODMACAO	1	31	9	0	2
	IoT
	OMCRI	5	9	20	15	2
	COT	6	4	21	0	3
	Transverse
	cloud concerns
	OCCI SLA	2	2	8	5	4
	OCCI MONITORING	2	3	9	0	2
	CLOUD SIMULATION	8	14	53	0	0
	CLOUD ELASTICITY	2	4	23	4	5
	Total	214	90	2821	1029	442
	VLAN range. The COMPUTE kind represents a generic
	information processing resource, e.g., a virtual machine or
	container.

ACKNOWLEDGMENT

This work is supported by the OCCIware research and development project funded by French Programme d'Investissements d'Avenir (PIA) and the Hauts-de-France Regional Council.

AVAILABILITY

Readers can find the FCLOUDS formal language and all the thirteen formal specifications at https://github.com/occiware/ fclouds-Framework.


L Zhang

L Botti

S Petit

Destination performance: Introducing the utility function in the Mean-Variance space

Keywords: Productivity Measurement, Mean-Variance, Tourism Efficiency, Efficiency Decomposition, Utility Function, Nord Pas-de-Calais L83, C61, C67

Economic characteristics of home countries can cause considerable variations in the tourism demand. For example, the average level of expenditure per tourist varies from one origin to another and these variations may alter overtime. Thus different tourist nationalities are associated with different level of expenditures and risks. Therefore strategies aimed at minimizing the variations may become an important issue for the policy makers. In this paper, we aim to use the productivity measurement theory in a mean-variance space to a French region (Nord Pas-de-Calais) by introducing the utility function in a mean-variance framework. With this method, we can calculate the optimal portfolio share for each origin and give some useful political advices to the policy decision makers to improve the performance of the tourist sector.

Introduction

Tourism is an important Industry in the French region of Nord Pas-de-Calais (NPDC). Given its favourable location in the heart of North-East Europe, in the middle of London-Paris-Brussels triangle, NPDC receives over 175 million trips per year. In order to take full advantage of this industry to strengthen the local economy, actions are being implemented to further develop regional tourism. The Eurostar and Thalys high-speed train make Lille, the capital of NPDC ever closer to London and Brussels.

Development of Lille Airport connect the region to other major markets such as Barcelona, which is now only two hours away by flight even more accessible. . In terms of employment, tourism generated an average of nearly 39,000 salaried jobs in 2009 for the NPDC, representing an increase of 16 % compared to 2003. This job places creation allows NPDC to rank only ninth at regional level. However, compared to the national average which is 4.8%, the tourism employment represents only 2.7% of salaried jobs in this region 1 . In terms of tax revenue, tourism is a springboard for the economy of the region. Indeed, tourism and leisure represent 3.30% of regional GDP in 2009, equivalent to the compulsory residence permit paid by the locals and amounting to 3.5 million euros. Nevertheless, the economic contribution from the tourism sector in this region is lower than the average French level as tourism represents more than 6.5% of the national GDP.

There is room for improving the efficiency of the tourism industry of in order to increase the economic contribution of the sector of tourism in this region of France. The region Nord Pas-de-Calais represents only 0.2% of the total national investment in tourism. The local authorities have understood the economic potential from tourism. Since the beginning of 4 the 2000s, the local authorities had invested in the organization of different business events. More than 55% of tourists are professional customers. The advantage of this strategy is to develop new opportunities of market. If the British is the first foreign market, the local authorities expect to attract another nationalities with the centenary of the 1 st World War (Canadian, American and Australian soldiers were present in this region just as well as Chinese workers) and the 70 th birthday of the end of the 2 nd World War.

The geographic localization of the NPDC region can also provide another advantage if it is well exploited.

Authors such as [START_REF] Barros | A Stochastic Cost Frontier in the Portuguese Hotel Industry[END_REF], [START_REF] Barros | Performance of French destinations: Tourism attraction perspectives[END_REF] and [START_REF] Assaf | Benchmarking the Asia Pacific tourism industry: a Bayesian combination of DEA and stochastic frontier[END_REF] have developed efficiency measurement of tourism industry. But very few works have been done on the efficiency measurement following origins of tourists. A viable and resilient tourism destination should try to maximize the number of tourists come from different origins, and minimize the instabilities in revenues by diversifying its market mix [START_REF] Kennedy | Risk Management in the Irish Tourism Industry: The contribution of a Portfolio Investment Approach[END_REF].

The efficiency following the tourist's origins is one of the essential questions to understand the composition and characteristics of the local tourism industry. In order to answer this question, the performance evaluation (in terms of possible revenue augmentation and/or possible risk contraction) of inbound tourist is valuable and necessary. The result of this kind of analysis can guide the policy makers by giving them the accurate efficiency indicators for future decision-making process.

The aim of the current paper is to introduce a nonparametric efficiency measurement framework into a mean-variance space, in order to evaluate the performance of tourism sector and identify the possible source of the existing inefficiency. The contribution of this paper is two-fold. First it improves the existing measures of efficiency by introducing the decision maker's utility function; second, the result obtained is used to develop strategies for reducing volatility in tourism receipt. Accordingly, this paper proposes a framework for the evaluation of destination performance which can assist Destination Management Organizations (DMO) in enhancing the performance of the industry.

The paper is organized as follows: section 2 critically reviews the existing literature on the measurement the tourism efficiency; section 3 presents our theoretical framework; in section 4, data from NPDC is analyzed using mean-variance method. The paper ends by a discussion of the results and develops a framework for policy makers. .

Efficiency measurement in tourism

The performance of a firm, particularly as measured by productivity and efficiency, has been a common subject in tourism studies. The hotel sector has attracted the most attentions, followed by travel agents and restaurants.

The empirical literature on the effectiveness of the tourism business has been dominated by the non-parametric approach: Data Envelopment Analysis (DEA; [START_REF] Seiford | Data Envelopment Analysis: The Evolution of the State of the Art (1978-1995)[END_REF].

The first effort of applying DEA to tourism begins in the year 80s. Hruschka (1986a) measured then different Australian restaurant groups and found that there exists difference efficiency among these groups. Banker and Morey (1986b) who introduced quasi-fixed variables in DEA, evaluated the technical and scale efficiency of 60 fast food restaurants with discretional variables. [START_REF] Morey | Evaluating a hotel GM's performance: a case study in benchmarking[END_REF] evaluated the performance of 54 hotels of a national chain in the U.S, and found these hotels were quite efficient, with an efficient score of 0.89. More recent applications include [START_REF] Anderson | Hotel industry efficiency: an advanced linear programming examination[END_REF], [START_REF] Hwang | Using Data Envelopment Analysis to Measure Hotel Managerial Efficiency Change in Taïwan[END_REF], [START_REF] Barros | Productivity in the tourism industry[END_REF], [START_REF] Daniels | Beyond Input-Output Analysis: Using Occupation-Based Modeling to Estimate Wages Generated by a Sport Tourism Event[END_REF], [START_REF] Chiang | A DEA evaluation of Taipei hotels[END_REF], Barros (2005), [START_REF] Barros | The measurement of efficiency in Portuguese hotels using Data Envelopment Analysis[END_REF], [START_REF] Köksal | Efficiency evaluation of Agroup travel agencies with data envelopment analysis (DEA): A case study in the Antalya region, Turkey[END_REF], Botti et al. (2009), [START_REF] Perrigot | Plural form Chain and Efficiency: Insights from the French Hotel Chains and the DEA Methodology[END_REF], [START_REF] Assaf | The future outlook for Portuguese travel agents[END_REF], [START_REF] Assaf | Benchmarking the Asia Pacific tourism industry: a Bayesian combination of DEA and stochastic frontier[END_REF] and many others. However, there are only very few works which have studied the tourism sector at a territory level: [START_REF] Bosetti | Benchmarking in tourism destination, keeping in mind the sustainable paradigm[END_REF]), Peypoch (2007), [START_REF] Barros | Performance of French destinations: Tourism attraction perspectives[END_REF] and these papers have used basic DEA model (CCR for [START_REF] Charnes | Measuring the efficiency of decision making units[END_REF] model and/or BCC for [START_REF] Banker | Some Models for Estimating Technical and Scale Inefficiencies in Data Envelopment Analysis[END_REF] model) as theoretical framework. And only two papers (Botti et al., 2009;[START_REF] Ratsimbanierana | Moroccan tourist portfolio efficiency with the mean-variance approach[END_REF]) make an efficiency assessment of regions with a directional distance function (DDF -Chambers et al., 1998).

In his paper, theoretical framework applies a nonparametric efficiency measurement, and uses DDF in a mean-variance space to calculate an overall efficiency (OE) indicator, which can be decomposed into a technical efficiency (TE) indicator and an allocative efficiency (AE)

indicator. The advantage of this technique is that with consideration of utility function in a Mean-Variance space, we can find out more precisely the source of the inefficiency, thus propose a more appropriate suggestion to the policy decision maker.

To the author's knowledge, there are only two articles [START_REF] Botti | French Destination Efficiency: A Mean-Variance Approach[END_REF][START_REF] Ratsimbanierana | Moroccan tourist portfolio efficiency with the mean-variance approach[END_REF], which used DDF in a mean-variance framework to measure the destination efficiency according to tourist origins. However, these papers have just measured the technical efficiency and did not attempt to find other kind of inefficiencies in the tourism sector.

The next sections of this present article fill this gap in the literature.

Theoretical Framework

Scarcity of resource and ever growing needs for justifying investment has lead to more and more emphasis being laid on the analysis of the relationship between resources allocation and their economic return. For a given country or region, ways to minimize the instability and maximizing the return of their inbound tourism with consideration of utility function are very important issues for the policy decision makers [START_REF] Kennedy | Risk Management in the Irish Tourism Industry: The contribution of a Portfolio Investment Approach[END_REF][START_REF] Botti | French Destination Efficiency: A Mean-Variance Approach[END_REF]. This idea is very related to the conception of modern investment theory. Therefore, the mean-variance space seems a suitable framework in our case.

Efficient frontier and portfolio management

Consider n funds with a return vector 12 ( , ,..., )

' n R R R R 
, each fund is then characterized by an expected return () i ER and a variance () i VR , where 1,2,..., in 

. Then the expected return vector and the variance vector can be written separately by

  12 ( ) ( ), ( ),..., ( ) ' n E R E R E R E R  and   12 ( ) ( ), ( ),..., ( ) ' n V R V R V R V R 
. Then the covariance matrix of these funds can be written by ( , )

ij i j COVA R R 
, where 1,2,..., in  and 1,2,..., jn  .

Then we can define a portfolio X , which is composed by these n funds, with the vector 12 ( , ,... )

n x x x x  , 1 i i x   indicate the weight of each fund.
The return of portfolio X is R( X) = xR . The expected return and its variance can be calculated as follows:

  ( ) ( ) E R X xE R  (1)   ( ) ' ij V R X x x  (2)
If all the constraints faced by the investors for each funds can be written by a linear function of the fund's weight, then the set of possible portfolio is defined as:

, 1, ' , 0

n i i x R x Ax b x           (3)
Then the Markowitz mean-variance space is defined as:

    ( ), ( ) ; V X E X x    (4)
But from a mathematical point of view, this representation cannot be used directly for quadratic programming (see [START_REF] Briec | Single Period Markowitz Portfolio Selection, Performance Gauging and Duality: A Variation on the Luenberger Shortage Function[END_REF]. The above set is then extended by defining a portfolio representation set as:

    ( ', ') ; ,( ', ') ( ), ( ) V E R R x V E V X E X          (5)
Then the efficiency frontier is defined as:

                ( ) , ( ) ; ( ) , ( ) ( ', ') ( ', ') V R X E R X x V R X E R X V E V E            (6)
This frontier represents the set of all the mean-variance points that are not strictly dominated in the two-dimensional space.

Markowitz efficiency frontier

Markowitz defines an optimization program to determine the portfolio corresponding to a given degree of risk aversion. This portfolio maximizes a mean-variance utility function defined by:

        ( , ) U E R x V R x    (7)
    * ( , ) 1,..., sup ( ) ( ) . . ' b 1 0 i in U E R x V R x s t Ax x x         (8)
So given the investors' risk aversion, this program allows one to choose an "optimal" portfolio in the efficiency frontier, which can maximize their utility function. Following [START_REF] Uysal | Revisiting Mean-Variance Optimization[END_REF], the conventional values for risk aversion

f = r m
often range between 0.5 and 10.

In this article, 2   (with r = 2 and m = 1 ) is used 3 according to [START_REF] Morey | Mutual Fund Performance Appraisals: A Multi-Horizon Perspective with Endogenous Benchmarking[END_REF] and [START_REF] Briec | Single Period Markowitz Portfolio Selection, Performance Gauging and Duality: A Variation on the Luenberger Shortage Function[END_REF].

Efficiency measurement

The efficiency measurement of a set of decision units (or a portfolio for the Markowitz model) consists in roughly enveloping the data and then measuring the distance between the realized performance of each unit (each portfolio in the Markowitz model) and this estimated frontier. This gap between the unit and the frontier is defined as inefficiency. In fact, the technology is represented by the frontier between feasible and infeasible productions. The frontier itself is important as it contains all the relevant information about marginal productivity, elasticity of substitution and returns to scale; it is not directly observable and must then be estimated.

The characterization of the frontier rests on an axiom that provides some indication on expectations from the frontier. This paper proposes to use a directional distance function to measure the inefficiency. The directional distance function measures the distance between the observation and the efficient frontier along a chosen directional vector pre-chosen. This idea was introduced by Luenberger (1992) and has been used in several sectors: [START_REF] Briec | Single Period Markowitz Portfolio Selection, Performance Gauging and Duality: A Variation on the Luenberger Shortage Function[END_REF] and [START_REF] Briec | Mean-Variance-Skewness Portfolio Performance Gauging: A General Shortage Function and Dual Approach[END_REF] suggest an application in the financial sector, as did [START_REF] Peypoch | A Note on Technical Efficiency in Tourism Industry[END_REF] andPeypoch (2007). [START_REF] Botti | French Destination Efficiency: A Mean-Variance Approach[END_REF][START_REF] Ratsimbanierana | Moroccan tourist portfolio efficiency with the mean-variance approach[END_REF] have already applied DDF in a Mean-Variance framework. However, as we explain at the end of this section, they just measured the technical efficiency in their papers and did not try to find other kind of inefficiency for the tourism sector.

3 A robustness check of our results by testing different values of risk aversion will be presented in the empirical section Following the demonstration of [START_REF] Briec | Single Period Markowitz Portfolio Selection, Performance Gauging and Duality: A Variation on the Luenberger Shortage Function[END_REF], the directional distance efficiency measurement function is defined as:

        ( ) sup ; ( ) , ( ) g V E S x V R x g E R x g        (9)
The DDF seeks the greatest possible risk (variance) contraction in the negative direction vector In fact, in their paper, they just used a Shephard's distance function, which is commonly used in the classic DEA models. Among other differences between these two functions (see [START_REF] Färe | Theory and Application of Directional Distance Functions[END_REF] for detail), one difference is DDF has an additive structure while the other ones are additive by nature.

For the policy makers, not only evaluating the performance of their sector is necessary, but also knowing the sources of its inefficiency is equally or even more important. Here the distinction between allocative, and technical efficiency is proposed when evaluating the scope for improvements of tourism strategies. OE indicator measures the distance between the maximum utility that the portfolio can reach and the current utility for one portfolio normalized by the directional vector. This idea is in fact very similar to the Nerlovian profit indicator. The formulation proposed by Chambers et al. (1998b) is followed to calculate this indicator, which allows us to a dual relationship between the Markowitz utility function and the DDF.

For a chosen risk aversion parameters ( , ), the maximum utility function is defined as

U * (r,m) ³ mE R(x) ( ) -rV R(x) ( ) for x .
This implies that the efficient utility is no less than the value of the feasible meanvariance vector. Thus, for the portfolio k , we have the relation: From the portfolio's specific utility function established earlier it can be observed, after the necessary re-arrangement, that a portfolio's utility efficiency or so we called OE in general can be expressed as:

                          * , k EV EV U E R x g V R x g E R x V R x g g                   (
* ( , ) (x) gg EV UU       (12)
The above inequality is explained by the possible presence of inefficient allocation of resources even when all technical inefficiencies are eliminated, like point B in the figure 1. While it is technically efficient for being on the efficient frontier; it is not overall efficient. The presence of inefficient resource allocation in portfolio B is a possible source of its profit inefficiency. The inequality is thus closed when the allocative inefficiency component is added, resulting in equality of the above expression. This means that the allocative inefficiency is residually determined from the Nerlovian profit and technical inefficiencies. It should be observed that the elimination of technical and allocative inefficiencies is expected, all else remaining constant, to achieve full efficiency. The equality between the utility, technical, and allocative efficiencies is given by the following expression:

* ( , ) (x) (x) gg EV UU AE       (13)
Then the Overall efficiency (OE) is calculated as:

OE(x,r,m) = U * (m,r) -U (x) ( ) m g E + r g V ( ) (14)
Portfolio efficiency indicator (PE) it is called technical efficiency (TE), as in [START_REF] Briec | Mean-Variance-Skewness Portfolio Performance Gauging: A General Shortage Function and Dual Approach[END_REF] and is calculated by:

( ) ' 1 0 PE o PE o o E PE o o V ij i in s t E R g xE R V R g x x x x            )
The overall efficiency OE o  is calculated in a 3 steps procedure:

1-Equation ( 8) is used to obtain * ( , )

U  , 2-Equation ( 14) to obtain OE o  , and finally 3-The allocative efficiency AE o  is calculated as follow:

AE OE PE o o o     (18)
For n origins, we have to repeat n times this process.

It is clear that the risk related parameters (  ,  ) will influence the slope of the utility function. Therefore, OE o  is variant with  and  . However, since the calculation of OE is not directly related to risk aversion, PE o  should remain invariant to these parameters. As we mentioned above, a robust test of our results by testing different values of risk aversion will be presented at the end of the empirical section of this paper.

An application to Nord Pas-de-Calais (France)

Instead of using the price of funds as in the traditional financial investment theory, we have to choose a variable, which can represent the value of inbound tourists for the concerned local economy. In the tourism industry, it's not the number of visitors' arrival, which is the most important element for an economy. The expenditure of tourists is a more proper variable to evaluate the contribution of tourism to an economy.

However, in our case, only the overnight stays data are available. This variable is commonly used in the literature (see for example Peypoch, 2007 and[START_REF] Botti | French Destination Efficiency: A Mean-Variance Approach[END_REF]. Furthermore, it is clear that a tourist who choses to stay in a "one star" hotel will normally spend less than a tourist who chose to stay in "five star" hotel. In this paper, we have used a Matlab program written by ourselves to run the estimation and produce the graphics. The results are presented in the following Tables (Table 3 to Table 6). As aforementioned, there are three models:

1. Model 1 maximizes the expected return for a fixed variance;

2. Model 2 minimizes the risk for a given expected return;

3. Model 3 maximizes the expected return and minimizes the risk for a pre-

chosen direction (with   , g V E 
) and therefore identifies the inefficiency level.

Table 3 demonstrates the results of the mean-augmentation approach (Model 1). Column 2 and 3 shows origins expected overnight stays and standard deviation for the year 2013. Column 4 shows the maximum attainable overnight stays for each origin, Column 5 shows the technical efficiency and the last column gives the rank of each origin according to its performance. For example, for next year, for the given risk level and optimal portfolio weights, NPDC can expect a maximum 43,853 overnight stays from Belgium, being an increase of 24.52% compared to the past.

Meantime, this increase can be as high as 63.19% for USA,which means that USA as a tourist origin places further from the efficient frontier than Belgium. Therefore, USA performs worse than Belgium in the tourist portfolio of NPDC. Table 4 displays the risk-contraction approach (Model 2). As for Belgium, for the same level of overnight stays, NPDC can reduce the risk, so the average volatility of tourism expenditures, from this origin by 22.9%.

However, if NPDC seeks to rise the overnight stays and at the same time reduce the risk, then the results of DDF approach presented in Table 5 should be considered (Model 3). Taking Belgium for example, for the year 2013, NPDC can expect 35,217 overnight stays from Belgium with a standard deviation of 14,665. But according to the results of our model, NPDC should be able to attract 38,522 overnight stays with a risk level of 13,960; it means NPDC could at the same time improve the return and reduce the instability of Belgium tourists by 9.4%.

For these three models, the UK is the most efficient origin and therefore severs as the benchmark for all the other origins. This can be explained by its geographic localization since the EUROSTAR train line and The Channel Tunnel link the UK and NPDC. The historical and cultural links shared between UK and NPDC is also explanation of this fact. The same explanation can be applied to Belgium. As the middle point between Paris and Brussels, it is not surprising that tourist from Belgium performs very well for NPDC. As for Spain and Italy, their good performance can be explained by the fact that firstly, there is lots of Spanish and Italian former immigrants in the region since the 19 th and 20 th centuries, lots of family reunion occurs in NPDC; secondly, as a European country, tourists from these two countries know well the tourist monuments and culture attraction in NPDC. As for the tourists from USA, China and Japan, NPDC is just a stop over to visit Paris, Brussels, Amsterdam or Luxembourg. And since the tourists from these countries traditionally do not know the region very well, so the poor performance of these markets is not surprising. This result is very interesting, since in the paper [START_REF] Botti | French Destination Efficiency: A Mean-Variance Approach[END_REF], the authors found USA is quite efficient to France, here the explanation is once more the American tourists who enjoy Paris and other more popular French destinations, may not be familiar with the tourism products of the NPDC.

The region NPDC played a prominent role during the First World War.

At any given moment, every community in the Pas-de-Calais had, to a greater or lesser extent, an involvement in the war and considered as a microcosm of the world at war. Therefore, local public authorities of NPDC are hoping to better market the region by developing "Memorial Tourism" to commemorate the beginning of the 100 th anniversary of the First World War to show case its products to Northern American and Chinese tourists.

As we can see in Table 6, the average performance of the origins is poor.

According to the average overall inefficiency score, NPDC can improve 86.53% of its utility obtained in the tourist sector for the given utility function. And the decomposition results show that among these potential utility improvements, 30.97% comes from technical inefficiency and 55.55% comes from allocative inefficiency. There is no origin perfectly satisfy NPDC's preference (The most efficient is the African countries, with an OE equals to 39.17%). This result means besides the possible return augmentation and risk contraction, the wrong choice of values of risk aversion is the main source of inefficiency for the region. In order to improve the allocative efficiency, NPDC should guide their tourist policy to change the combination of return and risk for these origins according to region's own preference (utility function). Once all the origins achieve the efficient frontier, NPDC need to move these origins along the frontier to reach the tangent point (maximum utility for NPDC). Optimal portfolio share (PS) for each origin, which allows NPDC to achieve its maximum utility ( * 240903

U  
) is also reported in Table 6.

Results of DDF approach and efficiency decomposition are also illustrated in Figure 2, 3 and 4 in the appendix. Figure 2 and Figure 3 present each origin in the mean-variance space and their projection on the efficient frontier. Figure 3 is obtained by omitting England, which is behaving as an outlier from the sample to present a clear representation of the framework. To illustrate the decomposition analysis, the Figure 4 proposes an utility function characterized by a risk aversion equal to 0.01, few origins and the optimal portfolio (in terms of OE). Shares of origins for this portfolio are reported in . The detail result will be showed in table 7. This kind of methodology can be very useful for territories which have a need to develop their international tourism market and which are characterized by a strong proportion of internal tourism (as NPDC). It is well known in tourism that the international market can provide a better economic contribution than the local market but all the marketing strategies, according to the nationality aimed, are not always efficient.

The other advantage of this methodology is to provide some crucial information about the power of attraction for a given destination according to the tourist's country of origin. A gravitational model, by using bilateral data, gives some important descriptions about this power of attraction. But, the method developed in this present paper provides a new source of information: the potential of output that can be expected and the risk associated. An interesting further research can be to combine these two methodologies (gravitational model and mean-variance analysis) and comparing the different results in order to understand how the international tourism marketing strategy developed by the local authorities can be improved. And another research line reports to the vector x introduced in the theoretical framework of this paper. It should be interesting for policy decision makers to know the composition of this vector i.e. the weight of each funds (here origins) in the optimal portfolio of origins.

  separately the marginal utility for the investors for the expected return and risk. The ratio f = r m traditionally represents investors' risk aversion. The quadratic program is written as:

Vg.

  in order to obtain the maximum attainable expansion of expected return in the positive direction E g . In summary, this function measures the potential improvement in term of the possible increase in expected return and reduction in variance for a The advantage of this method compared to the classical DEA model is the possibility to control the projection direction of the inefficient points to the efficient frontier.[START_REF] Morey | Mutual Fund Performance Appraisals: A Multi-Horizon Perspective with Endogenous Benchmarking[END_REF] already introduced the DEA model in portfolio efficiency measurement. But their model had two specific perspectives: maximize the expected return for a fixed variance, or minimize the risk for a given expected return. As we can see, their model is just a specific case of the DDF approach (

  10) This function establishes the relationship between portfolio k's utility function   * , kU  and the DDF. This relation can also be interpreted as the one portfolio's maximal utility is greater than or at least equal to the actual or observed utility, plus the gain in utility resulting from reductions in technical inefficiency. And we have:

  Fig. 1. Markowitz utility function, DDF and inefficiency decomposition

  were computed Since according to the literature the conventional value should range between 0.5 and 10, Figure5shows the decomposition of the average

Fig. 5 .

 5 Fig. 5. Evaluation of overall efficiency decomposition for a range of risk aversion

Table 1

 1 Statistical description of NPDC tourists monthly overnight stays between 2006 and 2012

	The database for NPDC, includes data on
	average hotel price of different categories (null and 1 star, 2 star, 3 and 4
	star) for 2013, and the number of overnight stays for tourists from different
	origins in different category hotels. Therefore, monthly data of the
	overnight stays from 16 different countries is weighted by their hotel rates
	to take into account different expenditure level. This variable will be used
	as a proxy of the value of inbound tourist for NPDC. Risk and return are
	calculated over a 7 years horizon between 2006-2012. The statistical
	description of our data is presented in table 1. Table 2 presents the average
	prices used.

Table 2

 2 Average price for hotels category in NPDC

		Average price (euro) for peak	Average price (euro) for normal season
		season (May, June, July, August)
	Null and 1 star	48,4444	43,4091
	2 star	78,0056	63,7955
	3 and 4 star	124,6173	96,0125

Table 8 .

 8 In Figure4, two efficient points (which represent China and African countries) are very close to the utility function which corresponds to decomposition results in Table8; the AE for these two origins is not far away from null (0.0063 for China, and 0.0191 for African countries).One potential issue is the sensitivity of our decomposition result since importance of OE and AE is related to the risk aversion  . In order to test the robustness of our result, computed the OE, AE for a large range of 

Table 3

 3 Results of mean Augmentation Approach

	Origins

Table 5

 5 Results of mean augmentation and risk contraction approach

	Origins

Table 7

 7 Robust test for the sensibility of OE decomposition

	rho/mu	OE	PE(TE)	AE
	0,01	0,755396	0,309748	0,445649
	0,05	0,839618	0,309748	0,529870
	0,1	0,852454	0,309748	0,542707
	0,2	0,859117	0,309748	0,549369
	0,3	0,861376	0,309748	0,551628
	0,4	0,862513	0,309748	0,552765
	0,5	0,863198	0,309748	0,553450
	0,6	0,863655	0,309748	0,553907
	0,7	0,863982	0,309748	0,554234
	0,8	0,864228	0,309748	0,554480
	0,9	0,864419	0,309748	0,554671
	1	0,864572	0,309748	0,554824
	2	0,865262	0,309748	0,555514
	3	0,865492	0,309748	0,555744
	4	0,865607	0,309748	0,555859
	5	0,865676	0,309748	0,555929
	6	0,865722	0,309748	0,555975
	7	0,865755	0,309748	0,556008
	8	0,865780	0,309748	0,556032
	9	0,865799	0,309748	0,556052

Table 8

 8 Decomposition of efficiency score for DDF approach, with risk aversion 0.01

	 

Even we can use two stage DEA model to identify the influence of tourist nationalities on tourism efficiency, the truncate regression in second stage still suffers lots of defauts ( forme specification, statitifcal reference can only obtained by boot-strap method, the frontier forme did not take into account the influence of environmental variables, etc). The parametric method however can not trait well multioutput problem and the results depends largely the function form pre-supposed.

0,865815 0,309748 0,556067