Guillaume Claret

Yann Régis-Gianas

Mechanical Verification of Interactive Programs specified by Use Cases

Interactive programs, like user interfaces, are hard to formally specify and thus to prove correct. Some ideas coming from functional programming languages have been successful to improve the way we write safer programs, compared to traditional imperative languages, but these ideas mostly apply to code fragments without any inputs-outputs.

Using the purely functional language Coq, we present a new technique to represent interactive programs and formally verify use cases using the Coq proof engine as a symbolic debugger. To this end we introduce the notion of scenarios, well-typed schema of interactions between an environment and a program. We design and certify a blog system as an illustration. Our approach generalizes unit-testing techniques and outlines a new method for mechanically assisted checking of effectful functional programs.

I. Introduction

Implementing and proving correct interactive programs is challenging. Indeed, interactive programs are hard to reason about because they communicate with an outer environment (the operating system, the network, the user, . . . ) which may be under-specified and non deterministic. Moreover, the communications between the program and the environment can happen at many points during the execution and may depend on previous interactions.

Many techniques have been developed to model, specify and prove correct interactive or concurrent programs [START_REF] Manna | The Temporal Logic of Reactive and Concurrent Systems[END_REF]. For instance, process algebra and temporal logics are well understood abstract models for such programs. In these abstract models, some interesting behavioral properties can be automatically proved by model-checkers. Yet, these tools usually provide guarantees about the model of the program, not its actual implementation.

In another approach, called software-proof co-design, the specification and the verification of a program is not disconnected from its actual implementation. In that case, specifying, implementing and verifying are tightly interleaved in the software development process. This tight integration is possible within the Coq proof assistant which is both a programming language and an assisted prover. Yet, even if a realistic compiler for the C language has already been developed in Coq [START_REF] Leroy | Formal verification of a realistic compiler[END_REF], using Coq as a general purpose programming language may be considered a tour de force especially because it is purely functional and only accepts total and terminating functions. Our objective is to alleviate the cost of certified programming (i) by importing monadic programming technique from the Haskell programming language to express effectful and partial computations ; (ii) by mechanizing mainstream software engineering techniques inside Coq to ease the migration from unverified to verified specifications.

In software development processes, use cases [START_REF] Jacobson | Object-oriented software engineering -a use case driven approach[END_REF] are commonly used to specify and verify programs with inputs-outputs. A use case is basically a list of interaction steps between a program and an environment, in order to denote functional properties. A use case can be verified by manually running the program or by automated unittesting. However, unit-testing methods are never complete as soon as there is an infinite set of possible values for the program inputs. We will show how to verify use cases on infinitely many inputs using the notion of scenarios.

A lot of ideas coming from functional programming languages changed the way we structure software today. Among these ideas are the use of composable higher-order functions as the main building block [START_REF]Report on the Programming Language Haskell, A Non-strict Purely Functional Language (Version 1.2)[END_REF], referentially transparent expressions, algebraic data types, polymorphic [START_REF] Milner | A theory of type polymorphism in programming[END_REF] and dependent types [START_REF] Norell | Dependently typed programming in agda[END_REF]. Many programmers now use these ideas to increase the modularity and the correctness of their programs.

One of the limitations of most functional programming approaches is that they are often only effective on the pure (as "without inputs and outputs") fragments of a program. Other methodologies are required to write the impure (or interactive) parts (see for example [START_REF] Peyton | Tackling the awkward squad: monadic input/output, concurrency, exceptions, and foreign-language calls in haskell[END_REF]). For example, in the functional language Haskell, the impure computations are represented into a monad [START_REF] Wadler | The essence of functional programming[END_REF] using some special combinators. This monad isolates by typing the pure and impure computations, but offers limited ways to reason about the correctness of the inputs-outputs.

To extend and continue with the techniques developed in Haskell, we chose the purely functional language Coq to write and mechanically certify interactive programs. Coq is both a purely functional language and a theorem prover. The theory of Coq is based on the CIC [START_REF] Coquand | The calculus of constructions[END_REF] (the Calculus of Inductive Constructions type theory). It features rich inductive and dependent types, terminatingby-construction expressions and the ability to mix proofs and computations. Its advanced module system allows to write large developments. Coq programs can be compiled to native code for maximum efficiency.

We develop a new method to write and certify interactive programs by formal use cases analysis using Coq. We illustrate our method by programming and certifying a blog engine with a web interface. The sources are available online on https://github.com/clarus/coq-chick-blog.

In this paper we will introduce and present:

