Rim Abid
email: rim.abid@inria.fr

Gwen Salaün
email: gwen.salaun@inria.fr

Noel De Palma
email: noel.depalma@imag.fr

Formal Design of Dynamic Reconfiguration Protocol for Cloud Applications

Keywords: Cloud Computing, Dynamic Reconfiguration, Distributed Applications, Fault-Tolerance, Verification

Cloud applications are complex applications composed of a set of interconnected software components running on different virtual machines, hosted on remote physical servers. Deploying and reconfiguring this kind of applications are very complicated tasks especially when one or multiple virtual machines fail when achieving these tasks. Hence, there is a need for protocols that can dynamically reconfigure and manage running distributed applications. In this article, we present a novel protocol, which aims at reconfiguring cloud applications. This protocol is able to ensure communication between virtual machines and resolve dependencies by exchanging messages, (dis)connecting, and starting/stopping components in a specific order. The interaction between machines is assured via a publish-subscribe messaging system. Each machine reconfigures itself in a decentralized way. The protocol supports virtual machine failures, and the reconfiguration always terminates successfully even in the presence of a finite number of failures. Due to the high degree of parallelism inherent to these applications, the protocol was specified using the LNT value-passing process algebra and verified using the model checking tools available in the CADP toolbox. The use of formal specification languages and tools helped to detect several bugs and to improve the protocol.

Introduction

Cloud computing leverages hosting platforms based on virtualization and provides resources and software applications as service over the network (such as the Internet). It allows users to benefit from these services without requiring expertise in each of them. For service providers, this gives the opportunity to develop, deploy, and sell cloud applications worldwide without having to invest upfront in expensive IT infrastructure.

Cloud applications are intricate distributed applications composed of a set of virtual machines (VMs) running a set of interconnected software components. Cloud users need to (re)configure and monitor applications during their time life for elasticity or maintenance purposes. Therefore, after deployment of these applications, some reconfiguration operations are required for setting up new virtual machines, replicating some of them, destroying or adding virtual machines, handling VM failures, and adding or removing components hosted on a VM. Some of these tasks are executed in parallel, which complicates their correct execution.

Existing protocols [START_REF] Etchevers | Automated Configuration of Legacy Applications in the Cloud[END_REF][START_REF] Fischer | Engage: A Deployment Management System[END_REF][START_REF] Salaün | Verification of a Self-configuration Protocol for Distributed Applications in the Cloud[END_REF] focus mainly on self-deployment issues where the model of application (the number of virtual machines, components, ports, and connections between components) is known before the application execution. These approaches manage static applications which do not require to be changed after the deployment phase. Existing deployment solutions barely take into account configuration parameters. Unlike these static applications, cloud applications need to be reconfigured in order to include new requirements, to fulfill the users expectations, or to perform failure recovery. More specifically, cloud users need protocols that are not only limited to deploy specific applications, but that are also able to modify applications during their execution and take into account the changes that can occur such as the failure of some virtual machine.

In this article, we introduce a novel protocol which aims at automatically deploying and (re)configuring applications in the cloud. These applications are composed of multiple and interconnected software components hosted on separate virtual machines. A reconfiguration manager guides the reconfiguration tasks by instantiating new VMs or destroying/repairing existing VMs. The reconfiguration manager may also apply a number of architectural changes to the application by adding new components or removing existing components hosted on a specific VM. After the creation of a component due to the instantiation of a VM or to a component addition request, the proto-col is responsible for starting all components in the correct order according to the architectural dependencies. Each VM embeds a local reconfiguration agent that interacts with the other remote agents. For each component, the VM agent tries to satisfy its required services by connecting them to their providers in order to start the component. The component cannot be started before the components it depends on. The provider of the service can be hosted on the same VM or on another VM. When a VM receives a VM destruction or a component removal request from the reconfiguration manager, it tries to stop and unbind each component. A component cannot stop before all partner components connected to it have unbound themselves. In order to exchange messages and bind/start/unbind/stop components, VMs communicate together through a publish-subscribe messaging system. The protocol is also able to detect VM failures that occur to a running application. When a VM failure occurs, the protocol notifies the VMs that are impacted. The protocol supports multiple failures. It always succeeds in finally reconfiguring the application at hand and stopping/starting all components.

Our management protocol implies a high degree of parallelism. Hence, we decided to use formal techniques and tools to specify, verify the protocol, and ensure that it preserves important architectural invariants (e.g., a started component cannot be connected to a stopped component) and satisfies certain properties (e.g., each VM failure is followed by a new creation of that VM). The protocol was specified using the specification language LOTOS NT (LNT for short) [START_REF] Champelovier | Reference Manual of the LOTOS NT to LOTOS Translator (Version 5.4)[END_REF], which is an improved version of LOTOS [START_REF] Iso/Iec | LOTOS -A Formal Description Technique Based on the Temporal Ordering of Observational Behaviour[END_REF], and verified with the CADP verification toolbox [START_REF] Garavel | CADP 2010: A Toolbox for the Construction and Analysis of Distributed Processes[END_REF]. For verification purposes, we used 600 hand-crafted examples (application models and reconfiguration scenarios). For each example, we generated the Labelled Transition System (LTS) from the LNT specification and we checked on them about 40 properties that must be respected by the protocol during its application. To do so, we used the model checking tools available in the CADP toolbox. These formal techniques and tools helped us improve the protocol by (i) detecting several issues and bugs, and by (ii) correcting them systematically in the corresponding Java implementation.

Our main contributions with respect to related approaches are the following:

• We propose a novel protocol, which reconfigures cloud applications consisting of a set of interconnected software components distributed over remote virtual machines.

• The protocol is fault-tolerant in the sense that it is able to detect and repair VM failures.

• The protocol was verified using model checking techniques and is implemented in Java.

The outline of this article is as follows. Section 2 introduces the reconfiguration protocol and presents how it works on some concrete applications. We present in Section 3 the LNT specification of the protocol and its verification using CADP. Section 4 reviews related work and Section 5 concludes the article.

Reconfiguration Protocol

This section successively presents the application model, the protocol participants, the protocol itself including the different possible reconfiguration operations, and an overview of the Java implementation.

Application Model

In this section, we present an abstraction of the model, which is sufficient for explaining the protocol principles. The real model exhibits more details such as port numbers, URLs, and other implementation details. The model we use here is used for verifying the soundness of the protocol but its primary role is to keep track of the VMs and components currently deployed in a cloud application. An application is composed of a set of interconnected software components hosted on different virtual machines (VMs). Each component may provide services via exports and require services via imports. Ports are typed and match when they share the same type. One export can provide its service to several components and can thus be connected to several imports. An import must be connected to one export only provided by a component hosted on the same machine (local binding) or a component hosted on another machine (remote binding). When many exports provide the same service, the import is bound to one of them which is randomly chosen by the publish-subscribe system. The import can be mandatory or optional. A mandatory import represents a service required by the component to be functional. Therefore, if the component needs mandatory imports, it cannot be started before all its imports are satisfied (i.e., all mandatory imports are connected to started components). On the other side, an optional import is a service needed by the component but not necessary for starting it. When a component has an optional service, it can be started before the component that provides it, which makes our model supports circular dependencies that involve at least one optional import. Hence, the connection of an optional import may be achieved after the start-up of the service requester and provider. Both kinds of ports are usual in component-based applications. Our protocol does not distinguish port types during the port resolution and (un)binding phases, but does when starting / stopping components. A component used in this model has three states, namely, stopped, started, and failed. Initially, when the VM is instantiated, all its hosted components are stopped. For each component, once all its mandatory imports (if any mandatory import exists) are bound to started components, the component can be started. Reversely the component must stop when at least one of the components to which it is connected through mandatory import requires to stop. When the VM fails, all its components are failed. This model is classic for designing autonomous protocols and has been used for describing, deploying, and reconfiguring real-world applications (see e.g., [START_REF] Kirschnick | Towards an Architecture for Deploying Elastic Services in the Cloud[END_REF][START_REF] Brogi | SeaClouds: Seamless Adaptive Multi-Cloud Management of Service-Based Applications[END_REF][START_REF] Palma | J2EE Applications Deployment: A First Experiment[END_REF][START_REF] Etchevers | Automated Configuration of Legacy Applications in the Cloud[END_REF][START_REF] Fischer | Engage: A Deployment Management System[END_REF][START_REF] Salaün | Verification of a Self-configuration Protocol for Distributed Applications in the Cloud[END_REF]). It is expressive enough for reconfiguration purposes, but should be enhanced for other tasks. For instance, if one's interest is quality of service, we would need more information in the model. Apache1 has a mandatory import that is Workers1. Therefore, Apache1 cannot be started before the start-up of the Workers1 provider. Apache2 has an optional import that is Workers2. Thus, it can be started before the startup of Workers2 provider. Both VM2 and VM3 are hosting one component (Tomcat and MySQL respectively). Tomcat provides two services that are Workers1 and Workers2 and has a mandatory import that is Data. Therefore, Tomcat cannot be started before the Data provider. MySQL does not require any service. Therefore, it can be started immediately.

