Nawal Guermouche

Silvano Dal

Towards Timed Requirement Verification for Service Choreographies

Keywords: Timed BPEL processes, choreography analysis, asynchronous services, real-time requirements, formal verification

In this paper, we propose an approach for analyzing and validating a composition of services with respect to real time properties. We consider services defined using an extension of the Business Process Execution Language (BPEL) where timing constraints can be associated to the execution of an activity or define delays between events. The goal is to check whether a choreography of timed services satisfies given complex real time requirements. Our approach is based on a formal interpretation of timed choreographies in the Fiacre verification language that defines a precise model for the behavior of services and their timed interactions. We also rely on a logic-based language for property definition to formalize complex real-time requirements and on specific tooling for model-checking Fiacre specifications.

I. INTRODUCTION

Web Services are a set of standards that enable the definition of complex software systems based on the composition of autonomous and heterogeneous services. Web Services programming relies on a set of XML based standards, such as the Web Service Description Language (WSDL) 1 , for the description of services interface, or the Business Process Execution Language (BPEL) 2 , for defining service orchestration. The notion of choreography (see e.g. [START_REF] Airkin | Web service choreography interface (wsci) 1.0. W3C Working Group[END_REF]) is useful to reason about the collaboration of services from a global viewpoint. Basically, a choreography provides a way to specify the overall behavior expected from the composition of services. Since time plays a crucial role when reasoning about business processes, we need to be able to express the time related attributes of a choreography and we need to be able to check timing requirements on them.

Taking into account temporal (quantitative) aspects in the specification of services improves expressiveness. However, it makes reasoning about service composition much harder and makes known problems more challenging such as timed conformance [START_REF] Eder | Temporal conformance of federated choreographies[END_REF] and timed compatibility problems [START_REF] Guermouche | Timed conversational protocol based approach for web services analysis[END_REF]. While timed conformance and compatibility are important, alone they are not sufficient. In fact, in addition to these features, it is crucial to check time related properties of compositions. For instance, it is useful to check the "worstcase execution time" of a composition [START_REF] Kazhamiakin | Representation, verification, and computation of timed properties in web service compositions[END_REF] or to check that a partial deadline is met. Particularly, in the context of our work, we are interested in checking complex time related properties of a choreography, such as verifying that once an event evt 1 arises, if an event evt 2 does not occur within a delay, then an event evt 3 must not occur before a given delay. To do so, we define a formal model for the semantics of timed choreographies and propose a model-based approach for checking complex real-time requirements, which extends our previous work on compatibility analysis [START_REF] Guermouche | Timed model checking based approach for web services analysis[END_REF]. Complex requirements we consider are defined using a logical-based formalism that is able to express real-time constraints between the occurrence of events; we use a property pattern language that defines a fragment of Metric Interval Temporal Logic (MITL), a real-time extension of Linear Temporal Logic. As a result, our framework can be used to check very general (complex) properties, that go beyond the mere absence of deadlocks or the worst-case execution time. We give some examples of real-time requirements that can be checked automatically in Section III.

More precisely, in this paper, we consider timed services extended with timing constraints. Our goal is to check whether a timed choreography, obtained from the composition of timed services, satisfies given complex requirements. We choose a rich model for expressing timing information where constraints can be associated to the execution time of (basic and structured) activities as well as on the delay between two events. In our context, an event may be local to a given service-for instance an invocation or the end of an activity-or may be global, associated to a message crossing service boundaries.

The formal semantics of timed choreographies is defined using an interpretation of services in Fiacre [START_REF] Berthomieu | Fiacre: an intermediate language for model verification in the topcased environment[END_REF], [START_REF] Berthomieu | The syntax and semantics of fiacre[END_REF], a formal modeling language that can be used to represent the behavioral and timing aspects of a system. The use of Fiacre is well adapted for this context since it captures efficiently timing and concurrency aspects of systems. It has been designed both as the target language of model transformation engines-interpretation have been defined for system description languages such as SDL, UML or AADL-and as the source language for formal verification toolboxes, such as CADP or Tina [START_REF] Berthomieu | The tool tina -construction of abstract state spaces for petri nets and time petri nets[END_REF], the TIme Petri Net Analyzer. In Section V we show how we can use our interpretation of timed BPEL processes in Fiacre and the Tina model-checking tools in order to check complex realtime requirements of timed choreographies.

The paper is organized as follows. In Section II we describe related works in the domain of the formal analysis of Web Services and outline our contributions. In Section III we define an example of timed choreography that is used to give an informal overview of our framework. Section IV presents our formal framework. Before concluding, we report on some experimental results obtained using a prototype implementation of our framework.

II. RELATED WORK

We list a series of works related to the formal analysis of Web Services. In [START_REF] Bultan | Choreography modeling and analysis with collaboration diagrams[END_REF], a Web service (peer) is modeled as non-deterministic communicating finite state machine. In this work, a choreography of services is specified as a collaboration diagram. In order to verify the reliability of a choreography, the authors propose to check if the peers realize the collaboration diagram. In this work, the authors are not interested in timed properties, which are very important. In [START_REF] Hwang | Verifying web services in a choreography environment[END_REF], Hwang et al focus on the problem of verifying the conformance of a set of Web services to a given choreography model. This problem consists in checking whether a set of Web services respects the specified choreography interaction model. As the work presented in [START_REF] Bultan | Choreography modeling and analysis with collaboration diagrams[END_REF], Hwang et al do not cater for timed properties.

In [START_REF] Benatallah | Analysis and management of web service protocols[END_REF], [START_REF] Benatallah | Web service conversation modeling: A cornerstone for e-business automation[END_REF], [START_REF] Bordeaux | When are two web services compatible?[END_REF], the authors address the problem of checking compatibility between two services. Their approach is restricted to synchronous services and is exclusively based on the sequences of messages that can be exchanged by a service. These assumptions are quite restrictive since, for instance, two services may engage in a successful conversation even if their behaviors do not have the same branching structure. On the other hand, compatible services may exhibit very different behaviors when time is taken into account. Compatibility between timed services has been first studied by Benatallah et al. [START_REF] Benatallah | On temporal abstractions of web service protocols[END_REF]. This work has been latter extended in [START_REF] Ponge | Finegrained compatibility and replaceability analysis of timed web service protocols[END_REF]. In these approaches, it is only possible to specify the delay between two messages inside the same service, whereas we consider richer time constraints. Moreover, these works address only one specific requirement-absence of deadlocks-while we allow the verification of more general complex properties.

Eder and Tahamtan introduce the notion of time conformance in [START_REF] Eder | Temporal conformance of federated choreographies[END_REF]. This is defined as the problem of checking whether a timed orchestration satisfies a given timed choreography. In this framework, time constraints are limited to expressing the execution time of basic activities. This approach is different in nature from the one followed in our work. Indeed, our goal is to check properties of choreographies; we do not suppose that a given choreography "is correct" and that parts of its implementation-a timed orchestration-should conform to this specification. We should point out that, in our case, we solve a modelchecking problem for a real-time extension of temporal logic, since we consider timed models, and for a dense time model. Another instance of a "behavior conformance" problem is studied by Ham et al [START_REF] Héam | Component simulation-based substitutivity managing qos and composition issues[END_REF], [START_REF] Héam | How to handle qos aspects in web services substitutivity verification[END_REF] that focuses on the problem of substituting a service by another. These works address both the temporal and financial costs of operations. The authors do not consider time constraints over structured activities or across service boundaries and are not interested in checking complex properties of timed choreographies.