• the notion of computations to express interactive computations in the purely functional language Coq; • a semantics for the computations as the set of welltyped runs. A run describes both the trace, which can be built interactively, and the result of a computation; • a new technique to express and prove functional properties over interactive programs. To this end, we introduce the concept of scenarios which are schema of well-typed interactions between a program and an environment. The scenarios are a mechanical formalization of the reasoning by use cases for verifying a program; • a symbolic debugger for interactive programs, to assist the writing of scenarios and to spot bugs. This debugger relies on the existing tactics mode [START_REF] Delahaye | A tactic language for the system coq[END_REF] of Coq, using this mode to explore the execution paths of an interactive computation; • a blog system implemented and certified using our method. In particular, the user can login, add, edit or remove a post though a web interface. This blog system is compiled to an executable version using as an intermediate language the OCaml programming language (see http://ocaml.org/).

II. A challenge

Our challenge is to both develop and certify a blog engine in Coq. This challenge is interesting because a blog is a realistic example of a system with interactive user interactions.

Using this blog engine, the user is able to login, add, edit or delete a post. We save the posts to the file system, with one file per post. We take a very simple login system (no passwords) to concentrate on the architecture. The user interacts with the blog through HTTP requests.

We use an implementation of the HTTP protocol written in OCaml, a general purpose programming language. The blog itself is entirely written in Coq. We formally express and prove some non-functional properties and some functional properties reasoning by use cases. To generate a runnable executable of the blog, we compile the Coq code into OCaml code, and then to assembly code using the OCaml compiler.

Our trust base is composed of:

Inductive C (A : Type) : Type := | Ret : ∀ (x : A), C A | Call : ∀ (c : Command.t), (answer c → C A) → C A.
This means that a computation can be either:

• a pure expression x of type A;

• a call to the environment with an argument c of type Command.t and a handler waiting for an answer of type answer c, dependent on the value of the command. The role of a computation is to combine pure code fragments to form more complex programs interacting with the outer system.

Here is a computation printing the content of a file in the console: We call an external procedure to read the file README on line 2. The variable text is set to the answer of the call, which is expected to be the content of the README file. If the content is None (in case of error), we return the unit value on line 4. If the content is some text, we print it on the standard output using the command Log on line 6. Once the printing function has terminated, we return the unit value.

1 Definition print_readme : C unit := 2 Call (ReadFile "README") (fun text ⇒ 3 match text with 4 | None ⇒ Ret () 5 | Some text ⇒ 6 Call (Log text) (fun _ ⇒ 7 Ret ()) 8 end).
The values of the answers are left unspecified. We only assume there will be one answer of the right type for each call. We will see how to define execution traces and characterize the answers more precisely.

B. Runs

To reason about interactive programs we need to give a semantics to the computations. The semantics is defined by all the runs of a program. A run is an execution of a computation with explicit answers to the calls.

The type of the runs R is parametrized by a type A and a computation c of type C A. We define it inductively in Coq, by symmetry with the definition of computations:

Inductive R (A : Type) : C A → Type := | RunRet : ∀ (x : A), R A (Ret x) | RunCall : ∀ (c : Command.t) (a : answer c), ∀ {handler : answer c → C A}, (R A (handler a)) → R A (Call c handler).
A run can be either:

• a run of a Ret that carries the pure value x returned by a computation; • a run of a Call of a command c that received an answer a of the corresponding type and a run of a handler applied to the answer a. We do not explicitly write the handler terms since they are already in the definition of the computation and thus can be automatically inferred by Coq. Implicit parameters are declared into braces in Coq.

For the print_readme program, an example of run is:

Definition run_print_readme : Run unit print_readme := RunCall (ReadFile "README") (Some "Blabla") ( RunCall (Log "Blabla") () ( RunRet ())).

This run tells us that the program will call a command ReadFile "README". If we answer Some "Blabla", then it will call the command Log "Blabla" to which the only possible answer, of type unit, is (). Then the program terminates without any other calls. We can see this run as a form of very weak specification of the program print_readme, describing its behavior only when we answer Some "Blabla" to the ReadFile operation.

A run describes both an execution trace of a computation and the result of its evaluation with this trace. Thus, we can extract the result of a run with the function eval:

Fixpoint eval {A : Type} {c : C A} (r : R A c) : A := match r with | RunRet x ⇒ x | RunCall c a h r ⇒ eval r end.
We define eval by induction over a run. We recurse until we find the inner Ret and return its value. The eval function returns a value of type A as expected.

Similarly, we can extract the trace of a run: A trace is a list of dependent couples of commands and answers of the corresponding type. We recurse over a run, accumulating the command and the answer of each call in a list. Notice that since Coq is a normalizing language, by construction, the trace is always a finite list and the evaluation of a run always terminates.

We have given a formal definition of interactive computations in Coq and defined the semantics of a computation as the set of its runs. We will show how we used the notion of computations to build a blog server.

IV. Programming the server

We will present the code of a blog engine, and how we used the notion of computations to implement the input/output operations.

A. The server handler

The main function of the blog server is:

server : Path.t → Cookies.t → C Response.t
This function handles one request from the client. A request is a path (an URL, like /login) and the status of the client's cookies. A response is:

• a MIME type;

• a new set of cookies;

• a body, typically some HTML content. The server function returns a computation of response since it does calls to the system. The state of the blog is saved on the file system and accessed through system calls. In total, the blog system itself is made of 786 lines of Coq code.

The server function is pure, expect for the uninterpreted input/output operations. In particular, this function is deterministic, cannot return any exceptions and always terminates by construction. This is given to us for free, thanks to the strict type-system of Coq.

The path of the request, initially a string URL, is parsed by a pure Coq function to the sum type P ath.t. A sum type is a union of different types, each introduced by a constructor. The constructors of the P ath.t type are given in the figure 1.

This explicit sum type also describes the web API of the blog application. The NotFound and WrongArguments constructors are for ill-formed requests. Static retrieves

B. Edit a post

We will see in details how we implemented the handler for the PostDoEdit requests. This is the code extract of the function post_do_edit, which generates a response for a request of the form: We check on line 3 if the user is logged. If so, we call the function Helpers.header on line 7 which gets the metadata of a post from the file system. Its type is: We program by continuations to compose computations. Since the monads can generalize the continuation-passing style [START_REF] Moggi | Computational lambda-calculus and monads[END_REF], we could have added the operator bind operator:

∀ A,
Bind : ∀ A B, C A → (A → C B) → C B
but we preferred to keep our number of primitives as small as possible. We believe it simplifies the reasoning over the runs, but we are opened to discussions on this point.

If the header is not available, we return false for the success status to the continuation k on line 9. Otherwise we call the command UpdateFile on line 14 to update the content of the post on the file system. The notation call! on line 13 is a syntactic sugar for a call:

call! x := c in e ⇐⇒ Call c (λx. e)
The list of the calls we use is given on figure 2. Finally, we return a page PostDoEdit on line 17 with a link to the original post and the success status of the update.

The Response.t type is a sum type, with one constructor per kind of page. A purely functional pretty-printer then renders the corresponding HTML content. The prettyprinter is not verified.

We have seen how to program a blog engine in a typesafe manner in Coq using the notion of computations. In the next section, we will see how we verified this blog system.

V. Specifying the server The type-system of Coq already provides some safety properties on the computations, like the termination. We will go further, proving non-functional and functional properties using our notion of scenarios.

A. Scenario

A scenario is a set of runs of a computation. A scenario whose definition is accepted by Coq is a set of runs validated by its computation. The idea is to specify the behavior of the blog reasoning by use cases, verifying functional requirements.

A scenario is usually described as a family of runs parametrized by some user inputs. To be relevant, the use case or the expression of the scenario should be as clear as possible. An example of an informal use case is the following:

1) I add a new post as an authenticated user 2) I edit this post with some content c 3) I show this post and check that this is the content c I edited

We formally verified this use case by writing a well-formed scenario. To keep the explanations short, we will study the simpler use case of the index page service:

1) I connect to the index page URL 2) the blog calls the file system to list the available posts