Protocol Participants

The management protocol includes three participants as showed in Figure 2. The reconfiguration manager (RM) guides the application reconfiguration by posting reconfiguration operations (e.g., instantiating/destroying VMs, adding/removing components) that are described in a reconfiguration scenario. The RM is also in charge of repairing a VM failure by creating a new instance of the failed VM. Each VM is equipped with a reconfiguration agent (agent for short in the rest of this article) that is in charge of (dis)connecting bindings and starting/stopping components upon reception of VM instantiation/destruction and adding/removing reconfiguration operations from the RM. The publish-subscribe messaging system (PS) supports the exchange of communications among all VMs. The PS transfers messages from a machine to others machines. To do so, it contains a list of buffers (a buffer for each VM). Each buffer is used to store the messages exchanged between the agent of its VM and the other agents. When a new VM is instantiated, a buffer for that VM is added to the PS. When an existing VM is destroyed, its buffer is removed from the PS. We assume that the communication model is reliable and messages are never lost during the communication between all participants. The PS also contains two topics:1 (i) the export topic where a component publishes its exports and subscribes its imports, and (ii) an import topic where a component publishes its imports and subscribes its exports.

Protocol Description

The protocol allows to instantiate new VMs/destroy existing VMs, to add a new component to an existing VM or to remove a component from its hosting VM. The protocol also supports VM failures. We explain in this section how the protocol works in these different situations.

Start-up

The RM guides the application reconfiguration by instantiating new VMs and also adding components to an existing VM. In both cases, the goal of the VM agent is to start components.

We explain first how the protocol works in order to add a component to a running application and start it. We present in Figure 3 the agent behavior when the component has mandatory imports only. First the agent receives an add component request () from the RM. When the component provides services, for each service, it subscribes to the import topic and then publishes the service to the export topic (). Then, if the component does not have any import, it starts immediately. Otherwise, each mandatory import requires an export with the same type provided by another component hosted on the same VM or on another VM. To be functional, the component expects that all its mandatory imports will be connected to started components. Therefore, for each mandatory import, the component subscribes to the export topic and then publishes the import to the import topic (). The PS receives that message and checks the import topic. If it does not find a provider for the service, the publication message is deleted. If it finds more than one service provider, the PS picks one randomly and sends a message with binding details and component state. Upon reception of that message (), the import binds to this compatible export (). Then, the VM agent sends a binding message () to the PS. When all the mandatory imports are connected and all the partner components have been started, the VM agent starts the component () and sends a started message to the PS (). When the component has also optional imports, it can start even if these imports are not satisfied. For each optional import, it subscribes to the export topic and publishes the import to the import topic. Upon reception of a message with binding details and component state, the import binds to this compatible export only if the component state is started. Second, we present how the protocol works to add a new VM to a running application. Once the RM instantiates a new VM, a buffer for this VM is added to the list of the PS buffers. After the creation of the new VM, its agent is in charge of starting all the components hosted on this VM. For this, it considers each component hosted on the new VM like a new component that will be added to an existing VM (see explanations above).

Shutdown

The second goal of the protocol is to remove existing components from a VM or to destroy an existing VM from a running application.

We present first how the protocol works when the RM requires the removal of a component from a VM as depicted in Figure 4. When the agent receives the remove component request from the RM (), it tries to stop the component without violating any architectural invariants (e.g., a started component cannot be connected to a stopped component). To do so, if the component does not provide any export, it stops immediately (). Then it unbinds () all its connections and sends an "unbind confirmed" message for each import (). When the component provides services, before stopping it, all components bound to it through mandatory imports must stop and then unbind in order to restore consistency of the whole application. Components bound to it through optional imports, need only to unbind without stopping. Therefore, for each export, it unsubscribes from the import topic () and then sends "an ask to unbind" message () to the PS. Then , it waits until all components bound to it through mandatory imports stop and then disconnect. Components bound to it through optional imports need only to disconnect. When the PS receives an "ask to unbind" message, it transmits it to all components subscribed to that export. It notifies the component that need to stop when another component connected to it has unbound by sending an "unbind confirmed" message (). Once all components connected to it have effectively unbound, it can stop itself (), unbind all its imports (), and send an "unbind confirmed" message to the PS (). When a component receives an "ask to unbind" message (Figure 5), it can remain in the same state and unbinds directly if it is bound through an optional import. If it is bound through a mandatory import, the protocol handles it as done for the component that needs to be removed. The only differences between stopping a component that will be removed and a component that receives an "ask to unbind" message are that, the second one should not unsubscribe from the import topic if it provides exports and after unbinding, it publishes its import in order to connect to another export proposed by the publish-subscribe system (). The component shutdown implies a backward propagation of "ask to unbind" messages and, when this first propagation ends (on components with no export or optional imports only), a second forward propagation of "unbind confirmed" messages starts to let the components know that the disconnection has been actually achieved.

When the RM sends a destruction VM request, the VM agent must properly stop all the components hosted on that VM as well as all components bound to them. Therefore, for each component hosted on the VM that will be destroyed, it behaves as if it has received a remove component request. Once all components are removed, the VM is finally destroyed (see explanations above).

VM Failures

VM failures and component failures can occur at any time to a running application (e.g., during a reconfiguration). We present in this section only the VM failure. A component failure is a specific case of a VM failure, so this is not a fundamental addition to the current protocol. When a VM fails, all its hosted components stop unexpectedly without alerting any partner components. Therefore, we can be in a situation where started components are connected to failed components. In order to restore the application consistency (i.e., architectural invariants), VM failures must be handled immediately. We explain in this section how the protocol takes into account VM failures and how it works to manage them (Fig. 6). The protocol supports also the case of multiple failures.

When a VM is instantiated, its agent interacts with the RM by periodically sending an "alive" message. The RM is configured to receive this message periodically from each agent. As long as the RM receives these "alive" messages from each agent within a specific delay, it considers that its VM is working correctly and still alive [START_REF] Bertier | Implementation and Performance Evaluation of an Adaptable Failure Detector[END_REF] (). Once the RM does not receive one of these "alive" messages from an agent before the delay elapses, it assumes that its VM has failed (). In that case, it alerts the PS () and then starts the repair phase by creating a new instance of the failed VM (). The new VM behaves as if the machine is instantiated for the first time (see Section 2.3.1). When the PS receives an "alert failure" message from the RM (), it unsubscribes each failed component exporting services from the import topic to avoid that other components try to connect to it (). Then, it warns the other VMs of this failure by:

• sending messages notifying all components bound to the failed components about the VM failure and asking them to unbind (). When an agent receives this kind of message, it tries to stop the impacted component if it is bound through a mandatory import or remains in the same state if it is bound through optional import. Then it unbinds it and tries to connect the disconnected import in order to restart the component as presented in Section 2.3.2;

• sending an "unbind confirmed" message to each component to which a failed component was connected via mandatory or optional import (). The reception of this message by a component that needs to stop indicates the disconnection has been actually achieved. In the case of a component failure, the agent of the VM on which it is hosted informs the PS and then creates a new instance of the failed component. The new component behaves as a component added to the application for the first time. When the PS receives the component failure alert, it reacts in the same way as for each component hosted on a failed VM.

Examples

We present in this section an example of removal and addition of a component to the application showed in Figure 1, as well as an example of VM failure. In this example, we begin with a running application where all components are connected and started.

A scenario of component removal

As it is depicted in Figure 8, the RM requests the VM2 agent to remove Tomcat (RM.1). Once VM2 receives the request, it aims to stop the Tomcat component before removing it. To do so, all components connected to the Tomcat must be stopped before. Tomcat provides two services Work-ers1 and Workers2. Thus, for each export, it unsubscribes from the import topic (A2.1 and A2.3) and sends messages to the PS asking it to unbind all components connected to it through Workers1 and Workers2 (A2.2 and A2.4). The PS receives these messages, checks the export topic and finds that Apache1 (Apache2 respectively) hosted on VM1 imports Workers1 (Workers2 respectively) from Tomcat. Therefore, it sends "ask to unbind" messages to Apache1 and Apache2 (PS.1 and PS.2). When VM1 receives these messages, Apache1 does not provide any service and it is bound to the Tomcat component through a mandatory import, so it is immediately stopped (A1.1). Then, it is unbound from Tomcat, sends an "unbind confirmed" message to the PS (A1.2), and publishes its import to the import topic (A1.3). VM2 receives that message from the PS (PS.3) but cannot stop the Tomcat component because Apache2 is still connected to it. Apache2 is connected to the Tomcat component through an optional import. Thus, it is only unbound from Tomcat without stopping, then sends an "unbind confirmed" message to the PS (A1.4), and publishes its import to the import topic (A1.5). The PS checks the import topic but there is no component that provides Workers1 or Workers2. VM2 receives the "unbind confirmed" message from the PS (PS.4). Tomcat has no component bound to it any more, so it is stopped (A2.5). Tomcat is unbound from MySQL and the VM2 agent sends an "unbind confirmed" message to the PS (A2.6). The PS finally sends that message to the MySQL component (PS.5).