Kazhamiakin et al. [START_REF] Kazhamiakin | Representation, verification, and computation of timed properties in web service compositions[END_REF] adopt a formalism closely related to timed automata to model the behavior of a timed orchestration. This work is based on a discrete-time variant of the Duration Calculus for expressing requirements, while we work with a dense model of time. Furthermore, they consider-other than timeouts-the temporal cost of manual activities and deal with synchronous services, while, in our framework, we propose a richer temporal model. Another difference is that we allow the declaration of more complex and expressive real-time requirements, like those related to the absence pattern, that states that parts of a system's execution are free of some events (e.g., once an event evt 1 arises, if an event evt 2 does not occur within a delay, so an evt 3 must arise after a duration).

In [START_REF] Kallel | Specifying and monitoring temporal properties in web services compositions[END_REF], Kallel et al adopt the formalism of XTUS-Automata to formalize the behaviour of services extended with timed constraints related to relative and absolute time. Based on this model, the authors present a verification process which aims at checking absence of deadlocks. In the same context and using Petri net theory, in [START_REF] Makni | Satisfaction and coherence of deadline constraints in interorganizational workflows[END_REF], the authors address the problem of assigning and verifying conformance constraints of deadlines. Although these approaches consider timed properties, they do not allow checking complex timed requirements.

Our approach extends previous works based on timed automata [START_REF] Guermouche | Asynchronous timed web service-aware choreography analysis[END_REF], [START_REF] Guermouche | Timed model checking based approach for web services analysis[END_REF] that are concerned with the compatibility analysis of timed services. In this work, verification is restricted to checking the absence of deadlock in a composition of services. Moreover, the model can only express temporal constraints on the delays between the exchange of messages and not on the duration of activities. Our Contributions. Our first contribution lies in the definition of a rich model for timed services. This model integrates efficiently the real-time and concurrent characteristics of timed services and is compatible with both synchronous and asynchronous services.

Our second contribution consists in defining new class of real-time requirements that goes far beyond the mere absence of deadlock or the worst-case execution time. In Section III we illustrate the use of this model in the context of a healthcare scenario and show how time constraints and requirements can be expressed. We also explain where this information could be reasonably stored: WSDL and BPEL for local constraints and Service Level Agreement (SLA) contracts for global constraints.

Our final contribution is the definition of a set of transformation rules of timed business processes into Fiacre, a formal verification language with native support for expressing concurrency and time-constrained interactions. By using the result of the transformation, we apply model-checking primitives in order to automatically check complex real time requirements. The proposed approach has been implemented in a tool that takes a collection of annotated BPEL processes and a set of real-time requirements as input, and as a result it validates the set of specified requirements.

III. GLOBAL OVERVIEW OF THE MODELING FRAMEWORK

This work is part of the National Project ITEMIS3 and the European JU Artemisia CESAR4 project.

ITEMIS aims at defining a reference architecture, methodologies, and a set of techniques and tools for the verification and systems development. CESAR aims at providing techniques and methodologies to develop reliable embedded systems. To do so, multi-viewpoint based development processes must be considered to tackle not only functional aspects but also safety, costs, robustness, timed constraints, etc. These properties must be captured and formalized to allow validation and verification to be performed [START_REF] Dal | Cost-efficient methods and processes for safety relevant embedded systems[END_REF]. In our work, we tackle the problem of verifying complex timed properties of service based systems.

Next, we will present the underlying features of our framework with the help of an example of timed choreography. Our modeling framework relies on a syntax for expressing services (based on BPMN); temporal constraints annotations; and a requirement language based on real-time property specification patterns. The verification framework is defined in the next section. We opted for a scenario from the healthcare domain related to patient handling during a medical examination. The scenario involves three entities, each one managed by a service: (1) the medical consultation clinic; (2) a medical analysis laboratory; and (3) a pharmacy.

The choreography is depicted in Fig. 1, where each service is in a different swimlane. With the aid of the medicalConsultationService (MCS), a doctor can check the social security number (ssn) of a patient. If the ssn is valid, then the MCS may ask the medicalAnalysisService (MAS) to perform some medical analyses and, in parallel, asks for a radiography. Once the medical analyses are fulfilled-and after analyzing the different medical data-a medical report is compiled and drugs can be ordered.

Temporal Constraints

The services may interact using asynchronous and synchronous exchange of messages. As usual, the choreography imposes constraints on the order of these messages. It also defines temporal constraints through the use of annotations. We consider two kinds of temporal constraints in our framework, local and global.

Local temporal constraints: are associated to the execution of a service. They are used to specify the duration and/or the delays required to perform an activity. We consider two kinds of local constraints:

(1) temporal costs are used to define the estimated execution time of an activity, say A, and are of the form d(A) ∈ I, where I is a time interval 5 . For instance, the medical report operation in the MCS requires at least 2 hours: d(medicalReport) ∈ [2, ..[. The most suitable place to store these constraints is in the WSDL file that describes the operations;

(2) temporal delays are used to specify the expected delay between two activities and are of the form d(A 1 , A 2 ) ∈ I. For instance, the Pharmacy Service performs the drugsChecking activity between 6-12 hours after the start of the service: d(drugsRequest, drugsChecking) ∈ [START_REF] Benatallah | Analysis and management of web service protocols[END_REF][START_REF] Bozga | Modeling synchronous systems in bip[END_REF]. A temporal delay expresses a commitment from the service, much like a timeout; it is not a requirement that should be checked a posteriori. The most suitable place to store temporal delays is to add annotations in the BPEL file that describes the service.

Global temporal constraints: are used to specify the temporal contract of a service and are associated to pair of messages (dotted lines in our diagram) that cross service boundaries. For example, the Pharmacy Service promises that the drug order is delivered within 24-48 hours of the drug request: d(msg 3 , msg 4 ) ∈ [24; 48]. Global constraints live at the same level than Service Level Agreement contracts.

Given these services, our goal is to verify if their choreography satisfies a set of real-time requirements, such as:

• Once drugs are requested, if the request is not canceled within 6 hours, then they should not be changed for another 48 hours. • Two medical analyses are not allowed for a patient in less than 10 days. • Once the medical examination starts, drugs must be delivered within 48 hours.

In the following section, we will present our framework. In this section, we consider the framework used to define the formal semantics of timed choreographies. Our approach is based on an interpretation of services in Fiacre [START_REF] Berthomieu | Fiacre: an intermediate language for model verification in the topcased environment[END_REF], [START_REF] Berthomieu | The syntax and semantics of fiacre[END_REF], a formal verification language that can model the behavioral and timing aspects of a system. This method has some advantages compared to related work where the semantics of services is given using a dedicated formalism (see e.g. [START_REF] Kazhamiakin | Timed modelling and analysis in web service compositions[END_REF]) or a low-level formalism, like timed automata [START_REF] Guermouche | Asynchronous timed web service-aware choreography analysis[END_REF]. Indeed, Fiacre provides high-level operators, special support for dif-ferent concurrency paradigm and a hierarchical (componentbased) structure that simplify the encoding of system description languages. Moreover, the language comes equipped with a set of dedicated tooling: compilers to different modelchecking tool suite (like CADP or Tina [START_REF] Berthomieu | The tool tina -construction of abstract state spaces for petri nets and time petri nets[END_REF]); support for the real-time requirement language described in the section IV-C; and support for Model-Driven Engineering. In particular, Fiacre is the intermediate language used for model verification in Topcased [START_REF] Berthomieu | Fiacre: an intermediate language for model verification in the topcased environment[END_REF], [START_REF] Farail | the TOPCASED project: a toolkit in open source for critical aeronautic systems design[END_REF]-an Eclipse based toolkit for critical systems (http://www.topcased.org/)-where it is used as the target of model transformation engines from various languages, such as SDL, UML or AADL.

A. The Fiacre Language

Fiacre offers a formal representation of both behavioral and timing aspects of systems for formal verification and simulation purposes. The design of the language is inspired from decades of research on concurrency theory and realtime systems theory. For instance, its timing primitives are borrowed from Time Petri nets [START_REF] Merlin | Recoverability of communication protocols: Implications of a theoretical study[END_REF], while the integration of time constraints and priorities into the language can be traced to the BIP framework [START_REF] Bozga | Modeling synchronous systems in bip[END_REF]. Fiacre processes can interact both through synchronization (message-passing) and access to shared variables (shared-memory). A formal definition of the language is given in [START_REF] Berthomieu | The syntax and semantics of fiacre[END_REF].

Fiacre programs are stratified in two main notions: processes, which are well-suited for modeling structured activities, and components, which describes a system as a composition of processes, possibly in a hierarchical manner. The language is strongly typed, meaning that type annotations are exploited in order to guarantee the absence of unchecked run-time errors.

A process is defined by a set of control states (say s 0 , s 1 , . . . ) and parameters, each associated with a set of complex transitions, which are programs specifying how parameters are updated and which transitions may fire. For example, the process declaration:

process P[q : none](&v : nat) is ... expresses that P is a process that uses the port q for synchronization-the port carries no data-and has one parameter, v, that is a (reference to a) shared variable holding natural values. Complex transitions are built from expressions and deterministic constructs available in typical programming languages (assignments, conditionals, while loops and sequential compositions), nondeterministic constructs (nondeterministic choice and assignments) and communication events on ports. For example, the transition:

from s 0 s e l e c t v :=v + 1 ; t o s 1 [ ] on ( v = 0 ) ; t o s 0 end
states that, in state s 0 , the process may choose nondeterministically between two alternatives. Either increments the value of the variable v and moves to s 1 , or loops to s 0 if v is nil.

A component is defined as the parallel composition of processes and/or other components, expressed with the operator par ... || ... end. While components are the unit of composition, they are also the unit for process instantiation and for ports and shared variables creation. The syntax of components allows to restrict the access mode and visibility of shared variables and ports, to associate timing constraints with communications and to define priority between communication events. For example, the following declaration states that C is a component with a private port r-synchronization over r is in time 0-and two fresh instances of the process P.

component C ( x : n a t ) i s p o r t r : none i n [0, 0] var v 1 : n a t :=x , v 2 : n a t :=3 par P [ r ] ( v 1 ) | | P [ r ] ( v 2 ) end

B. Interpretation of BPEL in Fiacre

In order to perform verification process, we define an interpretation of timed BPEL processes where a service is modeled by a Fiacre component and such that service invocation (both synchronous and asynchronous) is modeled using shared variables. In this approach, the interpretation of a choreography is obtained from the parallel composition of its services. We only detail the encoding of a representative subset of activities. Moreover, we note that our approach does not take into account the expected behaviour in case of faults or communication failures, which is out of scope for this paper.

Interpretation of communication.: We model communication using a shared variable that acts as a buffer counting the number of messages exchanged between services; each WSDL message, say msg i , is represented by an integer variable, msgVar i , with initial value 0. Then (an asynchronous) message emission is encoded by incrementing the variable and reception by decrementing it. For example, reception of the message msg is encoded by the Fiacre expression: on(msgVar>0); msgVar:=msgVar-1 (we use the on expression to test that the "message channel" is not empty). This approach can be extended to take into account the values exchanged in a message, as long as the number of values stay finite.

Interpretation of parallel activities as processes.: A service S is encoded by a component S. We encode each parallel activity A i in S by a Fiacre process A i with two specific ports: ps for signaling the start of the activity and pe for signaling its end. A <flow> activity in BPEL is used to execute sub-activities, A 1 , . . . , A n , in parallel. In our encoding, a flow activity inside the service S is turned into a parallel composition A 1 (ps,pe) || ... || A n (ps,pe), such that instances of the A i 's are synchronized on their start and end event. Hereafter, we define the processes corresponding respectively to the basic activities <receive>, <reply> and <invoke> Interpretation of sequential basic activities.: Basic activities that are not executed in parallel are mapped to a state in a single Fiacre process, say P. The goal is to obtain a more efficient encoding (with less processes and states). In this context, an activity A i is mapped to a state s i in P and its effect is implemented by a transition from the state s i to the state s j such that A j is the next in line from A i in the sequence. Interpretation of temporal constraints.: We start by describing the interpretation of temporal cost. An activity that can be executed within a delay is modeled as a transition that takes place after a timed interval. We consider two categories of activity that can have a temporal cost: one-way operation and request-response operation. In this context, we map an operation A i to a pair of states s i and s i . The effect of A i is implemented by a sequence of two transitions from the state s i to the state s j , where A j is the activity that logically follows A i . We give below the encoding of one-way and request-response <invoke> operations with an execution time of d.

(one-way) from si on ( msgVar>0); w a i t [0, 0] ; msgVar:=msgVar-1;

t o s i from s i w a i t [d, d] ; t o sj (request-response) from si on ( msgVar>0); w a i t [0, 0] ; msgVar:=msgVar-1; t o s i from s i w a i t [d, d] ; msgVar:=msgVar + 1 ; t o sj
The interpretation of temporal delays and global constraints are similar. We associate to every delay constraint of the form d(A 1 , A 2 ) ∈ I a process in Fiacre, say TObs. The role of this process is to observe the delay between the end of A 1 (synchronization on the port pe 1 ) and the start of A 2 (synchronization on ps 2 ). The encoding is very similar for a delay between messages. We give below the "time observer" process corresponding to a constraint of the form d(A 1 , A 2 ) ∈ [0; d] (the unless operator is used to state that the transition to err has an higher priority). We can test if the constraint is violated by checking whether the process TObs can reach the state err. We describe our interpretation of a timer-based alarm, <onAlarm for ="d">, using the example of a simple <pick> activity A i such that:

A i = <pick><onMessage name="m"/>
<onAlarm for="d">A k </onAlarm> </pick> meaning that the activity will select the activity A k after d unit of time unless it receives the message m before. The activity A i may be encoded using the following transition: from si s e l e c t w a i t [0, 0] ; on ( msgVar>0); msgVar:=msgVar-1; t o sj u n l e s s w a i t [d, d] ; t o s k end Example 1: (Interpretation of Pharmacy Service)

We take the example of the healthcare scenario introduced in section III to show our interpretation. The architecture of the Fiacre component corresponding to the Pharmacy Service is displayed in Fig. 2.

The Pharmacy Service (PS) has three temporal constraints: (c 1 ) the activity drugsChecking must be done within 6-12 hours of receiving the drugs request (a local, delay constraint); (c 2 ) the execution time of activity preparing-Shipping is 6 hours (a local, temporal constraint); and (c 3 ) the message sent by activity sendDrugsOrder should be emitted within 24-48 hours from receiving the drugs request (this is a global constraint). The PS is built from a <sequence> activity that contains two operations that should be performed in parallel (inside a <flow> activity): preparingShipping and invoicing. Therefore, in our (optimized) interpretation, the component PS contains the parallel composition of three processesone for the sequence and one for each activity inside the <flow>-added to a "time observer" process for the two constraints c 1 and c 3 . These four processes appear in the diagram of Fig. 2 with an explicit naming convention.

PS FIACRE component

We can describe the possible interactions of the PS component as follows. First, the deliverySequence process starts by receiving a drugs request. This message is labelled msg 3 in the diagram of Fig. 1 and is modeled using a shared variable msgVar 3 that is a parameter of PS. This event eventually triggers a transition in the process deliverySequence that corresponds to the end of the activity drugsRequest and also prompts the time observer process (via synchronization on port p 1 ) to start monitoring the elapsed time. The next state in line corresponds to the start of the drugsChecking activity that must be fulfilled within 6-12 unit of times unless the time observer enter its error state err (synchronization with the temporal observer on port p 2 ). At this point, the deliverySequence synchronizes on the "start" port of the <flow> process (port p 3 in Fig. 2). After the completion of the <flow> process (synchronization on port p 4 ) the deliverySequence gains hand again and the computation moves to the fulfillment of the reply activity sendDrugsOrder. Before concluding, the process interact again with the time observer (synchronization on port p 5 ) if the delay for sending the message msg 4 comply with the global constraint (c 3 ).

After presenting the BPEL transformation process to Fiacre language, let us present the real-time requirements we handle.

C. Defining real-Time Requirements

This section gives a description of the specification patterns used for the definition of real-time requirements available in our framework. A complete description of the language is given in [START_REF] Abid | Real-time specification patterns and tools[END_REF]. Our language extends the property specification patterns of Dwyer et al. [START_REF] Dwyer | Patterns in property specifications for finite-state verification[END_REF] with the ability to express time delays between the occurrences of events. The result is expressive enough to define a wide class of complex properties [START_REF] Abid | Real-time specification patterns and tools[END_REF], [START_REF] Abid | A verified approach for checking real-time specification patterns[END_REF]. The pattern language follows the classification introduced in [START_REF] Dwyer | Patterns in property specifications for finite-state verification[END_REF], with patterns arranged in categories such as occurrence or order patterns. In the following, we study examples of response and absence patterns.

Absence pattern with delay.: This category of patterns can be used to specify delays within which activities must not occur. A typical pattern in this category can be used to assert that an activity, say A 2 , cannot occur between d 1 -d 2 units of time after the occurrence of an activity A 1 . This requirement corresponds to a basic absence pattern in our language: Response pattern with delay.: This category of patterns can be used to express delays between events, like for example constraints on the execution time of a service. The typical example of response pattern states that every occurrence of an event, say e 1 , must be followed by an occurrence of an event e 2 within a time interval I. This pattern is denoted: e 1 leadsto e 2 within I .

absent A 2 after A 1 within [d 1 ; d 2 ] . (absent
(leadsto)

In our framework, we use the notation S.init and S.end to refer to a start, respectively an end, event in the service S.

V. EXPERIMENTATION

We have developed a prototype of a compiler from annotated BPEL processes to Fiacre in Java, named Bpel2Fcr, that is based on the interpretation defined in the previous section. The architecture of our transformation is depicted in Fig. 3. The input of our prototype is a set of BPEL processes, their corresponding WSDL and Service Level Agreement contracts that list the local and global constraints of the timed choreography. Our tool relies on EasyBPEL (http://easybpel.petalslink.org/), a library that provides a BPEL 2.0 engine to orchestrate services.

The Fiacre specification obtained as an output of Bpel2Fcr is the input of the model checker provided by the Tina verification toolbox to analyze specified choreography realtime requirements.

We give some results obtained with the analysis of our running example. The state graph for the HealthCare example has only 43 states and 51 transitions. This is obtained using optimized encoding (the graph for the unoptimized encoding is about three times as big). The generation of the Fiacre specification and its corresponding state space takes less than a second. For examples of this size, the verification time for checking a requirement is negligible; in the order of a couple of milliseconds.

This model is small due to the almost lack of concurrency in the scenario; only two <flow> activities and three services. For more complex examples, we have tested our approach on an extended version of the healthcare scenario with seven different services. The resulting example has 886 states and 2476 transitions. With this larger example of timed choreography, the verification process takes in the order of half a second. As an example, we give the time and the validity of some real-time properties: We describe a new framework for modeling and analyzing timed choreographies obtained through the composition of annotated BPEL processes. We most particularly focus on the problem of checking real-time requirements on a choreography. In this context, we have proposed a rich formal model for timed services composition that captures efficiently several kind of temporal constraints associated to the concurrent nature of services. The framework we propose has been implemented into a tool that automatically transforms timed BPEL processes into a Fiacre specification. In addition, we have shown an associated model-based verification approach to check real-time requirements on timed choreographies. In this context, we have defined classes of new real-time requirements which are specified using a logical-based formalism.

Property
Work is still ongoing to improve and optimize the transformation implemented in our verification toolchain. Moreover, our ongoing work focuses on extending our approach by fault handling primitives and checking more complex requirements that relate to automatic reconfiguration of service composition. We should be assisted in that by the fact that our transformations are compositional.

5

  Time intervals may be open, like ]2.5, 3], or unbounded, like [1, ..[.

Figure 1 .

 1 Figure 1. Global view of the health-care application

Figure 2 .

 2 Figure 2. Architecture of the Fiacre process for the Pharmacy Service

  Rpl [ ps : none , pe : none ](&msgVar : n a t ) i s s t a t e s start , s1 , s2 , s3 i n i t t o start from start ps ; t o s1 from s1 w a i t [0, 0] ; msgVar:=msgVar + 1 ; t o s2 from s2 pe ; t o s3

	p r o c e s s Invk [ ps : none , pe : none ](&msgOutVar ,
	&msgInVar : n a t ) i s
	s t a t e s start , s1 , s2 , s3 , s4 i n i t t o start
	from start ps ; t o s1
	from s1 w a i t [0, 0] ; msgOutVar:=msgOutVar + 1 ; t o s2
	from s2 on ( msgInVar>0); w a i t [0, 0] ;
	msgInVar:=msgInVar-1; t o s3
	from s3 pe ; t o s4

p r o c e s s Rcv [ ps : none , pe : none ] (&msgVar : n a t ) i s s t a t e s start , s1 , s2 , s3 i n i t t o start from start ps ; t o s1 from s1 on ( msgVar>0); w a i t [0, 0] ; msgVar:=msgVar-1; t o s2 from s2 pe ; t o s3 p r o c e s s

  Hence, we can check that the execution time of the service S is less than d units of time with the requirement S.init leadsto S.end within [0; d]. We can use the same pattern to express requirements on an activity. For instance that drugs must be delivered within 48 hours of the medical examination start: For instance, in our motivating example, we would like to check that the medical examination last less than 60 hours:M CS.init leadsto M CS.end within [0, 60] ∧ M CS.init leadsto M AS.end within [0, 60] ∧ M CS.init leadsto P S.end within [0, 60] .More generally, we can check that a service, say S 2 , always terminates its execution after service S 1 within a duration d with the requirement: S 1 .end leadsto S 2 .end within [0; d]

M CS.init leadsto P S.sendDrugsOrder within [0; 48] .

Using a composition of patterns with the conjunction operator, we can bound the time between the start of the initiating service (the client) and the end of the choreography (if any).

http://www.w3.org/TR/WSDL/

http://docs.oasis-open.org/wsbpel/2.0/wsbpel-v2.0.html

ITEMIS: Integrated information and embedded systems. It is an ANR (National Research Agency) project (2009-2012).

CESAR: Cost-efficient methods and processes for safety relevant embedded systems. It is a European funded project from ARTEMIS JOINT UNDERTAKING (JU) (2009-2012).


Marie-Claire Robic
email: robicmc@parisgeo.cnrs.fr

Elisée Reclus visited and revisited

This paper has been prepared in 2006 for an Axel Baudouin's Homage in Trondheim (Norwegian University of Science and Technology). Due to the international revival in Elisée Reclus'studies, which was already stated in this article, most references have not been updated, only a few of them (specially those issued from the conferences held in 2005). One of the recent seminar on Elisée Reclus in France is : « Élisée Reclus, l'Orient et l'Occident à l'âge des empires », Journée d'étude, Paris, 30 mai 2012 (École des Hautes Études en Sciences Sociales -GGH-TERRES -Groupe de géographie et d'histoire des territoires, de l'environnement, des ressources et des sociétés et UMR 8504 Géographie cités, équipe EHGO -Épistémologie et histoire de la géographie), org. : Federico Ferretti. See raforum./info/reclus Elisée Reclus has received particular attention in France on the occasion of the hundredth anniversary of his death. Two university congresses devoted to him were held, one in Montpellier (4-6 th July 2005), and the other in Lyon (7-9 th September 2005). The first proposed the theme "The Geographer, the City and the World: yesterday and today. Around 1905: Elisée Reclus, Vidal de la Blache", while the second offered "Elisée Reclus and our geographies: texts and pretexts". Beyond the mere commemoration, the number and the variety of participants, the presence of historians of anarchy alongside geographers, the international outreach of the conferences, and indeed the passionate turn of debate, all show that Reclus has become a major public figure in France when approaching present-day geography. The interest roused by Reclus among French geographers is however neither recent nor serene. It can be said that he has never ceased to be a reference, for some, since the 1970s. But he has been a reference that, far from signalling a community of viewpoint, highlights internal rivalries, at a time when the discipline is being reassessed. Thus, after a period of oblivion linked to a certain hegemony of the French school of geography, massed behind its "founder" Paul Vidal de la Blache, the anarchist geographer Elisée Reclus became the standard-bearer of competing groups, the common denominator of which was a rejection of the inherited geographical tradition: the "classical" or even "traditional" geography attributed to Vidal. Thirty years after this break with tradition, and the development of various innovating trends, how can this new curiosity, or even enthusiasm, about Reclus at the start of the 21 st century be interpreted? What is the meaning of the association, if there is one, with the other tutelary figure, Vidal de la Blache? It is by way of the analysis of the reception given to Reclus today, and then by repositioning him in his time, that we will endeavour to add to the visits and re-visits of which he has been the object. We will attempt to contextualise, to study the reception given him through time, and to obtain a clear in-depth image of his relative position in relation to the three emerging geographical issues of that period (nature, the city, and the finite world), so as to conduct a form of "follow-up" visit (to retain the metaphor) in historical perspective, in the light of the institutionalisation of geography at the beginning of the 20 th century

Contemporary reception

Geographical hero or Romantic geographer?

Richard Lafaille, writing in 1989, underlined that the geography of Reclus, "buried then exhumed, propelled to the forefront by some, categorised as outdated by others [...] now enjoys an enthusiasm that is as suspect today as was its rejection earlier" (p.443). This moment of recognition in the 1970s and 1980s was sustained by radical readings that "made politics the key to the interpretation of his work" (p.443). According to Lafaille, who reviewed some fifteen geographical authors who had studied Reclus between 1969 and 1986 (when a special issue of the Revue belge de géographie was published), these interpretations of "reclusian" geography as being "revolutionary geopolitics" are an oversimplification. They arise from a dual historiographic filter (the preconceptions of readers, and the fascination for the man himself, a sort of "Romantic hero [who] epitomises the heroic geographer" (p.447)), operating at the expense of the analysis of the texts themselves. This reading of Reclus, according to Lafaille, is selective and partisan: it overlooks the literary dimension of his work (which was criticised at a time when geography was being promoted as a positivist science) while this is where his Romantic dimension finds its expression. He thus underlines the strictly literary importance of reclusian geography, which "comes out as landscape poetry [...] which includes scientific and didactic preoccupations and numerous themes cherished by the Romantics" (p.458).

Non-conformism, progressivism

The political interpretation of Reclus in the early 1970s in France reflected a political radicalisation under the impulse of the May 1968 events, which shook the universities. The commemoration of the Paris Commune gave the libertarian movement considerable news coverage. These events shed light on the way in which Reclus was "appropriated" by the journal Hérodote, established in 1976 and directed by Yves Lacoste in the experimental university of Vincennes. After the spread of the libertarian theme "Elisée Reclus, geography, anarchism" for which [START_REF] Béatrice | Elisée Reclus, géographie, anarchisme[END_REF] was responsible at the time, very soon the ecological theme was added, a theme that was emerging in the public field. Here again it was diffused by B. Giblin (and Gary Dunbar"s Elisée Reclus, Historian of Nature, 1978). But the discovery in France of the "new geography" of the English-speaking world in the early 1970s, the diffusion of the polymorphous French "nouvelle géographie", and the questioning of the old French school of geography associated with the name of Vidal de la Blache, all gave other innovators the occasion to use the name of Elisée Reclus as a banner. Thus for instance from 1981 around Roger Brunet, who succeeded in grouping a number of the advocates of the renovation of geography in a spatial perspective, an official scientific organisation developed, the GIP Reclus. This denomination (in fact representing the Réseau d'Etude du Changement des Localisations et des Unités Spatiales) providing the acronym Reclus was intentionally indexed on the figure of a non-conformist and politically progressivist geographer: a "pilgrim for humanity", as he was presented in the new Universal Geography published from 1990.

Homage, revision, trivialisation and the time for stocktaking

The contemporary reception given to Reclus has initiated a more composite movement. Passions are still presentpeople fly to the defence of Reclus, or object to the attenuation of his heroic image; and others knowingly remove him from the pedestal, in particular by stigmatising his views on ethnic or colonial issues, a particularly sensitive question today. It should however be underlined that these encounters around Reclus have contributed several new dimensions.

Firstly these conferences convene geographers, militant anarchists and historians of anarchism. This interaction has enabled the first to gain a better understanding of the complicity between the geographical analyses conducted by Reclus and certain anarchist themes. For instance [START_REF] Florence | La France d"Elisée Reclus, une géographie libertaire de la nation[END_REF] interprets Reclus" France as a libertarian geography of the nation, in the light of the analysis of Proudhon and Deleuze writings that Daniel [START_REF] Daniel | Petit lexique philosophique de l'anarchisme, de Proudhon à Deleuze, Paris, Le Livre de poche[END_REF] provided in Petit lexique philosophique de l'anarchisme. Geographers should also put the position of Reclus within the anarchist movement into perspective. The analyses [START_REF] Gaëtano | Elisée Reclus entre l"insurrectionnalisme et l"éducationnalisme réalisateur[END_REF]/2009) offers of the positions adopted by Reclus towards the social movement, and of his personal itinerary (in which the Commune episode and exile play a major part) are particularly compelling; they give him a real consistency within the three ideal-typical attitudes of the anarchists: insurrectionism, unionism, educationism. This interaction should also enable the second group to introduce into their analyses the spatial and territorial perspectives used by Reclus to conceive collective organisation and outcomes.

Secondly, these new readings of the writings of Reclus have constituted an opportunity for critical review, in particular on the theme of his objectivity, or his sensitivity to "otherness". Alongside many colourless works on "Elisée Reclus in such and such a country", certain authors have speculated on the way in which he dealt with a given ethnic or religious community. These are frequently polemic readings, basically for the purpose of re-evaluation and tarnishingof his image, by showing him bogged down in the stereotypes of his day, in particular colonialism and orientalism. Other authors examine how he represented the colonial encounter [START_REF] Axel | Reclus, colonialiste ?[END_REF][START_REF] Giblin | Elisée Reclus et les colonisations[END_REF][START_REF] Florence | Elisée Reclus et la colonisation de l"Afrique du Nord occidentale[END_REF]) and debate on the "ambiguous" positions adopted by Reclus on colonisation. But, as Florence Deprest puts it, these must be contextualised and compared to the whole range of political postures of the time, when anticolonialism (expressed in particular in relation to military conquest by a state) was rare.

Thirdly, several analyses have tried to revise the historiographic vulgate, and in particular the figure of him as the outlaw, "the outcast, rejected both by political powers and by university institutions" (Lafaille, 1989, p.444) created by B. Giblin and Y. Lacoste in particular. Here there have often been genuine explorations to determine what audience Reclus really had, and to study what this geographer"s relationship was with university teaching. Thus, countercurrent to the theme of "rejection" that, according to some, Reclus underwent at the hands of the French school of geography, Jean-Baptiste Arrault (2005) explores the "Reclus reference" in and around the Annales de Géographie from 1890 to 1920, to conclude that in fact "the outcast was integrated early on into the history of geography, and given a specific place (the only great geographer before Vidal?) by the "vidalians" among whom no homogenous group can be identified". Maria Teresa Vicente Mosquette (2005) and Henri Nicolai (2005) analyse his place as university professor in Brussels. For Nicolaï, "the last avatar of Elisée Reclus" in Belgium was not a late achievement in a turbulent career, but rather a form of instrumentalisation within a conflict inside the Free University of Brussels, amounting, in all, to a solely political consecration: "in the events that shook the Brussels university institution, it is the political symbol that Reclus represented that was essential, and not the geographer or his geography". Likewise, Axel [START_REF] Axel | Entre attirance et refus. Elisée Reclus et l"université[END_REF] shows the ambiguous relationship "between attraction and rejection" that Reclus entertained with the university, as with any institution.

Geographer, writer, anarchist -a literary "worker" in the Maison Hachette

These deeper analyses, based on archive studies or contextual research, have revised the rosecoloured vulgate (the progressivist hero rejected by the conservative or reactionary institution), or the darker counter-legend (a man who, in fine, was a conformist, or at any rate less "politically incorrect" than has been claimed) in relation to particular issues. However, a study aiming to retrieve the meaning of a work by integrating it at once into a personal trajectory and into the material configurations that shaped it historically, is on a quite different scale. The various studies conducted by Soizic Alavoine adopt this global dimension that aims, in this instance, to characterise a deliberate purpose to educate humanity in its scope for emancipation through geography. Within this educational and political (in the strong sense) perspective is found the Grand Globe project on the 1/100 000 scale that Reclus designed for the Universal Exhibition of 1900 [START_REF] Soizic | Un globe terrestre pour l"Exposition universelle de 1900. L"utopie géographique d"Elisée Reclus[END_REF][START_REF] Jean-Marc | Institutionalization of geography and strategies of change[END_REF]. The writings of Reclus also entertain this concern, but within various constraints, in particular those of the popular press in the 19 th century. As S. Alavoine puts it, Reclus was a "literary (employed) worker" for the Maison Hachette (the publisher) (Alavoine-Muller, 2005), in a long-term state of financial dependency, as were many authors in the 19 th century studied by Pierre Bourdieu in his book Les Règles de l'Art. Reclus had to submit to editorial demand from the powerful publisher. The commission restricted him first of all to an agenda of picturesque popularisation, while Reclus would have preferred, more than anything, to engage in scientific geography. "To please, to captivate, to move, in order to be read and to instruct" was the brief for the drafting of the Nouvelle Géographie Universelle, at the expense of "didactism" which the owner of Hachette outlawed (in the name of the market), when he saw the first drafts from Reclus in 1872 [START_REF] Soizic | La Nouvelle Géographie Universelle, Elisée Reclus face aux contraintes éditoriales de la maison Hachette[END_REF]Lafaille, 1989, p.451-452). His commission also involved political censuring: no "propaganda", no militancy, specified the editor, or in the words of Elisée"s brother Onésime Reclus: "Your descriptive geography must never be politico-religiosociologico-militant!" (Alavoine-Muller, 2005/2009). There was censure, therefore, and selfcensure by Reclus in his universal geography, involving a degree of ethical rectitude with respect to the contract to which he had agreed, without renouncing his strongest convictions.

Elisée Reclus and the era of geography and geographers

2.1.Three processes contributing to the triumph of geography

Because they concentrate on the 1870 turning-pointwhich opened up an era of promotion of school geography designed to erase the humiliation of France"s heavy defeat in the Franco-Prussian warhistories of French geography have tended to over-emphasise the ideological and nationalistic dimension alone. The Third Republic, in some ways, also prolonged the modernising policy of the Second Empire, by diffusing geographical teaching with a utilitarian slant, aiming to provide knowledge of the contemporary world in order to facilitate military conquests and trading activities. It also associated all teaching disciplines with the common task of national reconciliation, following the terrible political threat seen in the Paris Commune. Nationalism, political integration to offset the class struggle, colonialism, popular education: the institutionalisation of the geographical discipline in schools, and following that in universities, was a fundamental trend which has been shown (in particular by Horacio Capel, 1982) to be everywhere correlated with the spread of secondary education.

Beyond this basic trend, there was also widespread polymorphous enthusiasm for knowledge of the world and nature that also included geography, from the start of the 19 th century (Robic, 2003a). The taste for travel, the attraction of the exotic, the success of the universal exhibitions, the spread of tourism, excursionism, and Alpinism, the beginnings of landscape conservationism, all give ample evidence of this trend. Today the historians of the 19 th century, previously reluctant to enter into cultural history, give a much fuller picture of this, as is the case for Alain Corbin for instance.

Finally, there was an awareness that the world was being progressively circumscribed by way of its gradual conquest by the Europeans and the shortening of distances obtained through new communication technologies, and this awareness fed a new geographical imagination. As early as the 1830-40s, the French Saint Simon school became the proponents of this trend Bretagnolle, Robic, 2005a). A collective imagination in relation to the removal of distance, the disappearance of blank zones on maps, and universal means of communication was propagated in the wake of transport revolutions, to finally reach, at the start of the 20 th century, the conclusion of a "finite world", in the views of Reclus, Frederick J. Turner (the end of the Frontier) or Mackinder (the "globe-wide world") (Bretagnolle, Robic, 2005b;[START_REF] Béatrice | Closed space and political practice: Frederik Jackson Turner and Halford Mackinder[END_REF].

Several generations of "geophiles" in France

At the start of the 20 th century, the French school of geography assembled around Paul Vidal de la Blache in an university setting was beginning to obtain renown in the intellectual field, both in France and abroad. Thus, at this time, four generations co-existed: pioneers of popularisation and three generations of teaching geographers. Several pioneers in geography were reaching the end of their life. Elisée Reclus (1830Reclus ( -1905)), then professor in the New University in Brussels, was completing his main work L'Homme et la Terre. Among his contemporaries taking an interest in geography two other people spring to mind: the writer Jules Verne (1828-1905) who published his Voyages extraordinaires in the 1890s, and in particular the Tour du monde en 80 jours; and the geographer, historian and statistician Emile Levasseur (1823Levasseur ( -1911)), who wrote the school curricula for geography between 1871 and 1872 and developed a new field he called « economic geography ». All three belong to a generation of intellectuals who were still mainly unspecialised and who were strongly implicated in scientific popularisation. They were contemporaries of the first universal exhibitions. Three other generations of geographers follow on. They were teaching geographers and followed the academic type of career generated by the promotion of the university under the Third Republic. A first subgroup is comprised of initiators such as Paul Vidal de la Blache (1845-1918) who entered the university at a time (1872) when geography teaching was considered to be a national issue. In this nationalistic and world competition setting, Vidal de la Blache had a correspondent in Germany, Friedrich Ratzel (1844-1904), and, in Britain, Halford John Mackinder (1861-1947). Vidal de la Blache progressively developed the tools of a geographical science, half way between esoteric science and communicable knowledge. Two following generations of university scholars were composed of Vidal de la Blache"s pupils, who learnt geography during their educational curriculum in the Ecole Normale Supérieure. But the first scholars (like Lucien Gallois, 1857-1941and Marcel Dubois, 1856-1916) had to devote their theses to history or historical geography whether the youngest choose modern field geography, as did Jean Brunhes (1869-1930), Camille Vallaux (1870-1945), Albert Demangeon (1872-1940), Emmanuel de Martonne (1873Martonne ( -1955) ) and others. This is the1870s generation, born at the time of the Franco-Prussian war and the Commune. They knew only the republican regime and its positivist university. Vidal de la Blache appeared to them as the main reformer of French geography. They considered Elisée Reclus, who died just at the time when they defended their doctoral dissertation, as a great geographer, but who had been overtaken by the progress of geographical science.

Reclus as seen by his contemporaries: "the" great French geographer in the face of the German challenge, but over-descriptive

It thus clearly appears that establishing a parallel between the itineraries and the scientific and political positionings of Reclus and Vidal de la Blache, as has frequently been the case, is not relevant. Despite their small difference in age (eighteen years), they did not belong to the same institutional world. The difference is complete if we consider the hiatus between Reclus and the "disciples" of Vidal de la Blache who made up the French school of geography. It is nevertheless interesting to explore the reception given to Reclus from the 1870s, when he was writing his Nouvelle Géographie Universelle, alongside contemporary efforts to institutionalise scientific geography, supported by the governing bodies of the university, as well as a professionalisation of scientific disciplines generally.

It would seem that, far from being ignored, his publications were received with a degree of enthusiasm in intellectual journals, including geographical journals, or those devoted to teaching and education. Ludovic Drapeyron, the founder of the Revue de Géographie created in 1877, claimed that he had been "touched by the grace" of geography when he read La Terre in 1870. Indeed Reclus was awarded the gold medal of the Société de géographie de Paris in 1892. Critics were nevertheless also present. Criticism predominantly concerned lack of style, or more strictly lack of scientific style. This is what motivated a critique by M.H. Gaidoz in the Revue Politique et Littéraire in 1875 in which, while he gave Reclus considerable praise for his feeling for nature, for his profound knowledge of the physical world, and for choosing to explore the Earth and the men living on it, he considers that the place given by Reclus to statistical erudition was too small, and that the "literary bent" of the author was at the expense of the necessary inclusion of a display of notes and bibliography. The same is true of a critique by Jean-Baptiste Pasquier, one of the protagonists of the educational reform, who gives an overview of the progress accomplished by geography in the Revue Pédagogique. He found the ninth volume of the Géographie Universelle (25000 copies issued) well written, easy to read, and well-served by its literary style, but excessively descriptive, and possessing faults in its design.

It does seem that in either case the issue is the critical encounter between the scientific requirements imposed by the positivist ideology favoured by the Third Republic, and the commercial censure of the editor requiring Reclus to adopt a descriptive style that was readily popular. Political criticism, on the other hand, as Lafaille has also shown, is absent from these critiques. The same explanation fits, since editorial censorship also comprised a requirement of political correctness. But it can be added that the reception given to the works of Elisée Reclus was also a response linked to the widespread complex entertained in France that saw the "German challenge" as a challenge to be met. And indeed who, other than Reclus, was in the position to personify, in geography, the figure of the French intellectual? This is probably the reason for the enthusiasm he inspired. Thus, for instance, in 1874, we find the following lines in the Revue des Deux Mondes (with which Reclus had disagreed on a feminist issue) written by Ernest Desjardins, professor of geography in the Ecole Normale Supérieure: "Who else in Europe, since Humboldt and Karl Ritter, has approached the physical geography of the globe with more skill, or studied it with more passion? [...] Whatever may be his egalitarian and socialist ideas, Mr. Elisée Reclus has more merit as a geographer than merely that of having written a good book: he has made disciples, and, what is extremely rare, he has made disciples within his own house [...]" (p. 178-179). Paquier also cites the names of the two German geographers with the intention of placing Reclus on a par with them. Conversely, Marcel [START_REF] Dubois | L"avenir de l"enseignement géographique[END_REF], who was then a young university intellectual engaged in introducing geography in the University, with Sorbonne personalities such as Ernest Lavisse, barely mentions Reclus in his analyses of the evolution of geography. He more readily mentions the academic trend to which the Sorbonne professor in historical geography whom he was assisting (Louis-Auguste Himly) belonged, and that of Vidal de la Blache in the Ecole Normale. He sets a parallel between Himly and Ritter (he and Reclus had both been auditors), and shows the merits of Vidal de la Blache in forming a new school of geography. If Dubois is one of the people to give Reclus some credit among authors published in and around the Annales de géographie, as has been demonstrated by J.-B.Arrault, this attitude is subsequent to the emergence of the "Vidalian" school, and the clash that finally led Dubois to break away from that journal in 1894-5.

In fact, in the last third of the 19 th century, before the emergence of the French school of geography in the Sorbonne, Reclus was seen as the French representative of modern geography, despite faults consisting in his over-literary style (at a time when a new style in scientific writing was becoming the norm), and his over-descriptive style (at a time when the fashion was more in favour of a sound naturalistic base and the exploration of natural causalities). This can be seen as a schizophrenic situation. Probably with some reluctance, he was caught up in a nationalistic appreciation of science. And indeed the requirements of his "salaried" status with the publisher Hachette (which he found difficult to endure) were in contradiction with the scientist ideal of the intellectuals of the day, as encouraged by the political regime.

Sensitivity towards the emerging geographical objects

We shall now see whether, beyond the differences relating to their scientific, professional and institutional generations, Reclus and his challenger Vidal de la Blache are complete strangers one to another when they confront issues in relation to which any geographer of the end of the 19 th century was likely to have to position himself. Only three will be discussed here, since they have been the object of particular study [START_REF] Pierre ; Bretagnolle Anne | Révolutions des techniques de communication et représentations du monde. Monde-point et monde difforme (1830-1840[END_REF]2003;Bretagnolle, Robic, 2005b): ecological sensitivity; the question of the large metropolitan areas, the experience of the finite nature of the world and in effect globalisation that was appearing at the turn of the 20 th century.

Reclus was one of those who, very early on, noted the risks of damage to the natural environment by human influences. Although he used the rather alarmist views of George P. Marsh, Reclus was overall more optimistic, confident in the ability of mankind to re-establish the physical balance it has upset. This ecological sensitivity appearing before its time can be found in several academics towards the end of the 19 th century [START_REF] Jussi | L"homme et la destruction des resources naturelles : la Raubwirtschaft au tournant du XXe siècle[END_REF]. For instance, like Reclus, J. Brunhes did not view this ecological risk as irreversible, nor did he see its global dimension (these were only perceived towards the mid 20 th century). This awareness of the risk went hand in hand with a holistic view of man and the earth, developed throughout Reclus" work, in a Romantic brand of science, impregnated with ideas of solidarity and harmony between man and nature. In relation to geographers of his time, the influence of Karl Ritter is evident, as for Vidal de la Blache. This influence contributed in both Reclus and Vidal an aspiration towards a unitary science, mere "geography", with no qualifier. But when they did qualify it, one with the epithet "social", the other with the epithet "human", their difference in viewpoint emerges. Likewise, in relation to a master of "colonial geography", M. Dubois, the difference is also evident, since Reclus sought harmony and beauty, the reconciliation of the beautiful with the useful in nature, while for Dubois nature was first a resource to be exploited, and geography the study of "the relationship of the master to his estate".

In another field, that of urbanism, Reclus also appears aware of what was at stake in issues of urban growth. Here he was in disagreement with many of his anarchist friends who supported the ruralist community models (for instance Kropotkine); he supported the virtues of democratic urbanism constructed at once on the conservative organicist model (Ruskin) and on that of civic rehabilitation experiments conducted by Patrick Geddes in Edinburgh. The interest he took in cities makes him in fact an active town-geographer, although more from the political "polis" angle than the "urbs" angle. In the same way, Vidal de la Blache, despite strong representations to the contrary, was also a geographer with an interest in the modern city. But through his arguments for regional cities capable of mobilising their surroundings, it is an economist"s position that Vidal adopted, with little sensitivity to democratic virtues or the scope for personal fulfilment that Reclus saw in the large contemporary metropolis. Both however based their analyses on what they saw as the major technological revolution of the time, the contraction of time-space as a result of the revolution in transport. For Vidal, the change in scale brought about by this revolution also required a change in the dimensions of regional patterns, in favour of the large city. Reclus, for his part, argued that the shrinking of time-distance was the material scope allowing the organisation of a center-periphery pattern in metropolitan areas so as to offer, in one and the same day, access to the collective and to individual pleasures: "Man must have the double advantage of access to the delights of the town, with its solidarity of thought and interest, its opportunities of study and the pursuit of art, and, with this, the liberty that lives in the liberty of nature and finds scope in the range of her ample horizon" (Reclus, 1895, p.264).

Finally, Reclus was particularly sensitive to the ongoing process of the unification of the planet. If he did not yet consider the whole world to be known in the 1870s, he was witnessing European colonisation and the irresistible extension of communication networks across the globe. The mobility and the speed of exchanges were synonymous with ubiquity: "The populations of townsnot those of the countryside for whom distances have decreased to a lesser degreehave become closer one to another, they live a common life, through constant exchanges of books, newspapers, letters and telegrams; they acquire a form of ubiquity" (Reclus, 1877, p.894). Vidal de la Blache reached the same conclusions, and also saw that time-distance was becoming the real spatial measure, and that the world was being miniaturised. Once again, however, their respective projects were different. Reclus wondered particularly about the ill effects of progress in communications, about the degree of emancipation of individuals and peoples that such progress could make possible, and conversely about the reinforcement of the power of the state that might result from it. Vidal de la Blache, for his part, was more interested in the economic consequences that would result.

Overall, at the start of the 20 th century, geographers from different generations were for the most part sensitive to the shrinking of time-space, and a certain form of emerging globalisation. However each applied this to his own project. Urbanisation and the large city alarmed many; but a few saw cities as the ideal place for exchange and circulation, favouring the development of civilisation. As for the vulnerability of the environment, if certain geographers and naturalists were aware of it at the time, the main community of geographers and common opinion were far from having the lucidity of Reclus and a few others. The colonisation of the earth and the exploitation of resources remained the priority. It is not surprising that the ideological and political commitments of these geographers differed, according to which issues they placed uppermost. Considering solely the cases of Reclus and Vidal de la Blache, it is obvious that for Elisée Reclus the issues were mainly political and social, whilst for Vidal de la Blache they were economic; as an anarchist Elisée Reclus gave primary importance to individualism and cosmopolitism, whereas Vidal de la Blache tried to reconcile patriotism with cosmopolitism (see [START_REF] Marie-Claire | Con o sin adjetivos? Algunas clasificaciones de la geografia y su sentido[END_REF].

Ranging among the issues that he himself constructed and tackled on the one hand, and on the other the issues viewed as important by those readers he has fascinated, sometimes in spite of themselves, "visiting and revisiting" Elisée Reclus also enables us to gain perspective on our own times and the challenges before geographers today.