• in case of error, a log message is printed on the server console 3) the index page is displayed with the list of posts

B. Symbolic debugger

To write scenarios we leverage the tactics mode of Coq. The tactics mode is normally used to prove theorems reasoning step by step. By using this mode to define scenarios, we get a kind of interactive debugger for computations: it is possible to evaluate a computation stepping through each call, like we would iterate into the reasoning steps of a theorem. At each call an explicit answer must be provided to go to the next call. The trace of the user interactions with the debugger is then a run of a computation.

More important, this debugger is symbolic: Coq being designed to manipulate symbolic expressions, we do not need to instantiate variables with concrete values. So the interactions with the debugger can actually describe sets of runs, that is to say scenarios.

The scenario of the index page when there are no errors is the following: This scenario describes a run of the server handler for each user cookie and list of post headers. We do not need to execute these runs: because index_ok is well-typed, we know they are all correct. They do just one call ListPosts and display the list of posts. This is a big advantage compared to unit-testing which would requires to run the program on each possible input, what is exhaustively impossible here since there are infinitely many inputs.

To construct this scenario using the debugger (the tactics mode), we type the first three lines. The Coq interpreter replies: This means that we have two symbolic parameters, cookies and headers, and aim to construct a run of the server handler applied to the index path and the cookies. We enter the simpl command on line 4 to partially evaluate the computation. Coq will use the fact that Path.Index is a concrete value. We get: We can guess what will be the next call unfolding the Main.Controller.index definition with the command unfold or looking directly at its source code on line 3 on figure 3.

1 Definition index (is_logged : bool) We guess it is ListPosts to some folder, to which we answer Some headers on line 7: apply (RunCall (ListPosts _) (Some headers)).

The Coq system validates our guess, unifying modulo evaluation the computation:

Main.Controller.index (Cookies.is_logged cookies)
with a computation of the form:

Call (ListPosts . . . ) (fun a ⇒ . . . )
We continue the evaluation of the computation by one step and get to:

Since we are on a Ret expression, the evaluation is terminated and we can conclude by the line 8, which explicitly states the expected result. In particular, we require the response to be the index page and to include the list of headers.

Likewise, we have defined a scenario for the index page with errors from the file system, by answering None to the call ListPosts. We have also verified the add, edit and show scenario.

In our experience, defining a scenario is similar to writing a unit-test. Indeed, a unit-test for an interactive program is basically a trace of all the responses of the environment to the program. This is exactly the same for a scenario, whereas the responses can be symbolic (representing an infinite set of possible values) and not only concrete (representing a single value).

C. Non-functional properties

We also verify some non-functional properties. Even if this not the main goal of the article, it shows that the notion computations is not only useful for the certification of use cases.

For example, we prove than an unauthenticated user cannot make a request which generates calls modifying the file system. To do so, we define a predicate: By disjunction on the path, we show in Coq that the predicate read_only is valid for any computation handling a request from an unauthenticated user:

∀ (path : Path.t),
read_only (Main.server path Cookies.LoggedOut) which proves our claim.

We have seen how to show both functional and nonfunctional properties over a computation. We can prove functional properties in an interactive way using Coq as a symbolic debugger.

VI. Compiling the server

We will explain how we compiled the computation of the blog system to an executable program, using an automatic translation to the OCaml language.

The Coq programming language is a purely functional language. We can represent the input/output operations but we cannot execute them. To do so, we use the extraction mechanism [START_REF] Letouzey | Extraction in coq: An overview[END_REF], which compiles Coq programs to the impure programming language OCaml.

We introduce some uninterpreted constants and extract them to specific OCaml impure expressions. For example:

Parameter printl : String.t -> t unit. Extract Constant printl => "Lwt_io.printl".

declares the Coq constant printl and associates it to the OCaml function Lwt_io.printl, which prints a line on the standard output. After extraction, this function will effectively display a line on the screen. As mentioned earlier, this compilation process is part of the trusted base.

We link the extracted code to the OCaml library Co-HTTP to handle the HTTP protocol. CoHTTP creates the main program loop, waiting for HTTP requests. The event-based concurrency model is managed by the Lwt library [START_REF] Vouillon | Lwt: a cooperative thread library[END_REF], a cooperative lightweight threads library for OCaml.

VII. Related work

Effectful functional programming have been intensively studied by the Haskell community, and large real programs have been written using this functional language. The main technique popularized by Haskell is the IO monad to express impure computations and to verify by typing the isolation of pure and impure expressions. Simon Peyton Jones gave a nice summary of the IO monad and other techniques [START_REF] Peyton | Tackling the awkward squad: monadic input/output, concurrency, exceptions, and foreign-language calls in haskell[END_REF]. We wanted to build upon this experience exploring new solutions, thanks to the more powerful typesystem of Coq featuring dependent-types and propositional types.

The Ynot project [START_REF] Nanevski | Ynot: Reasoning with the awkward squad[END_REF] studied the use of a parametrized monad to represent and reason about impure computations in Coq. This project focused more on the imperative and low-level memory management, using Hoarelogic [START_REF] Hoare | An axiomatic basis for computer programming[END_REF] with pre-and post-conditions together with separation logic [START_REF] Reynolds | Separation logic: A logic for shared mutable data structures[END_REF]. They explored extensions to reason about inputs-outputs and have written and mechanically certified a web application [START_REF] Malecha | Tracebased verification of imperative programs with i/o[END_REF]. Unlike our work, their application is specified by an invariant over the execution trace of the program. They do not study the verification of functional properties, or use cases.

The algebraic effects and handlers [START_REF] Plotkin | Handlers of algebraic effects[END_REF], a generic framework to represent effects in a compositional way in purely functional languages, led to a lot of research about proven safe effectful programs. This framework is more powerful than ours because it can represent many different kinds of effects, like non-determinism, exceptions, or states, and can combine them in a generic way. This power has a cost: the algebraic effects are also more complex to define and understand. It could be interesting to see if our notion of computations can be viewed as a particular case of algebraic effect.