A scenario of component addition

We present in this section an example of component addition to an existing VM. We show how to add a new instance of Tomcat to VM2 after removing it in Section 2.4.1.

VM2 receives the Tomcat addition request from the RM (1). The Tomcat component requires a mandatory service whose type is Data. Therefore, it subscribes to the export topic and then publishes its import to the import topic (A2.1). Tomcat provides two services Workers1 and Workers2. There-fore, for each export it subscribes to the import topic and then publishes it to the export topic (A2.2 and A2.3). The PS receives the first message from the VM2 agent, checks the import topic and finds that only MySQL provides a Data service (it has subscribed to the import topic). The PS notifies VM3 that there is a Tomcat that needs Data (PS.1). When Tomcat publishes its exports, the PS forwards the binding details and Tomcat state to Apache1 because it has subscribed to the export topic for Workers1 (PS.2) (Apache2 respectively because it has subscribed to the export topic for Workers2 (PS.3)). When VM1 receives the binding details and Tomcat state, Apache1 connects to Tomcat (A1.1) but it cannot start because the Tomcat state is stopped. Apache2 cannot connect to Tomcat because it is started and Tomcat is still stopped. After receiving the notification message from the PS about the Tomcat component need (PS.1), VM3 sends the MySQL binding details and state that it is started (A3.1). The PS receives the start-up information from the VM3 agent, checks and finds that the Tomcat component has required this service (it has subscribed to the export topic). Hence, a message with binding details and MySQL's state is added to VM2 buffer (PS.4). Upon reception of this message, the Tomcat component is bound to the mySQL component (A2.4) and the VM2 agent starts the Tomcat component (A2.5). Then, the Tomcat component publishes a started message containing its new state (A2.6). The PS receives that message and forwards it to VM1 (PS.5). Upon reception of this message, the VM1 agent starts the Apache1 component (A1.2). Apache2 can finally connect to the Tomcat component (A1.3).

A scenario of VM Failure repair

We present in this section an example of failure/repair of VM2. When VM2 fails, Tomcat is suddenly stopped without alerting the components bound to it. Therefore, Apache1 and Apache2 that are started are bound to a stopped component. When the RM detects the failure of VM2 (RM.1), it immediately alerts the PS (RM.2). Then, the RM creates a new instance of VM2 (RM.3). When the PS receives the alert message from the RM announcing the VM2 failure, it unsubscribes Tomcat from the import topic (PS.1). Then, it checks the export topic in order to find the impacted components. Thus, it finds that Apache1 and Apache2 are connected to Tomcat. Therefore, it notifies them about the failure (PS.2 and PS.3). When VM1 receives the notification Figure 9: The participants behavior when adding the Tomcat component messages, Apache1 does not provide any service and it is connect to Tomcat through a mandatory import so it is immediately stopped (A1.1). It is also unbound from the Tomcat component, sends an "unbind confirmed" message to the PS (A1.2), and then publishes its import to the import topic (A1.3). Apache2 does not provide any service and is connected to the failed component through an optional import so it is unbound from Tomcat without stopping, sends an "unbind confirmed" message to the PS (A1.4), and then publishes its import to the import topic (A1.5). After the creation of a new instance of VM2, each agent starts the components impacted by the failure as presented in Section 2.3.1.

Implementation

We present in this section some implementation details concerning the protocol. The core of the system of our implementation is roughly 6K lines of Java code. It is based on a IaaS abstraction layer that allows to instantiate VMs on different IaaSs (such as Amazon EC2 and Microsoft Azure) and on RabbitMQ [3], which is an implementation of the AMQP standard [1]. It is a message server, implementing the publish-subscribe messaging system. It is mainly used for the communication between VMs and RM. We chose an AMQP communication system in order to have a reliable and asynchronous communication system.

When the user requests the deployment of a new software instance, the RM first checks about the VM instance defined in the software instance model. If the user asks to deploy the software application on an already existing VM instance, the RM immediately sends the model to the VM. Otherwise, the RM checks if the software type of the software instance has a VM type defined. If so, the RM asks the IaaS to instantiate one VM of this kind. Otherwise, the RM asks the IaaS to instantiate a VM from the default VM template. When the RM asks the IaaS to instantiate a VM, it creates a message buffer on the message server for that VM.

When the RM sends the software instance model to the VM instance, it serializes the software instance object and sends it to the message buffer of the VM along with the configuration files (Puppet recipes for example). This part can be done even when the VM is not running thanks to the messages stored in its message buffer. When the VM boots, the agent starts, connects to the message buffer and gets the message.

The agent on the VM gets the software instance model and the configuration files associated with it. It checks what connector it has to use to perform the operations for the software instance. A connector is a Java class that implements four simple operations: setup, update, start, and stop. A connector is independent from any software it will install, it only does basic operations. The operations related to the software are located in the configuration files. Each connector, when calling a basic operation, transmits the configuration of the model (such as variables and imported variables) to the packaging and configuration system. This mechanism enables the user to separate actual operations on VM from binding details. Multiple connectors enable users to keep the original way of installing and configuring the software. In addition, it also enables to cover almost any kind of software: from software available in Linux repositories to legacy software. We implemented a Puppet [2] connector in order to install and update software on VMs. Puppet is one of the most known configuration system. It provides a language and a program. The language enables to describe the state of a system by describing its packages, files and services.

When the installation is completed (software instances are installed on VMs), each agent publish its configuration (according to the exports) and subscribe to other remote configuration (according to the imports) by using the RabbitMQ API.

Specification and Verification

In this section, we present the specification of the protocol in LNT [START_REF] Champelovier | Reference Manual of the LOTOS NT to LOTOS Translator (Version 5.4)[END_REF], an input language of CADP [START_REF] Garavel | CADP 2010: A Toolbox for the Construction and Analysis of Distributed Processes[END_REF]. LNT is an improved and simplified version of LOTOS [START_REF] Iso/Iec | LOTOS -A Formal Description Technique Based on the Temporal Ordering of Observational Behaviour[END_REF]. This language is expressive enough for specifying the reconfiguration protocol, in particular it supports the description of complex data types and concurrent processes. Its user-friendly notation simplifies the specification writing. LNT processes are built from actions, choices (select), parallel composition (par), looping behaviors (loop), conditions (if ), and sequential composition (;). The communication between the protocol participants is carried out by rendezvous on a list of synchronized actions included in the parallel composition (par). The specification is analyzed using CADP [START_REF] Garavel | CADP 2010: A Toolbox for the Construction and Analysis of Distributed Processes[END_REF]. CADP is a verification toolbox dedicated to the design, analysis, and verification of asynchronous systems consisting of concurrent processes interacting via message passing. The toolbox contains many tools that can be used to make different analysis such as simulation, model checking, equivalence checking, compositional verification, test case generation, or performance evaluation. Therefore, we rely on the state-of-the-art verification tools provided by CADP to check that the protocol respects some important properties.

In the rest of this section, we present the specification of the protocol in LNT, its verification using the CADP model checker (Evaluator), some experimental results, and problems detected and corrected during the verification process. It is worth noting that since these techniques and tools work on finite state spaces only, although dynamic reconfiguration may apply infinitely, we use only finite models and scenarios for verification purposes in this section.

Specification

The number of lines of processes depends on the size of the application model (the number of VM, component and ports). Processes are generated for each input application model2 , because a part of the LNT code depends on the number of VMs and on their identifiers. Therefore, the number of lines for processes grows with the number of VMs in the application model. The specification of the protocol consists of three parts: data types (200 lines), functions (800 lines), and processes (1,500 lines). The number given above corresponds to an example with three VMs.

Data types

They are used to describe the distributed application model (VMs, components, ports), the communication model (binding between components, messages, buffers, and topics), and the component states. We show below a few examples of data types. The application model (TModel) consists of a set of virtual machines (TVM). Each VM has an identifier (TID) and a set of components (TSoftware).