The dependently typed programming language Idris[1] proposes an implementation of algebraic effects [START_REF] Brady | Programming and reasoning with algebraic effects and dependent types[END_REF]. Edwin Brady and Simon Fowler show how to specify the rules of a game or a web protocol and how to verify by typing their implementations in Idris (see [START_REF] Brady | Resource-dependent algebraic effects[END_REF] and [START_REF] Fowler | Dependent types for safe and secure web programming[END_REF]). These works mostly focus on expressing invariants and building the right primitives to write correct-by-construction programs. By contrast, we focused on specifications by use cases and on a tool, the symbolic debugger, to express these cases interactively.

Ur/Web [START_REF] Chlipala | Ur/web: A simple model for programming the web[END_REF] is a functional programming language and a platform for the web development made by Adam Chlipala. We can cite the BazQux Reader, a commercial RSS feed reader, as a successful application of the Ur/Web platform. The language Ur does not feature full dependent types, but can generate formally valid and unexploitable web pages and SQL requests thanks to its rich type system and its integrated platform. Combining our notion of scenarios with the ideas of the Ur/Web platform could be an interesting subject.

VIII. Conclusion

We have presented the notions of computations and runs to represent and to give a semantics to interactive programs in the purely functional language Coq. We have shown how to define and prove non-functional properties on a computation using predicates inductively defined on the combinators of the computations. We have introduced the notion of scenarios to denote and verify functional properties or use cases of a program. The usage of the tactic mode of Coq provides a symbolic debugger to write these scenarios interactively. To illustrate this approach, we developed and certified a blog system in Coq.

We would like to extend our techniques to a wider class of programs. In particular, we want to support asynchronous calls and concurrent computations. To add concurrency, we could use a fork primitive or an actor model. As an application, this would allow us to certify together the blog system, its HTTP front-end and its database or file system back-end, even in the case of concurrent user requests.

  assuming the following relations: ReadFile : string → Command.t Log : string → Command.t answer ReadFile = option string answer Log = unit the unit type being a special type with just one value (), used for function which do not return any meaningful results.

Fixpoint

  trace {A : Type} {c : C A} (r : R A c) : list {c : Command.t & answer c} := match r with | RunRet x ⇒ [ ] | RunCall c a h r ⇒ (c, a) :: trace r end.

Fig. 1 .

 1 Fig. 1. Constructors of the P ath.t type.

/ 2 ( 3 if negb is_logged then 4 ret Response.Forbidden 5 else 6 let 8 match header with 9 | None ⇒ k false 10 | 12 Post 17 ret

 2345689101217 posts/do_edit/url?content =content 1 Definition post_do_edit (is_logged : bool) url : string) (content : string) : C Response.t := ! is_success : bool := fun k ⇒ 7 let! header := Helpers.header url in Some header ⇒ 11 let file_name := posts_directory ++ (Response.PostDoEdit url is_success).

4 simpl. 7 apply

 47 (RunCall (ListPosts _) (Some headers)).

2 :

 2

Fig. 3 .

 3 Fig. 3. Source code of the index function

  is_read : Command.t → bool to check that a command does not modify the file system. By induction over a computation, we define what is a computation free of write operations: Inductive read_only {A : Type} : C A → Prop := | RoRet : ∀ x : A, read_only (Ret x) | RoCall : ∀ (c : Command.t) (handler : answer c → C A), is_read c = true → (∀ (a : answer c), read_only (handler a)) → read_only (Call c handler).

  the OCaml compiler and runtime • the implementation of HTTP in OCamlIII. Computations and runsWe will introduce the notions of computations and runs to represent and give a semantics to interactive programs in Coq.

	A. Computations
	A command is the value emitted during a call of a
	program to the outer environment. Let Command.t be a
	type of command and:
	answer : Command.t → Type
	the dependent type of the answers to these commands. The
	set of interactive computations returning values of type A
	is represented by the type C A, inductively defined in Coq
	by:

• the Coq system • the compilation process from Coq to OCaml •

  Index shows the main page. You use Login and Logout to login and logout (there is no passwords or user names). PostAdd shows the form to add a post, PostDoAdd effectively add a post. So do PostEdit and PostDoEdit to edit a post. PostDoDelete removes a post. Finally, PostShow shows the content of a post.

	Constructor	Arguments	Root path
	NotFound
	WrongArguments
	Static	list string	/static
	Index		/
	Login		/login
	Logout		/logout
	PostAdd		/posts/add
	PostDoAdd	string × date	/posts/do_add
	PostEdit	string	/posts/edit
	PostDoEdit	string × string /posts/do_edit
	PostDoDelete	string	/posts/do_delete
	PostShow	string	/posts/show
	static content such as CSS files.

  Fig. 2. Calls we use in the blog. := e 1 in e 2 ⇐⇒ e 1 (λx. e 2 )

	Command	Arguments	Answer
	ReadFile	string	option string
	UpdateFile string × string	bool
	DeleteFile	string	bool
	ListPosts	string	option (list header)
	Log	string	unit
	This function Helpers.header waits for a continuation,
	a function returning the next computation. The notation
	let! on line 7 is just a syntactic sugar to call a function
	with a continuation:
	let! x

string → (option Post.Header.t → C A) → C A

subgoals cookies : Cookies.t headers : list Header.t ______________________________________(1/1) Run.t (C.Ret (Response.Index (Cookies.is_logged cookies) headers))


Baudel

Thomas

Laetitia Dablanc

OPTIMIZING URBAN FREIGHT DELIVERIES: FROM DESIGNING AND TESTING A PROTOTYPE SYSTEM TO ADDRESSING REAL LIFE CHALLENGES

Keywords: round optimization, Intelligent Transportation Systems, city-wide optimization, city logistics

In this article, we present efforts towards building a city-wide freight delivery rounds optimization system aimed at leveraging city traffic information to optimize professional vehicle rounds. This project, called SmartDeliveries, has been developed as part of the OptimodLyon project. We present the system's architecture and general objective. Then we present early evaluations which have led us to identify three main technical challenges to address, but also to quantify the potential productivity gains for its users: 18% in distance savings and 11% in time. This could lead, if the system were to be generalized at the scale of the city, to a reduction in as much as 5% in traffic, and to corresponding savings in emissions, which are the primary motivation of the project leaders. Finally we discuss the remaining challenges to address, from a technical as well as an organizational standpoint, to introduce real life implementation of the system.

INTRODUCTION Context

Traffic management in major cities faces well-known but major challenges. While mobility is directly tied to economic growth and prosperity, road networks are saturated. Costly attempts in the 1960's and 1970's to adapt European cities to massive car influx have yielded negative externalities, demonstrating the lack of sustainability of the approach. The current approaches in Intelligent Transportation Systems (ITS) favour, among others, to rely on better information processing from all the actors involved to develop alternate mobility patterns, for instance encouraging the use of public transports and cycling, or deferring rush hour travels.

OptimodLyon (http://optimodlyon.fr/en/) is a three year project supported by the French agency for the environment, in which eight industry partners, among which IBM, four academic institutions and the metropolitan authority of Lyon (called Urban Community of Lyon) work together to improve urban mobility through better collection, processing and distribution of mobility information. The flagship application of OptimodLyon is a real-time, predictive, multi-modal journey planner. This application lets travellers plan their journey through a combination of car, public transportation and bike sharing with the best available information. The expectation is to enable a reduction of 1% of the car modal share on the city, resulting in saving 25 kTe carbon of emissions per year and significant traffic improvements during rush hours, at a very reasonable cost compared to the amount of public works that are usually needed to obtain similar levels of decongestion.

Planned, professional urban mobility

Despite environmental concerns, there is a large portion of road traffic that will not lend itself easily to modal transfer. According to the (Academie des Technologies, 2009) report, 35% of road trips carry goods rather than people. If we account for the important portion of movements that involve moving both goods and persons to deliver a value added service (such as maintenance and construction visits, catering, sales visits…), an even larger portion of existing road traffic needs to be accounted for. We call this portion of the traffic we focus on "professional urban mobility" and we estimate (counting campaigns performed internally) that it covers at least 50% of daytime urban traffic. Most policies aimed at limiting private vehicle use affect almost equally professional urban mobility, which could impact economic activity negatively. Any policy aimed at limiting the negative externalities of urban car travel must therefore target this portion of the traffic properly.

Businesses are also acutely aware and affected by the cost of mobility and have direct incentives to rationalize it. For instance, fuel represents 18% of the total costs of a small freight operator employing 200 persons (undisclosed personal communication). Current estimates (CERB, 2007) consider that 20 minutes lost in urban traffic amount to about eight euros for such an operator, which represents, by-and-large, its gross financial margin for a half-day vehicle round. We can therefore consider there is a synergy of goals between public authorities and the private businesses in curbing congestion and optimizing trips. The shared objective of both public and private stakeholders is to tend towards the minimization of vehicle-kilometers and time spent on the road.

Our work stems from the observation that a large portion of professional mobility demand is actually planned. Somewhere, in the information system of the companies, the intent to move is known in advance, at a close informational distance from an internet connection. If the city can securely obtain this information and use it to improve its traffic forecast, providing in return relevant suggestions that can reduce the cost of mobility, both parties could benefit from this exchange of information.

Synergy between cities and freight operators

The expected gains of a cooperative data exchange for cities and road users are as follows:

• Freight trip planning data constitutes a new source of information for traffic regulation, providing an advance view of freight mobility, which represents a sizable portion of traffic.

• Data exchange provides a new regulation tool, enabling to divert a sizable portion of traffic outside of congested areas. • Because the service may measurably save time and money to its users, it can be turned into a revenue source for the city to leverage its traffic regulation investments.

For its users, we expect a high profitability, as distance and time savings shall directly impact their revenue. Finally, the costs of exploiting such a solution shall be fairly small, as all it requires is an information infrastructure whose core hardware aspects are already in place: internet, mobile phones, and traffic data.

Of course this is still an idealized view of the system we propose. In the remainder of this paper, we will present an implemented prototype, then discuss the evaluations we have performed with three companies and 4000 time-stamped and geolocalized tours. These tests led us to identify three major technical challenges, as well as helped us quantify the potential benefits of the system. In the final section of this paper, we will discuss the remaining challenges, which are equally divided between technical and organizational considerations.

OVERVIEW OF THE PROPOSED SYSTEM

SmartDeliveries [START_REF] Baudel | Optimisation du fret et des déplacements professionnels planifiés dans le projet OptimodLyon[END_REF]) is a software service and a set of applications comprising the following elements (Figure 1):

• A situation monitor maintains a model of the current and forecast traffic conditions for the whole city. It connects to the city information services (such as data.grandlyon.com) to gather planned events and public works information, real time and forecast traffic conditions, weather data. It provides means to plan routes and current and future travel time estimates. • A demand monitor gathers users' mobility plans. It is accessed either via a web application (for occasional users) or a dedicated web service (connecting to the firm's information services). The plans are provided as plain csv files comprising a list of destinations, together with constraints on the trips, such as time and precedence constraints. • A routes monitor creates, optimizes and follows all planned trips in real time, adapting to the observed route taken (as the driver stays in control of the plans), and provides optimization suggestions and alerts when there are traffic events from the city or deviations from the initial plans. It connects to a mobile application that acts as a route planner and provides traffic alerts. Once fully implemented, this architecture shall enable the computation of global optimization plans, enabling to spread traffic in time and space when potential delivery parking spots congestion is detected. The key implemented components for now are the travel time estimator and the time-dependent, robust optimization service, which will be described hereafter.

Usage scenarios

The system is meant to be used first in the morning, once the rounds have been assigned to individual drivers. The fleet manager can either upload route sheets on a web interface in a straightforward csv file format, or, for larger companies, the IT system can be directly interfaced via web services to the route optimizer. The system in return provides route recommendations, including public works and events that may impact the trajectory. For ease of integration, those can either be printed and given to the driver for guidance, or they may be uploaded on a smartphone application, which the driver may use to perform amendments to the suggested route, often adding constraints that are known only by them, such as the opening and closing hours of the delivery locations. Route changes and constraints on the delivery locations are stored for future reuse, which provides a degree of knowledge sharing and simplifies the daily use of the application for repetitive rounds.