type TModel is set of TVM end type type TVM is tvm (idvm: TID, cs: TSoftware) end type type TSoftware is set of TComponent end type

Functions

They apply on data expressions. Functions are used to define all the computations necessary for reconfiguration purposes (e.g., extracting information from the application, describing buffers and basic operations on them like adding/retrieving messages, changing the state of a component, keeping track of the started/unbound components, verifying the satisfaction of the imports, etc.). Let us show, for illustration purposes, an example of function that aims at removing a message from a buffer by using the FIFO strategy. This strategy consists in removing the message from the beginning and adding a new message at the end of the buffer. The remove function takes as input a buffer (q) which type is (TBuffer) that is composed of an identifier (TID) and a list of messages (TMessage). If the buffer is empty, nothing happens. When the buffer is not empty, the first message is removed.

function remove_MSG (q: TBUFFER): TBUFFER is case q in var name: TID, hd: TMessage, tl: TQueue in | tbuffer(name,nil) -> return q | tbuffer(name,cons(hd,tl)) -> return tbuffer(name,tl) end case end function

Processes

They are used to specify the participants of the protocol (the reconfiguration manager, the publish-subscribe messaging server, and an agent per VM). The reconfiguration manager guides the application reconfiguration. Each agent drives the behavior of its VM and encodes most of the protocol functionality in order to start/stop all the components hosted on its VM. The publish-subscribe messaging system assures the communication between all VMs. Its is equipped by a set of FIFO buffers (a buffer for each VM in the application). Each participant is specified as an LNT process and involves two sort of actions: actions which correspond to interactions with the other participants such as PStoAGENT that presents the message transferred from the publish-subscribe messaging system processes to the agent processes, AGENTtoPS that presents the message transferred from the agent processes to the publish-subscribe messaging system. The second type of action taggs specific moments of the protocol execution such as the VM instantiation/destruction, the component start-up/shutdown, the component addition/removal, the effective binding/unbinding of an import to an export, the failure of a VM, etc.

For illustration purposes, we present the LNT process main (named MAIN) generated for an example of application model involving three VMs. The LNT parallel composition is described with par followed by a set of synchronization actions that must synchronize together. Two processes synchronize if they share the same action. We can see that the agents do not interact directly together and evolve independently from one another. The VM agents communicate together through the PS. Each agent is identified using the VM name and synchronizes with the PS on AGENTtoPSi action when sending a message to the PS and PStoAGENTi action (i = 1, 2, 3) when receiving a message from it. Each agent defines actions for port binding (BINDCOMPO), for starting a component (STARTCOMPO), for stopping a component (STOPCOMPO), etc. The PS is initialized with a buffer per VM and two topics for imports/exports (ListBuffers). The RM processes is composed validate our protocol. From the specification and an example, CADP exploration tools generate an LTS that describes all the possible executions of the protocol for each example of application model and scenario. Moreover, we specified 40 properties in MCL [START_REF] Mateescu | A Model Checking Language for Concurrent Value-Passing Systems[END_REF], the temporal logic used in CADP. MCL is an extension of alternation-free µ-calculus with regular expressions, data-based constructs, and fairness operators. These properties helped us to chase bugs when finding them during the development phase. We use model checking to verify that they are respected during the protocol execution. There is an exception that when a VM failure appears, some properties are not respected (e.g., a started component cannot be connected to a stopped one). The model checker automatically says whether these properties are not verified on the LTS. When a bug is detected by model checking tools, it is identified with a counterexample (a sequence of actions violating the property). We distinguish two kinds of properties: (i) those allowing to focus on the protocol behavior for verifying that the final objectives are executed (Prop. 1 below for instance) and guaranteeing that the architectural invariants for a reconfigurable application are always satisfied (Prop. 2), (ii) and those helping us to identify more precisely the source of error when one of the original properties was violated by verifying that the progress/ordering constraints are respected (Prop. 3, 4, 5, and 6). Following the scenarios that we want to check, these properties belong to different categories: properties dedicated to start-up scenarios (Prop. 1 and 2), destruction scenarios (Prop. 3), mixed scenarios (Prop. 4), and VM failure scenarios (Prop. 5, and 6). We present in this section some concrete properties verified on the application model showed in Figure 1: 1. All components are eventually started. This property is automatically generated from the application model, because it depends on the name of all VMs and components hosted on each VM.

2. A component cannot be started before the components on which it depends for mandatory imports. (not "STARTCOMPO !Apache1 !VM1")* ."STOPCOMPO !Tomcat !VM2"

) . (not "STARTCOMPO !Tomcat !VM2")* ."STARTCOMPO !Apache1 !VM1" ] false
In the example of application showed in Figure 1, the Apache1 component is connected to the Tomcat component on a mandatory import. Therefore, we must never find a sequence where Apache1 is started before Tomcat, or a sequence where Apache1 is stopped, the Tomcat server is then stopped, and Apache1 is started again before Tomcat. This property is automatically generated from the application model because it depends on the component and VM names in the application model.

3. All components hosted on a VM eventually stop after that VM receives a destruction request from the DM. This property uses the macro inev (M), which indicates that a transition labeled with M eventually occurs. This macro is defined as follows:

macro inev (M) = mu x .( < true > true and [ not M ] X ) end macro
This property does not depend on the application. It can be verified for any application without knowing the name of VMs and components. Parameters can be related in MCL by using variables in action parameters (e.g., vm for the virtual machine identifier and cid for the component identifier). This property shows the data-based features that are available in MCL.

4. There is no sequence where an import (mandatory or optional) is bound twice without an unbind in between.

[ true* .

"BINDCOMPO !Apache1 !Workers1" .

( not "UNBINDCOMPO !Apache1 !VM1" )* .

"BINDCOMPO !Apache1 !Workers1" ] false
When a component is connected to another component through an import (mandatory or optional), it cannot be bound again except if it is unbound before.

5. There is no sequence with two VM instantiations without a failure or a destroy in between.

[ true* .

"INSTANTIATEVM1" .

( not "FAILURE !VM1 or DESTROY !VM1" )* .

"INSTANTIATEVM1"

] false

When a VM is instantiated, it cannot be instantiated again except if this VM is destroyed or failed.

6. A failure action in the VM is eventually followed by an alert of this failure

[ true* . { FAILURE ?vm:String } ] inev ( { ALERTPS !vm } )
This property does not depend on the application. The variable vm (the virtual machine identifier) used as first parameter of FAILURE must be the first parameter in ALERTPS. This property is verified for all applications and for all VM names and also uses the macro inev.

Experiments

We conducted our experiments on more than 600 hand-crafted examples on a Pentium 4 (2.5GHz, 8GB RAM) running Linux. Each example consists of an application model and a specific scenario (a sequence of instantiate/destroy VM operations and add/remove components to/from VMs). From this input, the CADP exploration tools generate the corresponding LTS by enumerating all the possible executions of the system. Finally, the CADP model checker is called, providing as result a set of diagnostics (true or false). The model checker returns true if a property is verified. When a property is not satisfied, it returns false as well as a counterexample. We present in this section experiments that summarize some of the numbers obtained when varying the number of VMs, the number of reconfiguration operations, and the number of failures.

We present in Figure 11 (left) the size of the LTS (transitions) as well as the time to execute the whole process (LTS generation and properties checking) when we modify only the number of VMs (no VM destruction or failure). The number of reconfiguration operations is the same as the VM number (we only instantiate VMs). Increasing the VM number leads to an increase of the number of components and ports. Then, the more VMs and ports, the more parallelism in the system and therefore the more messages exchanged among VMs. Figure 11 (left) shows how the LTS size grows exponentially when we slightly increase the number of VMs in the application. The computation time scales from a few minutes for applications with 1 VM and few ports to a few hours for an application with 4 or more VMs.

Figure 11 (right) summarizes the results obtained for the same application used to obtain results showed in Figure 11 (left) but with a destruction and re-instantiation operations at the end of the scenario. The LTSs size and analysis time increase in a remarkable way even when just adding one destruction operation to the same application. This operation triggers a double propagation, hence more exchanged messages between the PS and the agents.

Table 1 shows the size of the LTS (states and transitions) before and after minimization (wrt. a strong bisimulation relation) as well as the time to execute the whole process in the last column of the tables (LTS generation and minimization on the one hand, and properties checking on the other). These results are obtained for the application described in Figure 1, with an increasing number of failures (F). The more VMs fails, the more the LTS size and analysis time increase.

Fortunately, our goal here was not to analyze huge systems (with potentially many VMs) during the verification of the protocol, but to find bugs in the protocol. Indeed, most issues were found on small applications describing pathological reconfiguration cases.

Problems Found

We have presented in this section the specification and verification of our protocol. Model checking tools permitted to find bugs that were identified by counterexample analysis. This allowed us to revise several parts and correct specific issues (e.g., adding some acknowledgement messages after binding/unbinding ports, starting/stopping components, etc.) in both the specification and implementation that were written at the same time. During the verification steps, we detected two important issues that we corrected in the latest version of the protocol. The implementation was systematically corrected. In the rest of this section we will focus on these two problems.

In the first version of the protocol, the RM was centralized and in charge of creating VMs, starting and stopping components. Therefore it kept track of the states of components for each VM. To do this, the RM was informed every time there was a change in the application. It communicated with all the agents by exchanging messages in order to update the application after each change in the component architecture (e.g., a component binds to another component, a component changes its state). There was an overhead of messages transmitted to and from the RM. We noticed during our experiments that even with simple applications, CADP generated huge LTSs. We solved this drawback by proposing a decentralized version of the protocol. The new version of the protocol consists of an RM that is not in charge of starting or stopping components. The RM guides only the application reconfiguration by instantiating, destroying, and repairing VMs, or by adding and removing components from an existing VM. It is part of the agent behavior to drive the component start-up/shutdown. The decentralized version of the protocol avoids additional, unnecessary messages exchanged between agents and the RM. This version guarantees more parallelism and better performance in the corresponding implementation of the protocol.

The second issue that we detected during the verification of the protocol is in the way VMs are destroyed. Originally, when a component required to stop, it was stopped and then all components bound to it were stopped. Stopping components in this order induced started components connected to stopped components. This violated the consistency of the component com-position and well-formedness architectural invariants. This bug was detected thanks to a property stating that " a component cannot be started and connected through an import (mandatory or optional) to a stopped component ". Thus, we corrected this bug by proposing another way to stop components. When a component needs to stop, it requests to all components bound to it to unbind and once it is done, it can immediately stop. This implies first a backward propagation along components bound on mandatory imports. Once this first propagation stops (a component does not provide service or is connected only through optional imports), we start a forward propagation during which components are actually stopped and indicate to their partners that they have just stopped and unbound. This double propagation, as presented in Section 2.3, is necessary for preserving the component architecture consistency and for avoiding that started components can keep on using stopped components.

Discussion

In the final part of this section, we would like to comment on alternative verification techniques we could have used to complement our model checking based approach.

In order to formally analyse the reconfiguration protocol, we specified over 600 application models and reconfiguration scenarios in order to extensively validate our protocol. When achieving these tasks, we paid a lot of attention to cover very different applications and scenarios, in particular pathological and corner cases. Hence, this large investment in validation was helpful in order to detect very early in the development process subtle bugs and issues (see subsection 3.4 for more details). This also makes us highly confident in the correctness of the protocol. However, a limit of our model checking based analysis is that it works on concrete configurations and scenarios. A way to generalise these verification results would be to reason on generic applications and scenarios using for instance parameterised systems verification techniques [START_REF] Zuck | Model Checking and Abstraction to the Aid of Parameterized Systems (a Survey)[END_REF]. The application of these techniques to our work is not straightforward and several difficulties have to be faced and solved. As an example, when we change a reconfiguration scenario by, e.g., removing a reconfiguration operation or by changing the order of the reconfiguration operations, there is no formal relation connecting the LTS generated for the former scenario and the new LTS. Moreover, given an application model, we can infer an infinite number of possible reconfiguration scenarios. Nonetheless, this is a perspective of interest and we plan to study this idea in more details in future work.

Another complementary approach is to prove the correctness of the protocol using theorem proving techniques as achieved with Coq in [START_REF] Boyer | Robust Reconfigurations of Component Assemblies[END_REF] for ensuring the correctness of the reconfiguration of component assemblies. This is a very interesting and ambitious objective, but this would complement the validation of the reconfiguration protocol using model checking techniques presented in this paper, by ensuring that the protocol would work for any application and any reconfiguration scenario.

Related Work

In [START_REF] Chapman | Software Architecture Definition for On-demand Cloud Provisioning[END_REF][START_REF] Goldsack | The SmartFrog Configuration Management Framework[END_REF], the authors propose languages and configuration protocols for distributed applications in the cloud. [START_REF] Chapman | Software Architecture Definition for On-demand Cloud Provisioning[END_REF] adopts a model driven approach with extensions of the Essential Meta-Object Facility (EMOF) abstract syntax to describe a distributed application, its requirements towards the underlying execution platforms, and its architectural constraints (e.g., concerning placement and collocation). Contrary to us, in [START_REF] Chapman | Software Architecture Definition for On-demand Cloud Provisioning[END_REF], the deployment does not work in a decentralized fashion, and this harms the scalability of applications that can be deployed.

A recent related work [START_REF] Fischer | Engage: A Deployment Management System[END_REF] presents a system that manages application stack configuration. It provides techniques to configure services across machines according to their dependencies, to deploy components, and to manage the life cycle of installed resources. This work presents some similarities with ours, but [START_REF] Fischer | Engage: A Deployment Management System[END_REF] does not explain how they preserve composition consistency and architectural invariants when stopping resource drivers. The authors write that going from an active state to an inactive state has as precondition that dependencies are inactive without explaining the mechanism used to deactivate them.

There exist many approaches which focus on specifying and verifying distributed systems and component-based systems. In [START_REF] Kramer | Analysing Dynamic Change in Distributed Software Architectures[END_REF][START_REF] Magee | Dynamic Structure in Software Architectures[END_REF][START_REF] Magee | Behaviour Analysis of Software Architectures[END_REF][START_REF] Allen | Specifying and Analyzing Dynamic Software Architectures[END_REF][START_REF] Wermelinger | A Graph Based Architectural (Re)configuration Language[END_REF][START_REF] Cansado | A Formal Framework for Structural Reconfiguration of Components under Behavioural Adaptation[END_REF][START_REF] Salaün | Generation of Service Wrapper Protocols from Choreography Specifications[END_REF][START_REF] Krause | Modeling Dynamic Reconfigurations in Reo Using High-Level Replacement Systems[END_REF], the authors proposed various formal models (Darwin, Wright, etc.) in order to specify dynamic reconfiguration of component-based systems whose architectures can evolve (addition/removal of components and connections) at run-time. These techniques are adequate for formally designing dynamic applications. In [START_REF] Kramer | Analysing Dynamic Change in Distributed Software Architectures[END_REF][START_REF] Magee | Behaviour Analysis of Software Architectures[END_REF] for instance, the authors show how to formally analyze behavioral models of components using the Labeled Transition System Analyzer. Our focus is quite different here, because we work on a protocol whose goal is to automatically achieve these reconfiguration tasks, and to assure that this protocol respects some key properties during its application.

In [START_REF] Etchevers | Self-Configuration of Distributed Applications in the Cloud[END_REF][START_REF] Etchevers | Automated Configuration of Legacy Applications in the Cloud[END_REF][START_REF] Salaün | Verification of a Self-configuration Protocol for Distributed Applications in the Cloud[END_REF], the authors describe a protocol that automates the configuration of distributed applications in cloud environments. In these applications, all elements are known from the beginning (e.g., numbers of VMs and components, bindings among components, etc.). Moreover, this protocol allows one to automate the application deployment, but not to modify the application at run-time. Another related work is [START_REF] Boyer | Specifying and Verifying the Synergy Reconfiguration Protocol with LOTOS NT and CADP[END_REF], where the authors propose a robust reconfiguration protocol for an architectural assembly of software components. This work does not consider the distribution of components across several VMs, but assumes that they are located on a same VM. In [START_REF] Etchevers | Reliable Self-Deployment of Cloud Applications[END_REF], the authors present a self-deployment protocol able to automatically deploy cloud applications in a decentralized fashion. This protocol supports VM failures by detecting and repairing them, but it does not support reconfiguration features.

In [START_REF] Lascu | Automatic Component Deployment in the Presence of Circular Dependencies[END_REF], the authors present a design and an implementation of a technique for the automatic synthesis of deployment plans. It provides a reconfiguration algorithm to deploy heterogeneous software components and compute the sequence of actions allowing the deployment of a desired configuration. The algorithm works even in the presence of circular dependencies among components. This work presents some similarities with ours, but [START_REF] Lascu | Automatic Component Deployment in the Presence of Circular Dependencies[END_REF] does not provide methods for verifying its techniques and algorithms.

In [START_REF] Catan | Aeolus: Mastering the Complexity of Cloud Application Deployment[END_REF], the authors present the Aeolus component model that aims at mastering the complexity of cloud applications. It automates as much as possible the management of such applications. It uses an initial configuration, an universe of available components and a target component. A component is a grey-box presenting internal states and mechanisms to change its state during the deployment and reconfiguration process. In [START_REF] Catan | Aeolus: Mastering the Complexity of Cloud Application Deployment[END_REF] the initial configuration, target components and actions are known from the beginning but the algorithm/protocol does not support modifications that can take place at run-time.