When the planned tour has been downloaded on a GPS-enabled driver's mobile phone, the application with follow the driver, and manage to guess the course of the round, issuing planning corrections if the driver decides not to follow the initial recommendations. There can be many good reasons for a driver to modify the proposed tour, as we will see later, so the system is designed as a "recommender" rather than a prescriptive system. We believe this is a key issue to ensure that users accept to be tracked by a GPS enabled device. As an additional benefit, traffic events (such as accidents and congestions) are relayed to the mobile phone and trigger alerts and route change proposals, possibly re-ordering the stops so that problematic locations can be avoided. To the drivers, and the city, this later feature is seen as quite novel over common navigation aids: the ability of the planner to foresee several steps ahead allows issuing more complex re-routing than one-step ahead suggestions. Of course, it is possible to limit the amount of re-ordering, to account for heavy cargo that cannot be moved easily.

Although fairly new, some commercial systems do provide somewhat similar functionalities, but the integration of the services, the interfacing with the city's ITS, and the deliberate design as a recommender rather than a prescriptive system represent, to our knowledge, innovations.

EVALUATION OF THE SYSTEM

We performed extensive studies and projections to assess the suitability of the system to its purpose. We could identify a number of technical hurdles to overcome. Once they are, the gains seem fairly substantial.

Resources and methods

The city provides six minutes real time and historicised traffic data over 600 detectors spread throughout the urban area, advance data of the public works impacting road usage, as well as a DATEX II event stream manually fed to alert of ongoing traffic events such as accidents and major congestions (http://data.grandlyon.com/). Several studies [START_REF] Godinot | Mise en forme du réseau de routier sur l'Aire Urbaine de Lyon[END_REF][START_REF] Bousquet | Optimisation d'itinéraires multimodaux fondée sur les temps de parcours à l'échelle d'une agglomération urbaine dense[END_REF][START_REF] Leclercq | Règles de calcul pour la détermination de la vitesse moyenne et des temps de parcours[END_REF] have shown that historic traffic data together with known planned events allow for providing a somewhat accurate picture of traffic, and thus create a time-dependent travel time model usable for route planning. Our goal is to see if this knowledge can be used to optimize vehicle rounds at the scale of the city.

We first conducted a survey, interviewing about 50 drivers, fleet managers and logistics managers in France, from large to small freight carriers, in order to collect needs and assess workflows. When we started the studies, in 2012, all freight carriers had plans to leverage mobile technologies to improve agility and service to customers, but no system was fully operative or functioning as expected. Drivers mostly relied on their field experience to organize their rounds, using simplistic but somewhat effective nearest-neighbour heuristics to optimize their route. Existing routing system seemed to lack precision in travel time estimation to provide usable guidance, at least in the companies we surveyed. In 2015, all major companies are equipped with GPS vehicle tracking, and they are somewhat satisfied with the ability to better inform their customers of expected delivery time, and to better measure the productivity of their drivers. Yet, route optimization still appears of little use in urban round planning.

In order to assess why, and to see if accurate traffic information received from the city would remediate this reluctance to optimization, we have obtained two full months of complete delivery rounds, time-stamped and geo-localized, from three freight carriers in Lyon. This represents over 80,000 individual moves, 4,000 rounds, averaging 20 positions per round, and 10 minutes on average per trip. After various stages of data cleansing (described below), we obtained a test set of 1715 rounds that were suitable for evaluating the potential gain of a cityscale round optimization system (Figure 2). Using traffic and event data from the city for the corresponding months, we simulated our system to assess whether we could have provided the drivers with better routes. The key findings started with the identification of three major technical challenges:

• Understanding the mobility intent from the set of addresses that had been provided.

• Estimating travel times correctly.

• Optimizing algorithms that leverage accurately the available city data.

We will examine those issues in detail before assessing the potential value of the system.

Understanding the mobility intent

While seemingly trivial, figuring where a delivery is to be made given a written address turns out to be a challenge. 40% of the addresses that were provided to us in the pilot did not conform to a standard format. Geocoding is a difficult problem, which is highly dependent on local conventions, and which involves careful trade-offs to avoid overfitting while still providing enough error recovery [START_REF] Goldberg | From Text to Geographic Coordinates: The Current State of Geocoding[END_REF]). After fuzzy-match geocoding, 16% of the addresses are still imprecisely located, and 1% wrongly located. Note that our results compare favourably to off-the-shelf solutions such as Google maps, as we specialized our algorithm for the data at hand. Examples of imprecisions include: providing only a cell phone number as address, or providing a phrase such as "Street XX, construction site in front of the bakery." Quite often, the point of delivery is different from the postal address provided by the sender; for instance, the address is that of a shop, but deliveries are to be made in a back alley or at another location. All in all, after manually resolving the uncertainties, we estimate that about 8% of the addresses cannot be precisely resolved before the round, but will instead require some on-site searching by the driver. Depending on the type of shipment (express or standard deliveries, business or individual shipping), about 1-2% of the deliveries will return at the warehouse for lack of finding the proper delivery location.

Freight carriers are well aware of this issue. Right now, they partially alleviate it by performing systematic geotagging of all delivered addresses, so that the same loss of time shall not happen twice. In order to provide robust route planning under these circumstances, our system must take into account the uncertainty of delivery locations, adding extra padding time in proportion to the uncertainty of the interpreted location. Addresses that are completely unrecognizable are discarded from the round optimization, and extra time is added to the total time estimate of the round to account for the time to search for the delivery address. The driver is reminded of this uncertainty in the mobile application, and asked to notify when the proper location has been found to allow further occurrences of this address to be taken into account properly.

This particular technological issue highlights the importance of the driver expertise: experienced drivers have usually much lower return rates and higher productivity. This guides our choice to function only as a recommender system and be flexible about the deviations of the driver from the established path. Still, we believe proper interpretation of the rounds is a major issue to address to make the SmartDeliveries system bring its full potential.

Estimating travel time

The travel time estimation model used initially [START_REF] Leclercq | Règles de calcul pour la détermination de la vitesse moyenne et des temps de parcours[END_REF] relies on a set of rules which derive average speed for all road segments on the network based on a small number of variables: period of the year, time of day, measured or predicted congestion and various other road characteristics. While this model fits the available data overall (6% difference between observed and predicted total travel time), it is hardly usable due to the huge observed variance for individual trips: the average error for individual trips of 10 minutes reaches 55%. Worse, the use of a rule-based model introduces internal biases, which distort the error distribution outside of a normal law. As a consequence, errors along a full round do not compensate each other as well as the law of large numbers should allow. The result is that the overall standard deviation for the rounds is much higher than the estimates drivers provide when polled informally (23% vs. 15-20%). While a standard deviation amounting to 50% for trip durations of 10 minutes is of little incidence on the perception of the system reliability, it is more critical that the estimate for the overall tour match the expectation of the users. If we were to provide the system as-is to drivers, the discrepancy between forecast and observed travel time for the full round would generate distrust in the system reliability and reduce acceptance.