This article is an extended version of a conference paper published in [START_REF] Abid | Verification of a Dynamic Management Protocol for Cloud Applications[END_REF]. The key additions of this journal version are as follows: (i) introduction of new reconfiguration actions (addition and removal of components), (ii) extension of the protocol in order to detect and repair VM failures, (iii) a detailed presentation of the properties to verify the protocol, especially properties which verify the failure detection and repair, (iv) more experiments especially with multiple VM failures, and (v) presentation of an updated review of related work.

Concluding Remarks

In this article, we have presented a protocol that aims to dynamically reconfigure distributed cloud applications and support VM failures. It enables one to instantiate new VMs/destroy existing VMs and to add new components/remove existing components. Upon reception of these reconfiguration operations, VM agents connect/disconnect and start/stop components in a defined order for preserving the application consistency, which is quite complicated due to the high parallelism degree of the protocol. This protocol does not only detect VM failures but also repairs failures by creating a new instance for each failed VM and by warning the other VMs of this failure. The protocol is robust and fault-tolerant. It succeeds in stopping/starting components hosted on the different virtual machines even in case of multiple failures. The protocol was formally specified and verified using the LNT specification language and the CADP toolbox, which turned out to be very convenient for modeling and analyzing such protocols, see [START_REF] Salaün | An Experience Report on the Verification of Autonomic Protocols in the Cloud[END_REF] for a discussion about this subject. Model checking techniques were used to verify about 40 properties of interest on a large number of application models and reconfiguration scenarios. More importantly, during this verification stage, we improved several parts of the protocol and found several bugs. In particular, we deeply revise the part of the protocol dedicated to the VM destruction and component shutdown. All these issues have been corrected in the corresponding Java implementation.

Figure 1 :

 1 Figure 1: Example of an application model

Figure 2 :

 2 Figure 2: Protocol participants

Figure 3 :

 3 Figure 3: The Agent behavior when adding a new component with mandatory imports only

Figure 4 :

 4 Figure 4: The agent behavior when removing a component

Figure 5 :

 5 Figure 5: The agent behavior when stopping a component

Figure 6 :

 6 Figure 6: The RM behavior when detecting a VM failure

Figure 7 :

 7 Figure 7: The PS behavior when receiving an alert failure message

Figure 10 :

 10 Figure 10: The participants behavior when detecting the VM2 failure

(

  µX . ( < true > true and [ not "STARTCOMPO !Apache1 !VM1" ] X ) ) and . . .

and(

  µX . ( < true > true and [ not "STARTCOMPO !MySQL !VM3" ] X ) )

[(

  "nil" or true* . "STOPCOMPO !Apache1 !VM1" .

[

  true* . { DESTROYVM ?vm:String } ] inev ( { STOPCOMPO ?cid:String !vm } )

Figure 11 :

 11 Figure 11: Experimental results when increasing the number of VMs (left) start-up scenario without failure, (right) start-up and destruction scenario without failure

Table 1 :

 1 Experimental results (with failures)

	F	LTS (states/transitions)	Time (m:s)
		raw	minimized	LTS gen. / Verif.
	0	452,378/983,963	8,531/29,394	9:21 / 1:84
	1 612,293/1,262,732 9,568/31,472	10:37 / 1:79
	2 682,459/1,420,543 12,390/38,971	16:59 / 2:83
	3 793,813/1,584,238 16,673/48,562	24:73 / 3:69
	4 993,527/1,763,227 19,586/63,254	31:91 / 4:56

A topic is a logical channel where messages are published and subscribers to a topic receive messages published on that topic.

We developed an LNT code generator in Python for automating this task.

Acknowledgements. This work has been supported by the OpenCloudware project (2012-2015), which is funded by the French Fonds national pour la Société Numérique (FSN), and is supported by Pôles Minalogic, Systematic, and SCS. The authors would like to thank Radu Mateescu for his help during the formulation of MCL properties.

in parallel with the rest of system and synchronizes with the other processes on many actions. For example, the RM defines actions for VM creation and destruction (INSTANTIATEVMi (i = 1, 2, 3) and DESTROYVM, resp.). The RM guides also the application reconfiguration by adding and removing components from VMs (ADDCP and REMOVECP). When the RM detects a VM failure (FAILURE), it alerts the PS by an ALERTPS action.

All these actions are used for analyzing the protocol as we will see in the next subsection.

Verification

We apply the LNT specification of the protocol to a set of 600 examples (application models and reconfiguration scenarios) in order to extensively


D Martin

S Fougnot

F Grobost

S Thibaut-Jovelin

F Ballereau

T Gueudet

D De Mouy

Jérôme Robert
email: jerome.robert@psl.aphp.fr

Onerba-Ville Network

Prevalence of extended-spectrum beta-lactamase producing Escherichia coli in community-onset urinary tract infections in France in 2013

Keywords: Escherichia coli, ESBL, urinary-tract infection, community, fosfomycin, nitrofurantoin, Klebsiella pneumoniae

Objectives. We sought to assess the importance of extended-spectrum beta-lactamase (ESBL) producing Enterobacteriaceae in urinary tract infections in outpatients in France.

Methods. Retrospective laboratory based survey analysing susceptibility patterns of

Escherichia coli and Klebsiella pneumoniae isolates providing from urines collected from outpatients during three months in 2013.

Results

. 499 laboratories collected data on 51,643 E. coli and 3,495 K. pneumoniae isolates.

The overall proportion of ESBL-producing E. coli was 3.3%. The proportion was higher for males (4.8%) than for females (3.0%) and increased with age: 2% for patients <20 years to 5.4% for those aged >80 years. More than 95% of isolates we susceptible to cefixime, fosfomycin, and nitrofurantoin. In nursing homes, the ESBL-producing E. coli proportion was 12.1%. For K. pneumoniae, the proportion of ESBL-positive isolates was 6.6%, and this proportion increased with age. Data from 2010 collected from a subset of the network showed that the ESBL-producing E. coli proportion was 2.0%.

Conclusion.

ESBL-producing isolates were rather frequent in urines in French outpatients in 2013. Males and persons residing in nursing homes were at higher risk of ESBL-positive infection. Despite the increase in ESBL-positive isolates, the susceptibility to antibiotics used to treat cystitis remains high.

Introduction

The worldwide rise of antimicrobial resistance conducted many countries to develop national plans to control this public health threat. [START_REF]Antimicrobial resistance surveillance in Europe[END_REF][START_REF]Antimicrobial resistance -Global report on surveillance[END_REF] After promising results of its first plans, France is currently in the middle of its third antibiotic sparing plan. [START_REF] Schlemmer | Antibiotic sparing campaigns and the French Antibiotic Plan[END_REF] In a majority of these plans, surveillance of antibiotic resistance is recognised as a core issue. The goals for such surveillance have been listed elsewhere. [START_REF] Cornaglia | European recommendations for antimicrobial resistance surveillance[END_REF] In particular, surveillance data should help in establishing guidelines for empirical treatment when antibiotic susceptibility tests results are not yet available or will not be performed. In addition, up-to-date data are of interest to assess the accuracy of already published guidelines.

Urinary tract infections (UTI) are among the most common bacterial infections that are treated in the community by an empirical antibiotic treatment regimen. In many countries, it is currently not recommended to perform urinalysis for cystitis before treatment, and the choice of the antibiotic regimen relies on the epidemiology of antibiotic resistance.

Escherichia coli, which is a commensal species of the digestive tract, is the most common bacterial species isolated in UTI. The increase in resistance of E. coli to extended-spectrum cephalosporins (ESC) is now well documented, and is mainly due to the production of extended-spectrum beta-lactamase (ESBL) in the hospital setting as well as in the community. [START_REF]Antimicrobial resistance surveillance in Europe[END_REF][START_REF] Arpin | Nationwide survey of extended-spectrum beta-lactamase-producing Enterobacteriaceae in the French community setting[END_REF] In France for instance, there has been a 10-fold increase in the digestive carriage of ESBL-producing E. coli in the community in the last years. [START_REF] Gruson | 10-Fold increase (2006-11) in the rate of healthy subjects with extendedspectrum β-lactamase-producing Escherichia coli faecal carriage in a Parisian check-up centre[END_REF] The increase in ESBL-producing E. coli makes the treatment of community-onset UTI more complex because such isolates are usually multidrug-resistant, which increases the risk of treatment failure. [START_REF]Antimicrobial resistance surveillance in Europe[END_REF][START_REF]Antimicrobial resistance -Global report on surveillance[END_REF][START_REF] Esteve-Palau | Clinical and economic impact of urinary tract Infections caused by ESBL-producing Escherichia coli requiring hospitalization: a matched cohort study[END_REF] In addition, treating ESBL-positive infection is more costly that treating their susceptible counterpart. [START_REF] Esteve-Palau | Clinical and economic impact of urinary tract Infections caused by ESBL-producing Escherichia coli requiring hospitalization: a matched cohort study[END_REF] Therefore, it is of interest to gather up-to-date data on the prevalence of antibiotic resistance of E. coli isolated from UTIs in the community.

M A N U S C R I P T A C C E P T E D ACCEPTED MANUSCRIPT

Materials and methods

Laboratories

Private practice laboratories participating in one of the three pre-existing networks (Epiville, MedQual-ville, Aforcopi-Bio) of the national observatory for epidemiology of bacterial resistance to antibiotics (ONERBA), and to a fourth network previously set-up for other purposes than surveillance of bacterial resistance (BPR network) were asked to participate on a voluntary basis. A special attention has been paid to national coverage of the network. A total of 499 private practice laboratories distributed throughout metropolitan France, and that referred urines clinical samples to 43 bacteriological centres participated into the network.

Bacteriology

Laboratories participating in this new network called « ONERBA-Ville » complied with national recommendations regarding antibiotic susceptibility testing (www.sfmmicrobiologie.org), which are very similar to EUCAST recommendations (http://www.eucast.org/ast_of_bacteria), derived from ONERBA's recommendations for surveillance of bacterial resistance. [START_REF] Cornaglia | European recommendations for antimicrobial resistance surveillance[END_REF][START_REF]Epidémiologie de la Résistance Bactérienne aux Antibiotiques (ONERBA). Recommandations méthodologiques pour la surveillance de la résistance aux antibiotiques dans les laboratoires de microbiologie[END_REF] Antibiotic susceptibility test methods were chosen locally and included liquid media automated systems (n= 35 for Vitek-2, BioMérieux; n=4 for BD Phoenix system, BD Biosciences; n=4 for Microscan WalkAway, Siemens Healthcare diagnostics) and the disk diffusion method (n=6). ESBL-production was determined according to national recommendations as described elsewhere. [START_REF] Garrec | Comparison of nine phenotypic methods for detection of Extended-spectrum β-lactamase production by Enterobacteriaceae[END_REF] Isolates were considered susceptible to tested antibiotics by using the following breakpoints: ≤4/2 mg/L for amocicilline/clavulanate, ≤1 mg/L for cefixime, ≤0.5 mg/L for ciprofloxacin, ≤32 mg/L for fosfomycin, ≤64 mg/L for nitrofurantoin, and ≤2/38 mg/L for cotrimoxazole.

Database

Data analysis

Data have been analysed by using STATA 11 (StataCorp, College Station, TX, USA).

Fisher's exact test was used to compare proportions. The Chi2 test for trend has been used to assess the impact of age on the proportion of ESBL-producing isolates. A p-value < 0.05 was considered as statistically significant.

M A N U S C R I P T A C C E P T E D ACCEPTED MANUSCRIPT

Results

E. coli isolated from outpatients in 2013

Data on 51,463 E. coli isolates were collected from urine samples of outpatients during the 3month study period. The median age of the patients was 60 years and 86.4% were females. Among all isolates, 1,694 (3.3%) were ESBL-positive. Patients with ESBL-producing isolates were older (median, 70 years) than those with ESBL-negative isolates (median, 60 years; p<0.001). The proportion of ESBL-producing E. coli was higher in males (4.8%) than in females (3.0%, p<0.001). The proportion of patients harbouring ESBL-producing isolates increased with age (Table 1): from 2.0% among patients under 20 years, to 5.4% among those over 80 years (p<0.001, chi-square test for trend). This significant trend was observed after stratified analysis by gender (Table 1).

As expected, ESBL-producing isolates were significantly less frequently susceptible to antibiotics than ESBL-negative isolates: 22.7% against 67.6% for co-amoxiclav, 47.5% versus 80.8% for cotrimoxazole, 44.0% against 91.0% for ciprofloxacin, 4.0% against 98.0% for cefixime, 93.7% against 98.9% for fosfomycin, 95.4% against 98.9% for nitrofurantoin (Table 2). Overall, 6.0% of the isolates were resistant to at least 3 of the 6 drugs.

E. coli isolated in nursing homes in 2013

A subset of 17 technical centres analysing samples for 237 laboratories provided data on 908 E. coli isolates from patients located in nursing homes during the study period. The median age of patients in nursing homes (88 years) was higher than for outpatients (60 years; p<0.001). The proportion of ESBL-producing isolates was higher in nursing homes in 2013 (12.1%) than in outpatients (3.3%; p<0.001). Of interest, the proportion of ESBL-producing isolates in nursing homes, did not differ significantly according to gender (14.0% in males versus 11.7% in females; p=0.5). The percentage of susceptibility to ciprofloxacin was lower for E. coli isolated in nursing homes than for those from outpatients for isolates taken as a

K. pneumoniae isolated from outpatients in 2013

A subset of 41 technical centres analysing samples for 493 laboratories provided data on 3,495 K. pneumoniae isolates from outpatients. Patients harbouring K. pneumoniae were older than those harbouring E. coli (median, 67 versus 60 years; p<0.001), and were more frequently male (17.8% versus 13.6%; p<0.001). The proportion of ESBL-producing K. pneumoniae was 6.6% as compared to 3.3% for E. coli (p<0.001). As for E. coli, the proportion of ESBL-producing K. pneumoniae was higher among males than females (11.6% versus 5.6%; p<0.001), and increased with age (Table 1). Regarding antibiotic susceptibility (Table 2), K. pneumoniae isolates were significantly less frequently susceptible than E. coli isolates to cefixime (93.2% versus 95.0%), fosfomycin (74.4% versus 98.7%), and nitrofurantoin (71.0% versus 98.8%). On the contrary, K. pneumoniae isolates were significantly more susceptible than E. coli isolates to ciprofloxacin (91.2% versus 89.5%), and cotrimoxazole (88.4% versus 79.6%). Overall, 5.9% of the isolates were resistant to at least 3 of the 5 drugs.

E. coli isolated from outpatients in 2010

A subset of 27 centres analysing samples for 222 laboratories provided data on 15,658 E. coli isolates from outpatients from September to November 2010. The proportion of ESBLproducing isolates was 2.0% in 2010 as compared to 3.3% in 2013 (p<0.001). The proportion of ESBL-producing isolates increased with patients' age in 2010, 1.5% before 60 years old to 2.6% in patients over 60 years (p<0.001). Overall, isolates were significantly more susceptible to cefixime and cotrimoxazole in 2010 (96.5% and 82.9%, respectively) than in 2013 (95.0% and 79.6%, respectively; p<0.001 for both comparisons). Isolates were slightly less susceptible to fosfomycin in 2010 compared to 2013 (97.7% and 98.7%, respectively;

M A N U S C R I P T A C C E P T E D ACCEPTED MANUSCRIPT

Discussion

We conducted a retrospective survey on the proportion of ESBL-producing E. coli and K. pneumoniae isolated from urines of ambulatory or nursing home patients in 2010 and 2013. We showed that the proportion of ESBL-producing isolates was rather high and increased with age, was higher for males as compared to females and increased since 2010.

Nevertheless, the proportions of susceptible isolates remain elevated for most antibiotics used in the treatment of uncomplicated E. coli UTI. The 3.3% proportion of ESBL-producing E. coli in urine samples in France in 2013 is lower than what was reported in numerous European countries such as Spain (7,6%) Italy, United-Kingdom and Germany (all circa 6%) between 2008 and 2011. [START_REF] Aguilar-Duran | Community-onset healthcare-related urinary tract infections: comparison with community and hospital-acquired urinary tract infections[END_REF][START_REF] Horner | Surveillance of antibiotic susceptibility of Enterobacteriaceae isolated from urine samples collected from community patients in a large metropolitan area, 2010-2012[END_REF][START_REF] Noll | Antimicrobial resistance in Germany. Four years of antimicrobial resistance surveillance (ARS)[END_REF][START_REF] Picozzi | Do we really know the prevalence of multi-drug resistant Escherichia coli in the territorial and nosocomial population?[END_REF] On the opposite, a lower proportion (1.7%) of ESBL-producing E. coli was reported from outpatients in Switzerland in 2009-2010. [START_REF] Kronenberg | Active surveillance of antibiotic resistance prevalence in urinary tract and skin infections in the outpatient setting[END_REF] These differences may be explained by variations in populations surveyed, use of systematic urinalysis for UTI diagnosis, or by levels of antibiotic use in the community. [START_REF] Kronenberg | Active surveillance of antibiotic resistance prevalence in urinary tract and skin infections in the outpatient setting[END_REF][START_REF] Adriaenssens | European Surveillance of Antimicrobial Consumption (ESAC): outpatient antibiotic use in Europe (1997-2009)[END_REF] We report a significant increase in the proportion of ESBL-producing E. coli from 2010 to 2013. This is in accordance with previous findings in France showing that the proportion of ESBL-producing E. coli was 0.3% in 1999 and 1.1% in 2006. [START_REF] Arpin | Nationwide survey of extended-spectrum beta-lactamase-producing Enterobacteriaceae in the French community setting[END_REF][START_REF] Arpin | Extended-spectrum beta-lactamase-producing Enterobacteriaceae in community and private health care centers[END_REF] In addition, during the same period of time, there was a 10-fold increase in the prevalence asymptomatic carriers of ESBL-producing E. coli in the community. [START_REF] Gruson | 10-Fold increase (2006-11) in the rate of healthy subjects with extendedspectrum β-lactamase-producing Escherichia coli faecal carriage in a Parisian check-up centre[END_REF] However, these studies have been conducted with different methodologies, and comparisons should be interpreted with caution.

The significant upward trend in ESBL-producing isolates with age as been previously reported. [START_REF] Ben-Ami | A multinational survey of risk factors for infection with extended-spectrum betalactamase-producing Enterobacteriaceae in nonhospitalized patients[END_REF][START_REF] Colodner | Risk factors for the development of extended-spectrum beta-lactamase-producing bacteria in nonhospitalized patients[END_REF] In addition, we confirmed that men have a higher risk of ESBL-positive infections than women. [START_REF] Colodner | Risk factors for the development of extended-spectrum beta-lactamase-producing bacteria in nonhospitalized patients[END_REF][START_REF] Azap | Risk factors for extended-spectrum beta-lactamase positivity in uropathogenic Escherichia coli isolated from community-acquired urinary tract infections[END_REF] These findings underline the importance of age and gender stratification for correct interpretation of resistant data and for comparisons between populations in different settings. It suggests also that guidelines for the treatment of UTI should be adapted to age and gender.

M A N U S C R I P T A C C E P T E D ACCEPTED MANUSCRIPT 10

Antibiotic susceptibility

Despite the rise of ESBL-producing isolates, E. coli and K. pneumoniae isolates remain highly susceptible to fosfomycin, and nitrofurantoin, two drugs for which susceptibility rates were not affected by ESBL production. These data reinforce the 2014 French guidelines for empirical treatment of uncomplicated UTI, which recommend fosfomycin as first line drug and nitrofurantoin as an alternative. [START_REF]Diagnostic et antibiothérapie des infections urinaires bactériennes communautaires de l'adulte[END_REF][START_REF] Huttner | Nitrofurantoin revisited: a systematic review and meta-analysis of controlled trials[END_REF] Desperately, we could not gather data regarding pivmecillinam, which is recommended in the French guidelines. However, a high rate of clinical failure has been reported recently for the treatment of ESBL-producing isolates with this drug. [START_REF] Søraas | High rate of per oral mecillinam treatment failure in community-acquired urinary tract infections caused by ESBL-producing Escherichia coli[END_REF] We report that 95.0% of all E. coli isolates were susceptible to cefixime.

However, this third generation cephalosporin is currently not recommended for the empiric treatment of simple UTI mainly because of its ecological impact. In addition, the activity of cefixime is highly susceptible to the production of ESBL, which is now more frequent.

Limitations

Our study has some limitations. First, we collected routine data on urinary samples without information regarding clinical symptoms and risk factors. This is of importance in the context of UTI in the community where urinalysis for uncomplicated cystitis is not recommended.

Therefore it is likely that urinalysis was partly performed for the most complicated UTI, and the observed proportions of ESBL-producing isolates or of antibiotic resistance are likely to overestimates "true" proportions. However, the observed trend, which is in accordance with other studies, is likely to be real and calls for actions. The fact that we did not collect risk factors of antibiotic resistance limits the interpretation of the results. Second, no specific quality control was organized for the study. However, all French laboratories are now in the process of national accreditation, which makes mandatory internal and external quality controls such as the one annually organised by the French Medical Agency.

Conclusion

M A N U S C R I P T A C C E P T E D ACCEPTED MANUSCRIPT 11

The retrospective study allowed assessing the magnitude of ESBL-producing isolates in the outpatients settings. The observed proportion, which is ten times higher than the one observed 15 years ago is worrisome. Such study with a large network has to be repeated to assess trends over time of antibiotic resistance and the impact of national plans against antibiotic resistance. Co-amox: co-amoxiclav.

All differences between ESBL-positive and ESBL-negative isolates, between female and male patients, and between total E. coli and K. pneumoniae isolates are statistically significant (p<0.001) but for *

M A N U S C R I P T A C C E P T E D ACCEPTED MANUSCRIPT

The production of extended-spectrum beta-lactamase in Enterobacteriaceae has been associated with increased treatment failure and higher management costs.

The prevalence of extended-spectrum beta-lactamase producing Escherichia coli in urinary samples from outpatients has increased significantly in France to reach 3.3%.

The prevalence of extended-spectrum beta-lactamase producing Klebsiella pneumoniae in the outpatient setting is circa twice than for Escherichia coli

The prevalence of extended-spectrum beta-lactamase producing Escherichia coli in nursing homes is circa 4 times higher than in the outpatient setting.

The prevalence of extended-spectrum beta-lactamase producing Escherichia coli in urinary samples increases significantly with patient's age.

3

 3 Our main objective was to assess the prevalence of ESBL-producing E. coli amongst all E. coli isolated from urine samples in the community in ambulatory care in 2013. Data onM A N U S C R I P T A C C E P T E D ACCEPTED MANUSCRIPTKlebsiella pneumoniae the second most frequent Enterobacteriaceae isolated in communityacquired UTIs and data from patients in nursing homes were also collected for comparison purposes.

5

 5 Data were retrospectively collected for each E. coli or K. pneumoniae strain isolated from urines routinely collected for diagnosis of community-onset urinary tract infections in outpatients or those in nursing home during September to November 2013. Data included patient's age, gender, and susceptibility tests results including ESBL production. In case of duplicates, only the first isolate was retained for the study. Whenever possible and for comparison purpose, similar data were collected for 2010.

  .8% versus 89.5%, respectively; p<0.001) or when considering only ESBLproducing isolates (17.4% versus 44.0%, respectively; p<0.001).

  ). The susceptibility to ciprofloxacin and nitrofurantoin was similar in 2010 and 2013.The susceptibility of ESBL-producing isolates to these antibiotics didn't change between 2010 and 2013.

Table 1 .

 1 Proportion of extended-spectrum beta-lactamase producing strains isolated from urines according to age in ambulatory patients in 2013

	Variable			Age group			P
		0-20	21-40	41-60	61-80	> 80	value*
	Escherichia coli
	-Total (n=51463)	2.0	1.9	2.5	3.9	5.4	0.001
	-Female (42839)	2.0	1.9	2.3	3.6	5.1	0.001
	-Male (6733)	2.9	1.7	3.6	5.5	6.8	0.001
	Klebsiella pneumoniae
	-Total (n=3495)	3.4	4.1	4.8	6.5	10.3	0.001
	-Female (n=2753)	2.4	3.8	3.3	4.3	10.7	0.001
	-Male (n=594)	NA	9.1	11.7	13.7	7.6	0.001
	NA: the number of isolates was <30;
	* P-value: chi-square for trend

Table 2 .

 2 Susceptibility (%) to the main antibiotics of strains isolated from urines in

	ambulatory patients in 2013
	Variable	Co-amox Cefixime Ciprofloxacin Fosfomycin Nitrofurantoin Cotrimoxazole
	Escherichia coli (n=51463)
	Total	66.1	95.0	89.5	98.7	98.8	79.6
	Gender
	-Female	66.9	95.4	90.3	98.7	98.9	80.0
	-Male	61.6	92.8	84.4	98.6*	98.1	77.5
	ESBL production
	-ESBL-negative isolates	67.6	98.0	91.0	98.9	98.9	80.8
	-ESBL-positive isolates	22.7	4.0	44.0	93.7	95.4	47.5
	Klebsiella pneumoniae (n=3495)
	-Total	-	93.2	91.2	74.4	71.0	88.4

Funding

The study was funded by a special grant from the Direction Générale de la Santé (DGS), Ministère des Affaires Sociales, de la Santé et des Droits de la Femme.

Competing interest

All authors declare no conflict of interest regarding the results of the study