Improving on our travel time estimation required a novel approach, detailed in [START_REF] Ashton | Travel time forecast on an urban network using lowfrequency GPS Data[END_REF], which we summarize here. We first ran supervised learning regression methods to build a decision-tree-based predictor of travel time based on route features. The predictors took as inputs various attributes of the tour, including the geocoordinates of the origin and destination, the time of day, day of week, distance between origin and destination (along the shortest path), the eccentricity of the trip (angle of the travel direction taken from the city center), the observed congestion along the travelled path, the round identifier (drivers tend to serve the same neighbourhoods every day, and are specialized for one type of delivery service, with a specific type of truck. All those are summarized by the round ID). Using a 5fold method for cross validation, we found slightly better results for travel time estimation: 41% for individual routes, and 21% for the full rounds. The interesting lesson however is that the predictor assigns a strong predictive weight to the round id, which encapsulates many endogenous aspects of the round, while other exogeneous factors, such as the observed congestion (Occupancy attribute) have far less influence on travel time ( This observation yields to the following interpretations:

• The relatively low impact of occupancy rate suggests that congestion, while definitely noticeable, is fairly quickly remediated by the traffic regulation center, and hasoverallonly a low impact on total travel-time. This has been confirmed by the regulation authorities, in the following terms: "Our goal is not to get rid of all congestion, this is impossible. Rather, it is to make sure that on any trip, congestion won't impact you by more than five minutes". This does not mean in any way that our model can get rid altogether of city traffic information. On the contrary, awareness of the accidental or forecast (closed roads) congestions is of high value to drivers, even if it is used only 20 times per year. Provided this information is accompanied with an alternate route, it offers the opportunity to save some of what some drivers call "jours de galere" (bummer days), when a slight delay at the beginning of the round triggers cascading effects that impact the full round, resulting in a net loss for the day's work. • The high impact of the "round ID" attribute means that different drivers/round types have differing average speeds. In other words, endogenous aspects of the round may have a much higher impact than exogenous factors such as global road conditions. Interviews with drivers have confirmed that experienced drivers are far more productive than beginners, and of course, drivers may adopt less civil behavior when they are under stress, or take a time off if they see that their progress has been good. This suggests a fairly important degree of elasticity in the travel time estimate, and that our estimates shall be improved by a travel time prediction model that includes historical knowledge of the driver and vehicle past driving patterns in its input variables.

These observations have led us to propose a new travel time prediction model [START_REF] Ashton | Travel time forecast on an urban network using lowfrequency GPS Data[END_REF], based on estimating a trip duration with a weighted average of k-nearest neighbours taken from historical data. When the distance between the trip to perform and its nearest neighbours is too large, then the model relies on the simulation-based model defined by the traffic authority. The model parameters have been determined by cross-validation on our dataset. This new model enables reaching the precision wished, with an average error of 43% on individual routes, and 13% on rounds, with 83% of the rounds being inside a 20% margin error. This roughly matches the estimates drivers provide when interviewed.

In summary, while progress is still needed, it appears of utmost importance that a travel time estimation model take into account endogenous aspects of the round to be performed to perform adequately, which is not the case of most off-the-shelf travel time estimators.

Optimizing vehicle rounds

The core problem at the heart of round optimization, the Traveling Salesman Problem (TSP) under constraints, is a well-known "hard" computational problem. In addition, our optimization model involves precedence and time window constraints, time-dependency (the expected duration of a trip varies with the time of day), and uncertainty (the travel time is known only within certain bounds). The approach we have chosen to solve the TSP relies on constraints-programming and scheduling [START_REF] Baptiste | Constraint-based scheduling and planning[END_REF], [START_REF] Laborie | Reasoning with conditional time-intervals[END_REF], [START_REF] Laborie | Reasoning with conditional time-intervals. Part II: An algebraical model for resources[END_REF]. Our first implementation (Aguiar-Melgarejo et al, 2012), using state-ofthe art but straightforward approaches, would require on average 90 seconds of computation to provide a solution for a round. While this is sufficient for an individual round and for evaluating the potential impact of the system, it would prove highly impractical if used in production. If we assume thousands of rounds to optimize and that each round requires about three recomputations in the course of the day, this means hundreds of hours of intensive processor time per day. Because most rounds are planned in the morning hours between 6 and 8 am, and the response time should not exceed a few minutes per request, implementing a city-scale solution would require a significant datacenter (hundreds of processors) to deliver results in a reasonable timeframe. Given the expected returns, even if the results were allowing substantial savings to its users, the solution would not be economically feasible.

Fundamentally, the model for optimizing an urban vehicle round under constraints is the Time-Dependent Traveling Salesman Problem (TDTSP). The solution we provide involves implementing a global "TimeDependant no-overlap" constraint, that takes as parameter a distance tensor (origin-destination temporal matrix, wherein each of the element is a function of time indicating the distance from an origin to a destination over time). This new constraint and its benchmark are described in [START_REF] Aguiar Melgarejo | A Time-Dependent No-Overlap Constraint: Application to Urban Delivery Problems[END_REF]. It allows leveraging the distance tensor to further propagations to drastically cut the search space.

This new constraint enables our algorithm to find the optimal solutions in 0.1s of computation for rounds of 20 positions, and reach a minimum at 5% of the optimal solution in five seconds on average (Figure 3). This 13-fold performance increase makes our approach scalable, requiring only a dozen or so processors to serve the potential needs of a city the size of Lyon. Further work is required to adapt the model to the uncertainty of transition times.

Figure 3: Average time needed to compute optimized tours. NoOverlap is the straightforward approach, TDNoOverlap is the approach taken in [START_REF] Aguiar Melgarejo | A Time-Dependent No-Overlap Constraint: Application to Urban Delivery Problems[END_REF]. Note the vertical scale is logarithmic.

OPTIMIZATION RESULTS (projection)

Results for the freight companies

After filtering for poorly resolved delivery locations and rounds whose travel time forecast did not match the recorded data correctly, we obtained the test set described above consisting of 1715 rounds. Applying our optimization algorithms, we found the possibility of saving 18% in distance on average, and 11% in time.

The following example (Figure 4) is a round performed on June 12, 2014. It started at 8:50, consisting of 38 positions (some positions being at the same address). The difference between forecast and observed duration is 7%, and the truck has been on its delivery locations for 53 minutes.

Actual tour Optimized proposition

Results at the scale of the city

As our initial goal is to study the feasibility and potential impact of the solution for city traffic regulation, we have further projected what those individual gains could provide if the system was adopted at the scale of the city.

In partnership with the Grand Lyon climate protection service, we have obtained data after running the Freturb model [START_REF] Routhier | Mesurer l'impact du transport de marchandises en ville -Le modèle de simulation FRETURB[END_REF]. According to Freturb, there are on average 7630 rounds per day over the city, among which 2400 (31%) serve more than 10 positions and could be optimized. In a rough approximation, if our number of 50% of daytime traffic qualifies as "professional urban mobility," and 31% may benefit from our optimization service, this means SmartDeliveries offers the perspective of a reduction of 2.8% of traffic, with a net positive economic gain, as the productivity of the drivers is increased.

CHALLENGES AND FUTURE WORK

SmartDeliveries is now in preparation for conducting live tours with a few selected participants. Two main types of issues need to be carefully addressed: technological and organizational.

Technological challenges

Between 2012 and 2015, conditions have drastically changed, as many freight companies and drivers have acquired off-the-shelf hardware and information systems that they can leverage to use the proposed solution, at a very small cost. However, the key technological challenge remains the ability to gracefully manage the uncertainties in delivery locations and travel-time estimations. This is to be addressed partly by optimization algorithms that take these uncertainties into account, but also via user interfaces and proposed workflows that acknowledge these uncertainties, adapt to field constraints that the driver may not be able to inform the system about, and leave the user in charge. Finally, once sufficient volume can be reached, global optimization integrating delivery parking spots availability should be a significant challenge.

Organizational challenges

Urban freight distribution is made by a very large variety of freight operators [START_REF] Dablanc | Goods Transports in large European cities: Difficult to organize, difficult to modernize[END_REF]. Just in the parcel and express transport sector, for example, some very big transport companies (Chronopost, UPS, DHL for France) work alongside very small ones, with few employees, or no staff at all other than the drivers themselves (own account drivers). These small companies, which can be more than several thousands operating in a single large city such as Lyon or Paris, often work for the large ones, carrying the goods and providing the final deliveries on their behalf, as contractors. This specific end of the freight market suffers from very low profit margins and difficult working conditions. These small players may find it difficult to consider investing in a new technology, preferring to deal with delivery tour incidents with their own human resourcefulness. They will need to see actual gains of the system before joining it. Also, when embedded in highly dependent relationships with large transport companies (Reme [START_REF] Harnay | La sous-traitance de la messagerie urbaine: logistiques économiques et rapports de dépendance?[END_REF], small companies will not always be able to decide for themselves if they can join the system or not. Large operators, although more technologically savvy than small ones, can be reluctant to export their data on systems they do not fully control and they may raise security issues.

However, the framework in which urban freight deliveries are currently operated may be changing rapidly, specifically in French cities, allowing for more favourable conditions for the adoption of a delivery optimising system. Access regulations in city centres such as low emission zones are currently being adopted [START_REF] Dablanc | Impacts of environmental access restrictions on freight delivery activities, the example of Low Emission Zones in Europe[END_REF]. Municipalities increase bicycle use and promote roadway usages competing with delivery activities. Also, the rise in "residential deliveries" (deliveries for e-commerce consumers, at home or in pickup points spread around residential and commercial neighborhoods) in cities is adding a significant layer of complexity to delivery round planning. All these new urban conditions may make it more difficult to operate "low cost" last mile deliveries and may generate interest in optimization systems integrating real time data from all stakeholders.

CONCLUSION

There are good reasons to believe that no human can find near optimal solutions to the timedependent traveling salesman (TDTSP) problem for more than a few positions: the problem is proven to be hard to solve. The heuristics commonly employed by drivers, such as always moving to the nearest non-visited position, are quite robust and rarely yield very bad rounds. But those solutions are still far from the optimum. It is very reasonable to expect that 10 to 20% of productivity increase can be found if state-of-the-art algorithmics can applied successfully to the urban delivery round problem. Furthermore, this productivity increase would come with improved traffic conditions, benefiting all city residents.

Freight carriers and vehicle fleet operators are well aware of this opportunity, and numerous attempts have been made in the past 30 years to materialize this potential. In North America, several companies such as routific.com are starting to propose services that come close to our proposition. Yet, in practice, at least in Europe, drivers still prefer to rely on their experience, as the provided "optimized" plans often prove to be not so optimal in practice and fail in providing the needed flexibility.

Our hope is that injecting city traffic information to the optimization process, correctly assessing the travel time by taking the driver's experience into account and designing the full workflow of the optimization as a recommender system rather than a prescriptive system, we could see those expectations finally come to fruition. New urban conditions in which companies will operate in the future may provide a favourable milieu for the adoption of smarter technologies for urban deliveries.

Figure 1 :

 1 Figure 1: Smart Deliveries architecture

Figure 2 :

 2 Figure 2: key indicators of the cleansed round data for evaluation of potential gain and locations of the delivery points. Larger spots correspond to warehouse locations.

Figure 4 :

 4 Figure 4: example of optimization of a complex delivery round.

Table 1 :

 1 Table1). Gini importance of the main attributes of the decision tree predictor

	Feature	Distance	Round ID	Static travel time forecast	Occupancy	Angle	Time of day
	Gini importance	77	11	6	2	1	0.5

ACKNOWLEDGEMENTS

The OptimodLyon project, of which SmartDeliveries is a part of, is partly funded by ADEME and the French Investissements d'Avenir research programme. We wish to thank the OptimodLyon project's partners; Jean Coldefy, Diana Diziain and Luce Ponsar from the Grand Lyon; the freight companies who provided data and answered surveys; Philippe Laborie from IBM and Christine Solnon from INSA Lyon for advising optimization research, and the interns who contributed to the project: Pierre André, Clément Mathieu and Lexi Weng.