Daniel Câmara

Frederic Urbani

Mathieu Lacage

Thierry Turletti

Walid Dabbous

Simulation

Simulation Platform for Content Centric Networks Protocols Development

Keywords: Validation, Simulation, Emulation, Troubleshooting Presentation type: Technical talk

ou non, émanant des établissements d'enseignement et de recherche français ou étrangers, des laboratoires publics ou privés.

Presentation

The platform described in this work enables researchers to perform large scale experiments, in a controllable, realistic and repeatable way. The proposed framework relies on the combination of three main pieces of software: CCNx, ns-3, and Direct Code Execution (DCE) tool. DCE is a package we developed that is able to run, without any source code modication, real applications and protocols over the ns-3 simulator. Ns-3 is a powerful open source discrete-event network simulator. The framework trusts ns-3 to handle all the nodes interconnections and topology related issues. DCE is responsible for running the unmodied CCNx code and making the interface between CCNx and the simulator. The framework opens the gates for the CCNx community to the full power of the ns-3 simulator, and all its modules (e.g. WiMax, WiFi and LTE implementations). It is important to notice that, as the platform uses DCE to run the real CCNx, the very same code, developed using the simulated framework, can be executed over real networks without any change. Moreover, the platform allows developers to use standard debuggers to evaluate the status of the whole simulated network. One can, for example, add breakpoints and verify the state of variables and packet headers on any layer, of any node, of the simulated network. The proposed CCNx simulation platform is a valuable tool that intends to help researchers in the implementation, evaluation and troubleshooting of new CCN algorithms and applications.

Interests

Experimental results of research issues, e.g. caching, routing and resource management


Fatma Jebali

Frédéric Lang

Radu Mateescu

GRL: a Specification Language for Globally Asynchronous Locally Synchronous Systems ⋆

A GALS (Globally Asynchronous, Locally Synchronous) system consists of several synchronous subsystems that evolve concurrently and interact with each other asynchronously. Most formalisms and design tools support either the synchronous paradigm or the asynchronous paradigm but rarely combine both, which requires an intricate modeling of GALS systems. In this paper, we present a new language, called GRL (GALS Representation Language) designed to model GALS systems in an abstract and versatile manner for the purpose of formal verification. GRL has formal semantics combining the synchronous reactive model underlying dataflow languages and the asynchronous concurrent model underlying process algebras. We present the basic concepts and the main constructs of the language, together with an illustrative example.

Introduction

Computer science has led to new generations of heterogeneous systems called GALS (Globally Asynchronous, Locally Synchronous). A GALS system is composed of several synchronous subsystems, executing and interacting in asynchronous concurrency: no assumption is made, neither on the relative frequency of each subsystem, nor on the communication delays between subsystems. Each subsystem is composed of several components running together synchronously, all governed by a single clock and encompassing the zero-delay assumption: computations and communications between components are instantaneous (these are called the synchronous assumptions). As such, GALS systems involve a high degree of synchronous and asynchronous concurrency (introducing nondeterminism), which requires tedious effort to design and debug. Formal modeling and verification is then a crucial part in the design process of such usually safetycritical systems.

Many different approaches have been proposed for GALS modeling and verification. Some propose to model GALS systems in synchronous frameworks (such as Signal [START_REF] Mousavi | Modeling and Validating Globally Asynchronous Design in Synchronous Frameworks[END_REF]) directly or to extend synchronous languages with an asynchronous layer (Multiclock Esterel [START_REF] Berry | Multiclock Esterel[END_REF], CRSM [START_REF] Ramesh | Communicating reactive state machines: Design, model and implementation[END_REF]). Such representations are well-suited to hardware-based subsystems distributed on one single hardware platform, each with its own clock.

Other approaches, conversely, extend asynchronous languages to incorporate synchronous features. The most common approach is to surround each locally synchronous subsystem by an asynchronous wrapper, which provides an asynchronous interface to other subsystems. This way, GALS systems can be modeled and verified in asynchronous frameworks. In [START_REF] Doucet | A verification approach for GALS integration of synchronous components[END_REF], Signal modules are translated to Promela, the input language of the SPIN model checker [START_REF] Holzmann | The model checker SPIN[END_REF]. In [START_REF] Garavel | Verification of GALS Systems by Combining Synchronous Languages and Process Calculi[END_REF], Sam synchronous programs are represented by Mealy functions without internal state and are encapsulated into wrappers modeled in LNT [START_REF] Champelovier | Reference manual of the LOTOS NT to LOTOS translator (version 5.4)[END_REF], a language of asynchronous concurrent processes inheriting process algebraic concepts and extended with data and the control structures of classical algorithmic programming. LNT is equipped with the CADP verification toolbox [START_REF] Garavel | CADP 2011: A Toolbox for the Construction and Analysis of Distributed Processes[END_REF], which comprises tools for visual checking, model checking, and equivalence checking. Previously, LNT had been used successfully for the analysis of other GALS systems [START_REF] Coste | Towards Performance Prediction of Compositional Models in Industrial GALS Designs[END_REF][START_REF] Garavel | On the Semantics of Communicating Hardware Processes and their Translation into LOTOS for the Verification of Asynchronous Circuits with CADP[END_REF][START_REF] Lantreibecq | Model Checking and Co-simulation of a Dynamic Task Dispatcher Circuit using CADP[END_REF].

All the aforementioned approaches adopt specific techniques of a specific paradigm (synchronous or asynchronous) to accommodate GALS systems. On the one hand, synchronous frameworks are deterministic by nature, and not appropriate to model asynchrony. On the other hand, asynchrony and nondeterminism are granted for free in asynchronous frameworks, but those lack built-in constructs dedicated to synchronous components, which guarantee that system models fulfill the synchronous assumptions.

Moreover, most existing approaches depend strongly on the considered application field (e.g., distributed control systems [START_REF] Yoong | Synthesizing Globally Asynchronous Locally Synchronous Systems With IEC 61499[END_REF], FPGA and ASIC digital designs [START_REF] Carlsson | Synchronous design flow for Globally Asynchronous Locally Synchronous systems[END_REF][START_REF] Muttersbach | Practical design of globallyasynchronous locally-synchronous systems[END_REF], or networks on chip), the target platform (e.g., software [START_REF] Malik | SystemJ: A GALS language for system level design[END_REF], hardware [START_REF] Doucet | A verification approach for GALS integration of synchronous components[END_REF], or heterogeneous), and the preferred specification methods (e.g., based on Petri nets [START_REF] Moutinho | State space generation for Petri nets-based GALS systems[END_REF], automata [START_REF] Günther | On the Formal Verification of Systems of Synchronous Software Components[END_REF], process algebras [START_REF] Garavel | Verification of GALS Systems by Combining Synchronous Languages and Process Calculi[END_REF]). This narrows down the range of systems that can be addressed. On the other hand, the surge in complexity of GALS systems forces designers to tackle (among others) design concepts, synchronous and asynchronous computations, deterministic and nondeterministic behaviour, and verification approaches, which makes the design of such systems increasingly challenging.

To circumvent this complexity, an appealing trend has been to design new languages dedicated to GALS system modeling [START_REF] Berry | Communicating reactive processes[END_REF][START_REF] Malik | SystemJ: A GALS language for system level design[END_REF][START_REF] Bultan | Action language: A specification language for model checking reactive systems[END_REF], which enforce the assumptions of the GALS paradigm. In this paper, we propose GRL (GALS Representation Language), a new specification language with textual syntax and formal semantics, targeting systems consisting of a network of distributed synchronous systems (called blocks) that interact with their environments and exchange data asynchronously via communication mediums. The design of GRL has originally been driven by the need of general-purpose, designer-friendly, and formal representation of GALS systems suitable for efficient verification.

Our approach draws mainly from two semantic foundations. As regards synchrony, GRL holds a dataflow-oriented model based on the block-diagram model, widely used in industry: synchronous components are modeled by blocks connected together hierarchically to build higher-level blocks. Therefore, the GRL synchronous model inherits from the simplicity and modularity of the blockdiagram model. As regards asynchrony, GRL was inspired by process algebras, and more particularly by LNT: blocks exchange data by (implicit) rendezvous synchronization with communication mediums connected to other blocks, and the interactions between blocks and their environments work similarly. Thereby, GRL leverages process algebra expressiveness, versatility, and verification efficiency, with a specialization to the GALS paradigm.

GRL was designed with several concerns in mind. First, it provides a sufficiently high abstraction level to fit a wide range of applications, independently from both the target platform (hardware, software, or heterogeneous), the architecture (single or distributed platforms), and the application domain.

Second, GRL is aimed at being a pivot language between industrial design tools (in particular those based on function block diagrams for the synchronous part) and verification tools for both synchronous and asynchronous systems, which guarantee system reliability and correctness. This way, we hope that formal verification methods -claimed traditionally to require high level expertise in theoretical issues -are easier to learn by industrial users, without requiring companies to shift from their actual tools and languages to entirely new production approaches. Indeed, although some approaches seem efficient [START_REF] Girault | Automatic Production of Globally Asynchronous Locally Synchronous Systems[END_REF], the high cost of such a shift makes it unlikely to happen in the near future.

Last but not least, GRL is intended to have a user-friendly syntax as it does not require users to have solid background in neither synchronous programming (e.g., clocks are not modeled explicitly), asynchronous concurrent programming (e.g., parallel composition and synchronization), nor formal verification methods. All features are smoothly and tightly integrated to form a language with homogeneous syntax and semantics.

In this paper, we introduce GRL as a first step towards fully-automated verification of GALS systems. It is organized as follows. Section 2 presents some related work. Section 3 presents the language, its formal semantics, and the current status of software tools. Section 4 gives an illustrative GRL model of an aircraft flight control system used in the avionics industry. Finally, Section 5 summarizes the paper and indicates directions for future work.

Related work

In this section, we review the languages combining synchronous and asynchronous features. CRP [START_REF] Berry | Communicating reactive processes[END_REF] combines the Esterel [START_REF] Berry | The ESTEREL synchronous programming language: design, semantics, implementation[END_REF] synchronous language and the CSP [START_REF] Hoare | Communicating Sequential Processes[END_REF] asynchronous language. Despite its mathematical elegance, CRP is still rarely used in industry since it requires the user to have expertise in both Esterel and CSP. Such expertise is not required for GRL, which was designed to facilitate industrial GALS design. A language close to CRP is SystemJ [START_REF] Malik | SystemJ: A GALS language for system level design[END_REF], which extends Java with Esterel-like synchronous model and CSP-like asynchronous model. SystemJ allows efficient code to be generated automatically. However, it lacks rigorous support for fully-automated formal verification and is not suitable for systems with limited resources because of its reliance on Java virtual machine as target. To the contrary, GRL is intended to be general-purpose and verification-oriented. Action Language [START_REF] Bultan | Action language: A specification language for model checking reactive systems[END_REF] is a state-based approach, which aims at bridging the gap between high specification languages (Statecharts [START_REF] Harel | Statecharts: A visual formalism for complex systems[END_REF], SCR [START_REF] Heitmeyer | Automated consistency checking of requirements specifications[END_REF], and RSML [START_REF] Leveson | Requirements specification for process-control systems[END_REF]) and the SPIN model checker. A key difference between this approach and ours is that Action Language adopts a low-level condition/action model whereas GRL is equipped with high-level control structures making GRL models clearer and more structured.

The GRL Language

The syntax and semantics of GRL are formally described in a research report [START_REF] Jebali | GRL: A Specification Language for Globally Asynchronous Locally Synchronous Systems[END_REF] (76 pages). In this section, we present them briefly and informally. Figure 1 is a simplified presentation1 described in EBNF (Extended Backus-Naur Form), where square brackets denote optional syntactic parts and vertical bars denote alternatives. The symbols K , X , and E denote respectively literal constants, variables, and expressions (built upon constants, variables, and function applications). The symbols S , B , N , M , T , and f denote respectively system, block, environment, medium, type, and record field identifiers.

Overview

GRL specifications are structured in modules, called programs. Each program can import other programs, which promotes code organization and reuse. A GRL program contains the following constructs:

1. types, ranging from predefined types (such as Booleans and naturals) to user-defined types (such as arrays and record types), 2. named constants, visible by all other constructs, 3. blocks, representing the synchronous components, 4. mediums and environments, representing respectively communication mediums and physical or logical constraints on block inputs, and 5. systems, representing the composition and interactions of blocks, environments, and mediums.

In the sequel, these five constructs are called entities, and blocks, environments, and mediums are called actors.

As regards synchronous behaviours, blocks are the synchronous composition of one or several subblocks, all governed by the clock of the highest level block. A block performs a sequence of discrete deterministic steps and preserves an internal state, hereafter called memory. At each step (each cycle of the clock), it consumes a set of inputs, computes a reaction instantaneously, produces a set of outputs, and updates its memory. Within one block (i.e., at actor level ), connections between subblocks are carried out using parameters in modes "in" (input) and "out" (output). Every output parameter can be connected to several system ::= system S [(X0 :T0 , . . . ,Xm :Tm )] is allocate actor0 , . . . ,actorn [temp input parameters of different blocks; however, an input parameter can be connected to only one output parameter of another block. Such connections describe synchronous communication by instantaneous broadcasting. As regards asynchronous behaviours, blocks are composed, together with environments and mediums, within systems to form networks of distributed connected synchronous subsystems. Within a GRL system (i.e., at system level ), the separate blocks execute asynchronously, i.e., each block evolves cyclically at its own frequency (blocks have independent clocks). Blocks interact with each other across mediums, which allows separate blocks to be loosely coupled so that communication is performed asynchronously (i.e., takes an arbitrary amount of time). Connections between blocks and mediums are carried out using parameters in modes "receive" and "send". Receive parameters of mediums can be connected to send parameters of blocks, and conversely. Such connections describe synchronisation and communication by message-passing rendezvous be-Fig. 2: Schematic representation of a GRL system tween blocks and mediums. Mediums may exhibit nondeterministic behaviour, a key feature for asynchronous systems modeling and compositional specification; this provides descriptions with accuracy and high abstraction capability.

X ′ 0 :T ′ 0 , . . . ,X ′ l :T ′ l ] network block call0 , . . . ,block callp [constrainedby env call0 , . . . ,env callq ] [connectedby med call0 , . . . ,med callr ] end system block ::= block B [[const param]][(inout param0 ; . . . ;inout paramm )] [{com param0 ; . . . ; com paramn }] is [allocate sub block0 , . . . ,sub blockp ] [local var0 , . . . ,local var l ] I end block | block B [[const param]][(inout param0 ; . . . ;inout paramm )] is !c string | !lnt string end block env ::= environment N [[const param]][(inout param0 | . . . |inout paramm )] is [allocate sub block0 , . . . ,sub blockn ] [local var0 , . . . ,local var l ] I end environment med ::= medium M [[const param]][{com param0 | . . . |com paramm }] is [allocate sub block0 , . . . ,
= Bi [(arg (0 ,0 ) , . . . ,arg (0 ,m 0 ) ; . . . ;arg (n,0 ) , . . . ,arg (n,mn ) )] | Bi [(arg (0 ,0 ) , . . . ,arg (0 ,m 0 ) ; . . . ;arg (n,0 ) , . . . ,arg (n,mn ) )] [{arg ′ (0 ,0 ) , . . . ,arg ′ (0 ,p 0 ) ; . . . ;arg ′ (q,0 ) , . . . ,arg ′ (p,pq ) }] env call ::= Ni (arg (0 ,0 ) , . . . ,arg (0 ,m 0 ) | . . . |arg (n,0 ) , . . . ,arg (n,mn ) ) med call ::= Mi {arg (0 ,0 ) , . . . ,arg (0 ,m 0 ) | . . . |arg (n,0 ) , . . . ,arg (n,mn ) } signal ::= on [?]X0 , . . . ,[?]Xn -> I I ::= null | X :=E | X [E0 ]:=E1 | X .f :=E | I0 ;I1 | Bi(arg0 , . . . ,argn ) | if E0 then I0 elsif E1 then I1 . . . elsif En then In else In+1 end if | while E loop I0 end loop | for I0 while E by I1 loop I2 end loop | case E is K0 -> I0 | . . . | Kn -> In | [any -> In+1 ] end case | X := any T [where E ] | select I0 [] . . . []In end select | signal
Blocks behaviour can also be constraint-driven by a collection of user-defined environments. In essence, environments exhibit a similar behaviour as mediums, except that their connections to blocks are carried out using modes "in" and "out". They have been introduced in GRL to explicitly separate the specification of communication mediums from external constraints imposed by the environment; this contributes to provide more comfort and insight about the system composition. With such a composition, we seek enhanced user-convenience to smoothly and tightly tailor complex network topologies, environment requirements and constraints, as well as communication protocols.

As an example, GRL can be used to model the network topology depicted in Figure 2: block1 is constrained by env1 and communicates with block2 and block3 respectively across med1 and med2 ; block2 and block3 are both constrained by env2 ; block2 is the synchronous composition of two subblocks.

Block

Blocks, defined by the non-terminal block in Figure 1, are the central building unit of the language. At actor level, a block is defined by the following elements:

a list "const param" of typed constant parameters (read-only variables).

a list "inout param 0 , . . . ,inout param m " of typed input and output parameters preceded by their mode ("in" or "out"). -a list "local var 0 , . . . ,local var l " of local variables. Temporary variables are declared using the keyword "temp"; their values are lost when the current block execution terminates. Permanent variables are declared using the keyword "perm"; their values are kept until the next execution cycle. The memory of the block is the list of values assigned to its permanent variables. -a list "sub block 0 , . . . ,sub block p " of subblock allocations, which enables subblock instances to be created, each maintaining its own memory. This concept is inherited from the block-diagram model, which is similar to, but simpler than, the class-instance paradigm in object-oriented languages. -a body "I " expressed as a deterministic statement defined by combination of high-level control structures (bounded loops, if-then-else, sequential composition, etc.) and synchronous subblock invocations. The scheduling of subblock executions is inherently specified by the order in which the subblocks are invoked, using the sequential composition operator ";". Nondeterministic statements such as "X := any T where E " and "select" (arbitrary choice of one statement among a set) are forbidden within block bodies.

Alternatively, blocks can be specified in an external language. Their body consists of a pragma denoting the language in which the external function implementing the block is written, followed by the name of the function in the external code. So far, the supported external languages are C and LNT: an external function identifier in C (resp. LNT) is preceded by the pragma "!c" (resp. "!lnt"). Although C external blocks provide more flexibility for the user, they should be defined to comply with the GRL block semantics (in particular, side effects in external C code are prohibited to enable model checking). LNT external blocks, however, have formal semantics and can thus be used safely.

In a block invocation, actual parameters have different forms according to their modes. A question mark precedes both output and send actual parameters, meaning that the parameter will have a value assigned when returning from the block. An underscore (" ") is used for unconnected parameters (i.e., unused inputs or outputs). An output parameter X i declared in "out X 0 :T 0 , . . . ,X n :T n " of a block Bi and an input parameter Y j declared in "in Y 0 :T 0 , . . . ,Y m :T m " of a block Bi ′ can thus be connected synchronously using a variable "Z :T i " by passing "?Z " to Bi and "Z " to Bi ′ in a subsequent invocation.

Additional elements can be used to define a block that can only be invoked at system level, namely lists "com param 0 , . . .,com param n " of typed receive and send parameters preceded by their mode "receive" or "send". They enable blocks to interact asynchronously within a network of blocks via mediums. Such a block cannot be allocated nor invoked inside another actor since communication between blocks within actors is necessarily synchronous. At system level, actual input parameters of blocks can have the additional form "any T ", meaning that an arbitrary value of type T is passed as input to the block.

The behaviour of a block is the following. In each cycle of its clock, (1) the block consumes data received over input and receive parameters, (2) the block computes by executing its body, then (3) the block produces data sent over output and send parameters. During computation, its memory is assigned the updated values of permanent variables so as to keep them stored up to the next cycle. As usual in the synchronous paradigm, all these steps are performed in zero-delay, i.e., instantaneously and atomically.

Medium

Mediums, defined by the non-terminal med in Figure 1, are dedicated to the modeling of communications and asynchronous interactions within a network of synchronous blocks. A medium is defined by the following elements:

a list "const param" of constant parameters.

a list "com param 0 , . . . ,com param m " of send and receive parameters.

a list "sub block 0 , . . . ,sub block p " of subblock allocations enabling blocks to be used in mediums in the same way as functions in programming languages. -a list "local var 0 , . . . ,local var l " of local (temporary and permanent) variable declarations. -a body "I " expressed as a statement (not necessarily deterministic) defined as a combination of high-level control structures, subblock compositions, and nondeterministic statements.

A medium sends and receives messages to and from several blocks. When a block wants to send a message to or receive a message from a medium, it triggers the execution of the medium, which we call medium activation. Therefore, the invocation of mediums is demand-driven by different blocks at unpredictable instants. In this respect, mediums are passive actors, whereas blocks are active actors. Each medium is activated during a block execution cycle at most once to send messages to the block, then at most once to receive messages from the block. Since several messages may have to transit via one medium, those messages are grouped in tuples, called channels, all messages of a channel being exchanged within a single block-medium interaction. The channel under consideration is then called activated. The activations of a given medium are thus guided by the separate activations of its channels, as is suggested by the pipe symbol ("|") used to delimit formal and actual channel parameters, each channel activation leading to a separate execution of the medium.

To control medium activations, we introduce signal statements, whose syntax is defined by the non-terminal signal in Figure 1. A signal guards the part of the medium code that needs to be executed upon the activation of a particular channel. When a channel of the form "receive X 0 , . . . ,X n " is activated, the signal statement "on X 0 , . . . ,X n -> I " can be executed and the values of variables X 0 , . . . ,X n passed to the channel can be read within the statement I . When a channel of the form "send Y 0 , . . . ,Y m " is activated, the signal statement "on ?Y 0 , . . . ,?Y m -> I " can be executed and the statement I must assign values to the variables Y 0 , . . . , Y m . Static semantics prohibit sequential composition of signals, loop statements containing signals, and nested signals, so that at most one signal is present on each execution path.

Mediums introduce flexibility in system models since they provide an accurate design of complex network topologies (e.g., bus, star, ring, mesh), connection modes (e.g., point-to-point, multi-point), as well as communication protocols. This way, we address a lack identified in existing languages confined to rigid topologies and point-to-point communications between separate synchronous subsystems, such as those based on CSP rendezvous [START_REF] Malik | SystemJ: A GALS language for system level design[END_REF][START_REF] Berry | Communicating reactive processes[END_REF][START_REF] Doucet | A verification approach for GALS integration of synchronous components[END_REF]. Limita-tions of adopting point-to-point communications in GALS models are considered as drastically restrictive to design complex networks of arbitrary topologies [START_REF] Singh | Generalized latency-insensitive systems for single-clock and multi-clock architectures[END_REF].

Environment

Since synchronous systems are often recognized to be outside-aware, GRL allows the user to model explicitly, yet abstractly, the behaviour of the environment. There are two major roles the environment can play: impose outside physical and logical requirements that block inputs may undergo, and put constraints on the scheduling of blocks executing in parallel. Additionally, an environment may be local, i.e., connected only to one block, or global, i.e., connected to several blocks at the same time. Environments, defined by the non-terminal env in Figure 1, are syntactically and semantically very similar to mediums, except that send and receive parameters are replaced by input and output parameters.

System

Systems, defined by the non-terminal system in Figure 1, are the top level entities in GRL programs, within which actors are invoked and connected to each other. A system is defined by the following elements:

a list "X 0 :T 0 , . . . ,X m :T m " of parameters, which can be used in actual channels to connect blocks to environments and mediums. They are the visible parameters of the system, observable from the outside world. -a list "actor 0 , . . . ,actor n " of actor instance declarations.

a list "X ′ 0 :T ′ 0 , . . . ,X ′ l :T ′ l " of temporary variables, which can be used in actual channels to connect blocks to environments and mediums. They are the invisible parameters of the system, not observable from the outside world.

a list "block call 0 , . . . ,block call p " of block invocations.

a list "env call 0 , . . . ,env call q " of environment invocations that constrain the blocks. -a list "med call 0 , . . . ,med call r " of medium invocations that ensure the traffic inside the network of blocks.

All interactions between actors within a system are built on message-passing synchronisations (rendezvous). Since blocks are the active actors of systems, the scheduling of the whole system is focused around their executions. Blocks execute cyclically, each at its own frequency, and force environments and mediums to perform some operations by sending messages (requesting or providing data) through channels. Environments and mediums, consequently, are passive actors responding to arisen demands from different blocks. At system level, GRL prohibits blocks to be connected directly to each other in order to preserve an independent behaviour of each block and an asynchronous behaviour of the network. Thus, blocks communicate only indirectly across mediums. Each interaction between two actors is performed through exactly one channel. Namely, an output channel of the form "out X 0 :T 0 , . . . ,X n :T n " of an actor Ai and an input channel of the form "in Y 0 :T 0 , . . . ,Y n :T n " of another actor Ai ′ can thus be connected using a set of variables "Z 0 :T 0 , . . . ,Z n :T n " by passing ?Z 0 , . . . , ?Z n to Ai and Z 0 , . . . , Z n to Ai ′ , in their respective invocations within a system. Send and receive channels can be connected similarly.

The semantics of a system are the following. Blocks execute arbitrarily often and cyclically. Each time a block begins its execution cycle, all environments and mediums connected respectively to input and receive channels of the block are activated to provide the needed input and receive values. Unconnected input and receive channels are assigned arbitrary values. Then, the block executes its body, and thus updates its output and send channels as well as its memory. Finally, all environments and mediums connected to respectively output or send channels of the block are activated.

The combined execution cycle of a block, and its related environments and mediums is performed instantaneously according to the synchronous assumptions. As a consequence, a block is executed only if all its connected environments and mediums are able to respond to all input, output, receive, and send signals of the block.

Formal Semantics

The semantics of GRL are formally defined in [START_REF] Jebali | GRL: A Specification Language for Globally Asynchronous Locally Synchronous Systems[END_REF]. They consist in 145 rules of static semantics and 24 rules of Plotkin-style structural operational semantics for the dynamic part. In this paper, we only sketch briefly the principles of the dynamic semantics, defined in terms of LTSs (Labelled Transition Systems). An LTS is a quadruple (S, L, →, s 0 ) where S is a set of states, s 0 ∈ S is the initial state, L is a set of labels, and → ⊆ S × L × S is the labelled transition relation.

The memory of an actor, denoted by µ, is a partial function mapping all permanent variables of the actor and its subblocks to their current values. A state S of the system is the union of memories µ i of all actors composing the system, and the initial state s 0 maps all permanent variables to their initialization values. Each label has the form Bi (a 0 , . . . , a n ){a ′ 0 , . . . , a ′ m } with Bi a block identifier, a 0 , . . . , a n the visible actual parameters of input and output channels, and a ′ 0 , . . . , a ′ m the visible actual parameters of receive and send channels. A transition µ Bi(a0,...,an){a ′ 0 ,...,a ′ m } ---------------→ µ ′ expresses the combined execution of one cycle of the block instance Bi , together with its connected environments and mediums. The semantics of the system are obtained by interleaving all possible block executions. Verification (e.g., visual checking, equivalence checking, model checking) can be done by inspection of the LTS.

Tools for GRL

There are currently two software tools for handling GRL models. The first one is a parser for GRL (2000 lines), developed using the SYNTAX and Lotos NT compiler construction technology [START_REF] Garavel | Compiler Construction Using LOTOS NT[END_REF], which performs lexical and syntax analysis, type checking, binding analysis, and variable initialisation analysis of GRL programs.

The second one, named GRL2LNT (8000 lines), is an automated translator from GRL to LNT. Each block is mapped to an LNT function that takes inputs and produces outputs. Its permanent variables are mapped to inout parameters, i.e., parameters whose values are updated during function invocation. Synchronous block composition is mapped to sequential composition. Additionally, each actor invoked within a system is also mapped to a wrapper process, which contains communication actions to exchange data with its connected actors. The whole system is mapped to the LNT parallel composition of the wrapper processes with appropriate synchronizations of the communication actions.

GRL and GRL2LNT play the role of an intermediate and appropriate layer of abstraction and compositionality to provide generated LNT code with accuracy and conciseness, since scalability of automated model checking is limited. We can take advantage from the CADP toolbox available for LNT to build state spaces and apply visual, equivalence, and model checking techniques.

Example: Flight Control System

Our aim here is not to present a full case study, but rather to illustrate the main concepts of GRL via a feature rich example: the aircraft Flight Control System (FCS)2 , whose role is to control the aircraft turning and which is one of the most critical systems inside new generations of Airbus aircraft designs. Subsets of FCS have been studied at different levels of abstraction. In [START_REF] Miller | Formal verification of flight critical software[END_REF], the Flight Guidance System component of the FCS has been studied as a composition of synchronous systems following a single-platform GALS architecture. In [START_REF] Bae | Definition, semantics, and analysis of multirate synchronous aadl[END_REF], control systems have been studied as synchronous systems following a distributed-platforms PALS (Physically Asynchronous, Locally synchronous) architecture. For the sake of simplicity, we model the global behaviour, at a very high level of abstraction, of an FCS containing the following subsystems:

-Flight Control Surfaces adjust and control the aircraft's flight turning. We consider only one aileron (a flap attached to the end of a wing) controller. -Fly-By-Wire Computers command the movement of the Flight Control Surfaces. We consider only two Fly-By-Wire Computers commanding the position of the aileron, one being used as a backup in case the other fails. -A Flight Control Data Concentrator schedules the execution of Fly-By-Wire Computers and allows interaction with pilot displays.

The GRL model. The FCS system depicted in Figure 3 (see the GRL code below) consists of four block instances, whose cyclic behaviour is as follows:

-The Ail (for aileron) block instance receives movement requirements from the network, computes the next position of the aileron depending on its current position, then sends it to the network. -The Alarmer block instance checks whether the system is evolving safely by receiving from the environment a message indicating whether Ail is still controlled by either Prim or Sec, then informs the pilot about the safety state of the system.

Communications within the network of blocks are modeled by the medium Coord (for coordinator ) as follows. Prim provides Ail with move requirements, then Ail achieves the required computations and sends its new position to Prim. Sec and Ail communicate similarly.

The environment constraints are modeled by two environments. The first environment Conc (for concentrator ) ensures that either Prim or Sec, but not both, can control Ail, the priority being given to Prim by activating its token. Conc determines whether Prim is in a safety state (i.e., able to control Ail ). Once Prim is not in safety state, it is considered out of order (not alive). Then, Conc blocks the execution of Prim by inactivating its token and gives the control of Ail to Sec by activating its token. Once Sec is not in safety state anymore, which means that neither Prim nor Sec is in safety state, then Ail is considered out of control and Alarmer warns the pilot.

The second environment Ctrl (for controller ) constrains the execution of Ail as follows. Ail sends cyclically its new position to Ctrl. Ctrl verifies whether the position is still within a predefined interval, which means that Ail moves smoothly; if not, the execution of Ail is blocked. The GRL specification of the system follows. LTS generation. The GRL model has been translated into an LNT specification using the GRL2LNT tool, yielding a code that is 2.5 times larger than the input GRL model. Using CADP [START_REF] Garavel | CADP 2011: A Toolbox for the Construction and Analysis of Distributed Processes[END_REF], the LTS of the model has been generated (2, 653 states, 7, 406 transitions) then reduced modulo branching bisimulation (5 states, 1, 287 transitions), naturals being represented on 8 bits. This apparently small LTS size can be explained by the following facts. Different states represent different values of permanent variables whereas inputs and outputs only appear on transitions (temporary variables are not stored but only used in intermediate computations). Only variables p ord, s ord, and alarm are visible on the LTS. Other variables (17 inputs and outputs) are hidden and thus do not occur in transition labels. Environment Ctrl constraints the range of possible positions to which Ail can move, thus drastically reducing the LTS. Reduction modulo branching bisimulation also helps in keeping the LTS small.

Conclusion and Future Work

We gave an overview of GRL, a new language with user-friendly syntax and formal semantics for modeling GALS systems, intended to enhance their design process. GRL combines synchronous features of dataflow languages and asynchronous features of process algebras, and makes possible a versatile, modular description of synchronous subsystems, environment constraints, and asynchronous communications. We designed GRL initially as a pivot language intended to facilitate the connection of industrial environments for designing PLCs (Programmable Logic Controllers) to formal verification tools. However, the language appears to be sufficiently expressive and general-purpose to model a wide range of GALS architectures (possibly nondeterministic), implemented on single or distributed platforms, and involving point-to-point or multi-point communications. Moreover, its user-friendly syntax and abstraction level, which is close to the dataflow model used in industry, makes GRL easier to learn and employ than a full-fledged process algebraic language like LNT.

GRL can independently be connected to verification frameworks based on either the synchronous or the asynchronous paradigms. The language is currently equipped with an automated translator to LNT, which makes possible the analysis of GRL descriptions using the rich functionalities of the CADP toolbox (e.g., simulation, verification, performance evaluation), focusing on the asynchronous behaviour of the GALS. GRL and the GRL2LNT translator start to be used in the Bluesky industrial project3 , which addresses the validation of PLC networks. After a positive feedback received from our industrial partners, we are investigating an automated connection between their PLC design software (based on function block diagrams) and GRL, which would provide a complete analysis chain having CADP as verification back-end. We also develop reusable GRL programs describing basic function blocks and mediums corresponding to communication protocols used in PLC networks.

We plan to continue our work by applying equivalence checking and model checking techniques to industrial GALS systems described in GRL. Hardware/software co-simulation is also possible using the EXEC/CAESAR framework [START_REF] Garavel | System design of a CC-NUMA multiprocessor architecture using formal specification, model-checking, co-simulation, and test generation[END_REF] of CADP, which enables the C code generated from a GRL description to be integrated with a physical platform. We also plan to investigate the connection of GRL to verification frameworks based on the synchronous paradigm to analyse the behaviour of individual blocks corresponding to synchronous subsystems.

  sub blockn ] [local var0 , . . . ,local var l ] I end medium const param ::= const X0 :T0 [:= E0 ], . . . ,Xn :Tn [:= En ] inout param ::= (in | out) X0 :T0 [:= E0 ], . . . ,Xn :Tn [:= En ] com param ::= (send | receive) X0 :T0 , . . . ,Xn :Tn local var ::= (perm | temp) X0 :T0 [:= E0 ], . . . ,Xn :Tn [:= En ] sub block ::= B [[arg0 , . . . ,argn ]] as Bi actor ::= B[[arg0 , . . . ,argn ]] as Bi | N [[arg0 , . . . ,argn ]] as Ni | M [[arg0 , . . . ,argn ]] as Mi block call ::

Fig. 1 :

 1 Fig. 1: The syntax of GRL (excerpts)

Fig. 3 :

 3 Fig. 3: Architecture of the Flight Control System

  perm lckBuff :bool := true, upBuff , dwnBuff :bool := false, posBuff :nat := 0 select on p lck , p up, p dwn -> lckBuff := p lck ; upBuff := p up; dwnBuff := p dwn [] on s lck , s up, s dwn -> lckBuff := s lck ; upBuff := s up; dwnBuff := s dwn [] on pos -> posBuff := pos [] on ?p pos -> p pos := posBuff [] on ?s pos -> s pos := posBuff [] on ?lck , ?up, ?dwn -> lck := lckBuff ; up := upBuff ; dwn := dwnBuff end select end medium

70 EBNF productions were necessary to present the full language in[START_REF] Jebali | GRL: A Specification Language for Globally Asynchronous Locally Synchronous Systems[END_REF]

http://www.skybrary.aero/index.php/Flight_Control_Laws

www.minalogic.com

⋆ This work was partly funded by the French Fonds unique interministériel (FUI), Pôle Minalogic (project "Bluesky for I-Automation").


I Molinari
email: irene.molinari@erdw.ethz.ch

J Verbeke

L Boschi

E Kissling

A Morelli

Key Points

X -3

of ambient noise Rayleigh-wave phase-and group-velocity of [START_REF] Verbeke | High-resolution Rayleigh-wave velocity maps of central Europe from a dense ambient noise dataset[END_REF]. We first complement the database of [START_REF] Verbeke | High-resolution Rayleigh-wave velocity maps of central Europe from a dense ambient noise dataset[END_REF] with a dense set of new ambient-noise-based phase-velocity observations. We next conduct a suite of linear least squares inversion of both phase-and group-velocity data, resulting in 2D maps of Rayleigh-wave phase and group velocity at periods between 5 and 37 s. At relatively short periods, these maps clearly reflect the surface geology of the region, e.g. low velocity zones at the Po Plain; at longer periods, deeper structures such as Moho topography under Alps and Apennines, and lower-crust anomalies are revealed. Our phase-and groupvelocity models are next inverted via the Neighbourhood Algorithm to determine a set of one-dimensional shear-velocity models (one per phase/groupvelocity pixel), resulting in a new three-dimensional model of shear velocity (v S ) parameterized in the same way as the European reference crustal model EPcrust [START_REF] Molinari | EPcrust: A reference crustal model for the european plate[END_REF]. We also show how well v S is constrained by phase and group dispersion curves. The model shows the low velocity area beneath the Po Plain and the Molasse basin; the contrast between the low-velocity crust of the Adriatic domain and the high-velocity crust of the Tyrrhenian domain is clearly seen, as well as an almost uniform crystalline crust beneath the Alpine belt. Our results are discussed from the geological/geodynamical standpoint, and compared to those of other, interdisciplinary studies.

Introduction

Detailed maps of the seismic structure of the crust are valuable because they reflect the effects of past and present tectonic processes, and because crustal structure must be known if seismic data are used to image deeper, mantle structure or to constrain the parameters that define seismic events. Seismic observations are very sensitive to crustal structure, but are often unable to image it unambiguously. In particular, teleseismic observations are affected by seismic velocities and depth of discontinuities within the lithosphere, in particular the Moho, but it is hard to separate crust and mantle effects by analyzing teleseismic data alone. As a consequence, seismic tomography studies often rely on a priori descriptions of crustal structure, not necessarily based on direct observation [e.g. [START_REF] Arlitt | Three-dimensional crustal structure beneath the TRO array and effects on tele-seismic wavefronts[END_REF]Auer , 2014, and references therein]. An inaccurate crustal model may significantly reduce the accuracy of mantle imaging [e.g. [START_REF] Bozdag | On crustal corrections in surface wave tomography[END_REF], and our knowledge of the long-wavelength seismic structure of the crust is still, in many instances, unsatisfactory.

The Alpine and Apennines mountain ranges have been the subject of countless geological and geophysical studies for the last two centuries at least [e.g. [START_REF] Doglioni | The Western Mediterranean extensional basins and the Alpine orogen[END_REF]Handy et al., 2014, and references therein]. Owing to the mentioned difficulties in crustal imaging, a number of fundamental questions are still open concerning orogeny and mantle dynamics in this complex area [START_REF] Faccenna | Shaping mobile belt from small scale convection[END_REF]. Local-scale crustal models have been derived from geological datasets [Molinari et al., 2015], active reflection and refraction seismic experiments [e.g., [START_REF] Waldhauser | Three-dimensional interface modelling with two-dimensional seismic data: the alpine crust-mantle boundary[END_REF][START_REF] Brückl | Crustal structure due to collisional and escape tectonics in the Eastern Alps region based on profiles Alp01 and Alp02 from the ALP 2002 seismic experiment[END_REF], P-wave travel-time tomography [e.g., [START_REF] Chiarabba | Crustal velocity structure of the Apennines (Italy) from P-wave travel time tomography[END_REF][START_REF] Piromallo | P wave tomography of the mantle under the Alpine-Mediterranean areas[END_REF]; D R A F T November 11, 2015, 9:13pm D R A F T X -5 [START_REF] Serretti | Seismic rays and traveltime tomography of strongly heterogeneous mantle structure: application to the central mediterranean[END_REF][START_REF] Gualtieri | Finite-difference p wave travel time seismic tomography of the crust and uppermost mantle in the Italian region[END_REF], local earthquake tomography (LET)

[e.g., [START_REF] Diehl | High-resolution 3-D P-wave model of the alpine crust[END_REF][START_REF] Di Stefano | Shallow subduction beneath Italy: Three-dimensional images of the Adriatic-European-Tyrrhenian lithosphere system based on high-quality P wave arrival times[END_REF], receiver-function studies [e.g., Piana

Agostinetti and Amato, 2009], and combinations of the latter two data types [START_REF] Wagner | Combining controlled-source seismology and local earthquake tomography to derive a 3-D crustal model of the western Alpine region[END_REF][START_REF] Spada | Combining controlled-source seismology and receiver function information to derive 3-D Moho topography for Italy[END_REF]. These methods provide important constraints on threedimensional (3D) P-wave velocity structure and on the depth of sharp discontinuities.

However, they all have intrinsic limitations: the scarcity of seismic events in large regions prevents LET to be applied at a regional scale; observations of receiver functions are limited to station locations and thus relatively sparse; active seismic experiments need 3D migration [START_REF] Waldhauser | Three-dimensional interface modelling with two-dimensional seismic data: the alpine crust-mantle boundary[END_REF]]. Hence, these techniques cannot be easily applied at large scales. Even more importantly, none of them constrains S-wave velocity (v S )

directly. Some studies have combined information from different methods, to determine larger-scale crustal models [e.g., [START_REF] Tesauro | EuCRUST-07: a new reference model for the European crust[END_REF][START_REF] Grad | The Moho depth map of the European Plate[END_REF][START_REF] Baranov | A new crustal model for central and southern Asia[END_REF][START_REF] Molinari | EPcrust: A reference crustal model for the european plate[END_REF]Molinari et al., 2012]. This approach requires some subjective assumptions: for instance, information from distantly neighbouring refraction profiles could be interpolated on the base for instance of gravity data, and v S could be derived by scaling P-wave velocity (v P ) using some standard relations. and depth of the deep Po-plain sedimentary basin has been determined from geological data [Molinari et al., 2015].

In this study, we derived the 3D crustal structure (S wave velocity) underneath Italy and the Alpine region, expanding and exploiting the database of [START_REF] Verbeke | High-resolution Rayleigh-wave velocity maps of central Europe from a dense ambient noise dataset[END_REF]. We first derive new maps of fundamental-mode Rayleigh-wave group-and phase-velocity, making use of phase-velocity observations that were not available to [START_REF] Verbeke | High-resolution Rayleigh-wave velocity maps of central Europe from a dense ambient noise dataset[END_REF], and enhancing lateral resolution significantly. The study of [START_REF] Verbeke | High-resolution Rayleigh-wave velocity maps of central Europe from a dense ambient noise dataset[END_REF] was limited to phase-and group-velocity maps; here we infer 3D v S structure using a fully nonlinear direct-search inversion algorithm [Wathelet, 2008]. This method allows for a priori information other than seismic dispersion curves to be taken into account in the inversion:

we thus combine ambient-noise surface-wave data with the above-mentioned, independent observations of discontinuity depths, which surface waves are only weakly sensitive to; in practice, the resulting 3D map can be seen as a model integrating information on receiver functions and surface wave.

In the following, we first describe the linear tomographic inversion that provides phaseand group-velocity maps; we next illustrate the results of the nonlinear inversion for v S , including an assessment of uncertainties; finally, we discuss our results from the geological/geodynamical standpoint, and compare them to those of other, interdisciplinary studies.

2. Rayleigh-wave phase velocity maps from ambient noise belonging to the Italian, Swiss and German permanent broadband networks (Fig. 1). For each station pair, surface-wave group velocities have been measured applying the time frequency analysis (FTAN) method [START_REF] Ritzwoller | Eurasian surface wave tomography: Group velocities[END_REF], while phase velocities have been obtained following the two-station method as implemented by [START_REF] Meier | One-dimensional models of shear wave velocity for the eastern Mediterranean obtained from the inversion of Rayleigh wave phase velocities and tectonic implications[END_REF]. The accuracy of phase-velocity measurements was verified by [START_REF] Boschi | On measuring surface-wave phase velocity from station-station cross-correlation of ambient signal[END_REF],

who validated the method used by [START_REF] Verbeke | High-resolution Rayleigh-wave velocity maps of central Europe from a dense ambient noise dataset[END_REF] against an independent approach based on frequency-domain cross-correlation.

Our database is based on that of [START_REF] Verbeke | High-resolution Rayleigh-wave velocity maps of central Europe from a dense ambient noise dataset[END_REF]. With respect to the work of [START_REF] Verbeke | High-resolution Rayleigh-wave velocity maps of central Europe from a dense ambient noise dataset[END_REF], group-velocity data are exactly the same, while phase-velocity dispersion curves have been entirely recomputed from the original cross-correlations, to include phase-velocity measurements made at a denser and broader set of frequencies as illustrated in the following. With respect to group velocity, phase-velocity data sample a wider depth range and are less contaminated by interfering phases, because measurements are made within a narrrower time window [e.g. [START_REF] Boschi | On measuring surface-wave phase velocity from station-station cross-correlation of ambient signal[END_REF]. On the other hand, group velocities are more sensitive to relatively shallow depth and are easier to measure.

We take advantage of both data types to constrain 3D crustal structure at the highest possible resolution. After measuring dispersion as described between all available station pairs (Fig. 1), we derive phase-velocity maps between 5 and 37 seconds periods and group-velocity maps from 8 to 35 seconds.

Phase-and group-velocity imaging method

Assuming, as is done in most seismic ambient-noise literature, that the effects of nonuniformity in noise source distribution can be neglected, an ambient-noise database is

D R A F T November 11, 2015, 9:13pm D R A F T X -9
equivalent to a "traditional" one, with earthquake sources replaced by seismic stations acting as "virtual" sources [START_REF] Boschi | Stationary-phase integrals in the cross correlation of ambient noise[END_REF]. We set up a linear system in the ray-theory approximation as described e.g. by [START_REF] Boschi | High-and low-resolution images of the Earth's mantle: implications of different approaches to tomographic modeling[END_REF]. Based on the available ray coverage, we parameterize the region of interest in terms of 0.25 • × 0.25 • cells, independent of period and for both phase-and group-velocity. We take the phase-and group-velocities predicted by PREM [START_REF] Dziewonski | Preliminary reference Earth model[END_REF],

period-dependent but laterally homogeneous, as reference values, and determine phaseand group-velocities through a suite of least-squares inversions (one per period for both group and phase data) via the iterative LSQR algorithm [START_REF] Paige | LSQR: an algorithm for sparse linear equations and sparse least squares[END_REF].

LSQR approximates the exact least square solution, converging, according to a rigorous "stopping criterion" [START_REF] Paige | LSQR: an algorithm for sparse linear equations and sparse least squares[END_REF], after some tens of iterations. In order to obtain a stable solution, we regularize the inverse problem via the roughness minimization scheme of [START_REF] Boschi | High-and low-resolution images of the Earth's mantle: implications of different approaches to tomographic modeling[END_REF], which is equivalent to requiring the solution model to be smooth. We do not apply norm minimization because, in cases of nonuniform data coverage, this form of regularization can result in solution models with unnaturally large velocity gradients Boschi and Dziewonski [e.g. 1999]. We carry out many tentative inversions with different regularization parameter values until a satisfactory solution is achieved, i.e.: (i) variance reduction of the data is relatively high; (ii) using resolution tests (sec. 2.2) as a reference, we verify that there are practically no features in our maps at wavelengths shorter than our target resolution. We verified that solutions found in this way correspond to the corner region of the L-curve as defined by [START_REF] Hansen | Analysis of discrete ill-posed problems by means of the l-curve[END_REF] and shown in Fig. 2: the roughness damping value is 0.75 for both phase and group velocity and for all periods. As can be expected, variance reduction changes as a function of surface-wave

D R A F T November 11, 2015, 9:13pm D R A F T period.
Highest variance reductions (up to ∼ 75%) of both group and phase data are achieved in the 8-25 s period range; at periods <8 s and >25 s variance reduction does not exceed 50%.

Resolution test

We quantify the horizontal resolution of phase-and group-velocity allowed by our dispersion data sets via synthetic tests [e.g., [START_REF] Boschi | High-and low-resolution images of the Earth's mantle: implications of different approaches to tomographic modeling[END_REF]. Following [START_REF] Husen | The effects of data quality in local earthquake tomography: Application to the Alpine region[END_REF] and [START_REF] Verbeke | High-resolution Rayleigh-wave velocity maps of central Europe from a dense ambient noise dataset[END_REF], we choose as "input" model a random 2D map of velocity anomalies (Fig. 3) whose size and distribution is statistically similar to typical seismic maps at this scale length. This is preferable to unrealistic though widely used "checkerboard" input models who tend to yield too optimistic estimates.

The input model of Fig. 3 is characterized by anomaly values ranging between -10% and +10% with respect to PREM [START_REF] Dziewonski | Preliminary reference Earth model[END_REF], filtered via 2D Fourier transformation to isolate the wavelengths of interest, resulting in anomalies of spatial extension > 50 km and < 200 km. We calculate phase and group delay times predicted by this model for all ray paths and periods in our database (station coverage depends on period and on whether phase or group velocity is measured); we add Gaussian noise to the data (the standard deviation of random noise is the same as that of the data, σ = 0.2km/s). Finally, we solve the two inverse problems -for phase and group velocities -using the inversion algorithm and regularization scheme and parameters that we apply to our real data set. The results associated with 7, 12 and 20 s Rayleigh-wave phase velocity data and with 8, 16, 24s group velocity data are shown in Fig. 3. We only show our solution in cells sampled by more than 5 rays, estimating that less well sampled pixels might not be sufficiently well constrained. As a general rule, the test model is recovered

D R A F T November 11, 2015, 9:13pm D R A F T X -11
fairly well, within the resolved area, independently of period; group velocity, for which we have a denser ray coverage (see maps in Figure 3), is recovered more accurately than phase velocity; amplitude of both phase-and group-velocity anomalies is underestimated. At short periods (up to 14 seconds), phase velocity is resolved well in Switzerland, Southern

Germany, Western and Eastern Alps and North-Western Apennines; at longer periods phase-velocity resolution becomes acceptable also in North-Eastern, Central and Southern

Italy. Group-velocity resolution is fairly good throughout the region of interest, with the exception of Western Tyrrhenian Sea, Sardinia, Corsica and Southern Adriatic sea.

We anticipate that, as a consequence, the resolution of our final 3D model changes as a function of location (and not only in depth, due to differences of depth sensitivity for phase and group velocity at each period, see Section 2.3): in areas where short period surface-wave velocity is not constrained by either group or phase dispersion observation, shallow crustal structure is underconstrained (see Section 3.2).

Rayleigh-wave phase-and group-velocity maps

We show in Fig. 4 the phase and group velocity maps obtained from our data sets at periods between 5s and 37s, and 8s and 35s, respectively. Long-period surface waves sample deeper into the Earth and are correspondingly characterized by higher velocities than short-period ones, as noted in Fig. 4. As a first order approximation, surface waves of 7s image structure from surface down to 10 km depth, those of 20s period are most sensitive to structure between 10km and 30km, and those of 37s period between 35km and 55km depth [Warren et al., 2013]. At any given period, group velocity is sensitive to structure at shallower depth than phase velocity.

Inversion for 3D structure

At each cell of our phase-/group-velocity maps, we construct fundamental-mode Rayleigh-wave dispersion curves, ranging from 5 to 37 s period in phase velocity, and 8 to 35 s in group. We subsequently invert each combination of phase-and group-velocity dispersion curves, to determine isotropic v S , v P and layer thicknesses. Each inversion consists of a stochastic direct search, implemented via the "Neighbourhood Algorithm" [Sambridge, 1999a;Wathelet, 2008]. In this approach, the solution space is sampled sequentially and non-uniformly, taking into account the data fit achieved by old samples when generating new ones: in practice, while possible solutions are sought randomly, the search is biased towards regions of the solution space were better-fitting solutions have been found [Wathelet, 2008]. The cost function is the L2-norm of the difference between the observed dispersion curves, and those calculated from a solution model.

This approach is suited to the inverse problem under consideration because of its inher- Outside the Po Plain, we allow the top-layer thickness to vary between 1-5 km. The exact variability range of each parameter is given in Table 1.

Each inversion consists of a nested exploration of the solution space, carried out in 140 steps; at each step, the 110 best-fitting solutions are kept. In summary, 35,400 possible solution models are evaluated at each cell. In Fig. 5, the best-fitting 15,400 models are plotted for a few sample cells, illustrating the range of possible models sampled by the inversion, and the goodness of fit they achieve. The similarity between best and mean models in Fig. 5 reflects the velocity resolution afforded by our database: the solution is generally robust (similar to the mean) except for the first few kilometers, and for the top of the mantle.

We run our algorithm once for each of the 0.25 • × 0.25 • pixels of our dispersion maps.

The root mean square (RMS) of the misfit is shown, as a function of period, in Fig. 6, where we compare the fit achieved by crustal models EPcrust and CRUST2.0 [START_REF] Bassin | The current limits of resolution for surface wave tomography in North America[END_REF] and by our final best model. We infer from Fig. 6 that inversion improves data fit significantly with respect to existing regional models. CRUST2.0 (i) are continental-/global-scale models, not designed to be employed at the scale of this study, and (ii) they were derived from observations independent of surface waves (whether earthquake or noise-generated). The fact that EPcrust and CRUST2.0 reduce the variance of our ambient-noise data at most periods is a nontrivial result, and a significant validation of those models. Our final best-fitting model ultimately accounts for a broad variety of data; it strongly improves the fit of surface-wave dispersion observations and additionally accounts for apriori knowledge of crustal structure derived by other independent methods; it is overall an important upgrade of EPcrust, in particular as far as v S structure is concerned.

Local velocity profiles

In Fig. 5 we select examples of nonlinear v S inversions involving a diverse set of geological settings. Our group-and phase-velocity data, combined with the mentioned a priori information on the depth of the main sedimentary basins and, in particular, of the Moho depth, allow us to map v S crustal structure with higher resolution than previously possible. The lack or poor quality of data at very short periods (<5s) may lead to near-surface velocities that are poorly correlated with geology, but this effect is marginal,

D R A F T November 11, 2015, 9:13pm D R A F T X -17
owing in particular to the careful a-priori constraint introduced in our inversion strategy as explained above.

We noted that both phase-and group-velocity data are generally well explained by our model. In areas where crustal structure is particularly complex (e.g., deep sedimentary basins, Moho offsets at plate boundaries), the data fit is occasionally poor: the problem might be solved by means of a local, ad-hoc, finer parameterization, but this would be extremely time-consuming and is beyond the scope of this study. of European lithosphere outside the orogenic belts. We find here a crustal thickness of about 25km, with an almost uniform upper crust and a large velocity gradient in the lower crust. The Moho appears to be relatively shallow, but a closer look at Fig. 5b shows that many solution models exist that fit the data about equally well.

In the Alpine orogen cell (Fig. 5c) our model is characterized by a relatively high near-surface velocity of about 3.15km/s reflecting the granitic basement rocks exposed at surface after intensive uplift and erosion. The Moho is more than 50km-deep [START_REF] Schmid | The arc of the Western Alps in the light of geophysical data on deep crustal structure[END_REF], near the lower limit or resolution by our data. That the Moho is anomalously deep could be directly inferred from the phase-velocity dispersion curve, where the kink typically associated to Moho depth [START_REF] Lebedev | Mapping the Moho with seismic surface waves: A review, resolution analysis, and recommended inversion strategies[END_REF] is not found, presumably because it takes place at longer periods, outside our measurement range.

The south-west Alpine foreland cell (Fig. 5d) is located at the Southern edge of the Ivrea Body [START_REF] Solarino | Local earthquake tomography of the southern part of the Ivrea body, North-Western Italy[END_REF], and shows very low surface velocity of about 2.3km/s and velocities of about 3.4km/s in the whole crust, in good agreement with known near-D R A F T November 11, 2015, 9:13pm D R A F T surface structure. Imaged Moho depth is relatively shallow (20km), corresponding to the Ivrea mantle upwelling [START_REF] Spada | Combining controlled-source seismology and receiver function information to derive 3-D Moho topography for Italy[END_REF].

In the Po Plain, along the Adriatic coast (Fig. 5e), Tertiary and Mesozoic sediments reach 7-km thickness [Molinari et al., 2015]. Their effect is visible in the corresponding dispersion curves up to 25-30s period; group velocity is particularly low, i.e. ∼2 km/s at period < 15 s. We emphasize that, in this anomalous location, our a priori definition of the solution space plays a particularly important role: we have only explored solution models that included a thick sediment layer. Preliminary inversions had shown that, in the absence of such constraint, group-and phase-velocity anomalies would have been explained in terms of very low v S throughout the crust. Despite that, a broad range of plausible solution models are shown in Fig. 5e, suggesting that this remains a relatively poorly constrained location that could benefit from further seismic observations of all kinds. Besides the thick sediment layer, our best profile at this location includes upper crustal basement rocks of cumulative thickness > 15km, overlying rather average Adriatic lower crust.

The last cell is representative of the Tyrrhenian crust (Fig. 5f). At this location the Moho is relatively deep (∼ 25 km); the upper crust is characterized by a strong velocity gradient; the middle-lower crust is approximately uniform.

Model variability

Before discussing 3D v S variations, we evaluate how robustly they are constrained by our procedure. Non-linear, direct-search inversion techniques -such as the Neighbourhood Algorithm used here -allow the exploration of the model space, guided by explicit a priori informations that designate physically plausible models on the basis of supple-

D R A F T November 11, 2015, 9:13pm D R A F T X -19
mentary data. This approach can thus provide an assessment of the range of 'possible' models -i.e. those that reach an acceptable fit to observations -in a more general fashion than linearised standard error analyses. While a rigorous model appraisal, geared for accurately picturing posterior probability density functions in a Bayesian sense, may often be an expensive task [START_REF] Sambridge | Geophysical inversion with a Neighbourhood Algorithm -II. Appraising the ensemble[END_REF], the suite of models tested during the search stage provides a fair picture of model uncertainty. Our non-linear search technique [Sambridge, 1999a;Wathelet, 2008] generates an ensemble of acceptable models that may be taken to represent the posterior probability distribution function (PDF) of the earth structure reflected by the observations. We limit our estimation of model variability to this approximate PDF representation.

The marginal velocity probability density distribution of a single model parameter (i.e., shear-wave velocity at some particular depth in vertical v S profile) appears well behaved, not far from a Gaussian. This can be verified in Fig. 7, that shows the distribution of v S values at three fixed depths for a sample geographical location (cell e) in Fig. 5). The a priori PDFs -in each case, a boxcar representing a range of variability with uniform probability density -is also plotted, showing that significant improvement to fit local Rayleigh phase and group dispersion curves. We recall that the quality of fit of the dispersion maps to observed data is depicted by Figure 6 showing the geographical variation of global RMS misfit.

S-wave velocity structure

The maps of v S anomalies associated with our best-fitting model are shown in Fig. 8.

At each depth, the solution model is only shown in cells that are sampled by at least 5 ray paths for which both phase and group velocity measurements have been successfully obtained at 16s period. We conservatively estimate that less well sampled cells are not sufficiently robustly constrained. The well resolved cells at each depth depends on the surface wave velocity coverage (Figure 3), at periods whose sensitivity is maximum at that depth (Warren et al.

[2013], Fig. 7b). As discussed in the previous section, we do not have sufficient resolution to resolve the structure of shallow sedimentary layers, which are therefore controlled, in our inversions, by a priori constraints provided by geological models.

D R A F T November 11, 2015, 9:13pm D R A F T

X -21

The 3-km deep section in Fig. 8 shows the uppermost part of the crust including the sediment layer. The Po basin and the Ligurian-Sea basin are the most prominent features of this image. The a-priori v S variability range is from 1.2 to 3.2 km/s and the inversion results show a v S ≈ 2 km/s, in good agreement with Molinari et al. [2015].

The deeper part of the Molasse basin is also well marked and shows a higher velocity(2.5 Apennines can be caused by "smearing" in depth of the low surface wave velocity anomaly from 5 to 20 seconds (Fig. 4). Within each domain, v S does not show strong 3D variations but highlights the difference in composition (and in origin) of Alpine and Apennines upper crust. In the southern Tyrrhenian, the crust is oceanic, the Moho depth is known to be about 10-15 km depth and low S-wave velocity values found at 10 km depth is consistent with a large percentage of partial melting and high temperature.

D R A F T November 11, 2015, 9:13pm D R A F T
The 20-km deep section shows the lower crust, both in the Tyrrhenian and Adriatic domain, and the upper mantle in the Tyrrhenian sea (v S ∼ 4.0 km/s). Alps and Apennines

show up very clearly in our imaged structure. Beneath southern Germany and northeastern Italy, v S is as high as 3.6-3.9 km/s. Moreover the contrast between relatively high v S under the Tuscan Apennines and low v S under the Marche region is in agreement with new interpretations based on the CROP03 profile [START_REF] Pauselli | The crustal structure of the Northern Apennines (Central Italy): an insight by the CROP03 seismic line[END_REF], which samples that area. Ligurian upper mantle is visible as high shear-speed beneath the South-Wester

Alps and western-most part of the Po Plain.

At 35km depth, the geographic pattern of v S heterogeneity is correlated with that of Moho topography. v S values typical of the lower crust (3.6 -3.9 km/s) are still found along the Alpine belt and the Northern and Central Apennines; besides that, v S is within the range of typical upper mantle values. However, with respect to their surrounding areas, Central Apennines have relatively low v S , i.e. between 3.2-3.5 km/s; this confirms published observations of anomalously low lower-crust v P ≈ 5.8 km/s in this region, and thus the requirement of anomalously high lower-crust temperature, given the granitic composition [START_REF] Chiarabba | Crustal velocity structure of the Apennines (Italy) from P-wave travel time tomography[END_REF][START_REF] Chiarabba | Deep geometry and rheology of an orogenic wedge developing above a continental subduction zone: Seismological evidence from the northern-central Apennines (Italy)[END_REF][START_REF] Di Stefano | Shallow subduction beneath Italy: Three-dimensional images of the Adriatic-European-Tyrrhenian lithosphere system based on high-quality P wave arrival times[END_REF].

Structure at larger depth (> 50 km) is not resolved well by our dataset. Our dataset does not allow to resolve the complex geometry of subduction zones, which should be discussed in future work involving longer-period surface-wave and/or body-wave travel-time data.

Our inversion provides also an updated Moho map since we allow crustal layer thickness to vary up to 10 % with respect to the total crustal depth from the Moho of Spada et al. [START_REF] Hunziker | Lower Paleozoic amphibolite to granulite facies metamorphism in the Ivrea Zone (Southern Alps, Northern Italy)[END_REF][START_REF] Rivalenti | The origin of the Ivrea-Verbano basic formation (Western Alps) -Whole rock geochemistry[END_REF]. This feature is present in all the three works at Within the crust, the sediments and upper and lower crustal domain are clearly marked.

The Po plain is a prominent feature; as explained above, the a priori model in this area is characterized a thicker-than-average sediment-layer thickness, which compensates the lack of short-period data; v S is, however, a free parameter of the inversion (see Table 1

Conclusions

We have derived a new 3D v S model that fits surface wave group and phase dispersion curves between 5 and 37 s. Virtually all other relevant data on the Italian and Alpine crust at the scale length of interest have been accounted for, in the form of an a-priori model.

Especially at high frequency, our model leads to a significant reduction of surface-wave data variance, with respect to some recent crustal models. We found that, at periods between ∼20 and ∼40s, both EPcrust and Crust2.0 fit our ambient-noise data fairly well, with the higher-resolution model EPcrust achieving a systematically better fit. The fact that EPcrust fits a data set that was not employed in its derivation is an important proof of its reliability.

To obtain our model, we have first inverted the database of [START_REF] Verbeke | High-resolution Rayleigh-wave velocity maps of central Europe from a dense ambient noise dataset[END_REF], to find Rayleigh-wave fundamental-mode phase-and group-velocity maps at periods from 5 to 37 s, and from 8 to 35 s, respectively. We have then applied a direct-search method Our final preferred model consists of three layers (sediments, upper crystalline and lower crust); within each layer, the seismic parameters are described with a linear gradient. This model is suited to many applications, such as wave propagation modelling at regional scale, crustal correction in tomography, gravity studies, dynamic topography inference.

Relatively poor data fit at periods below 10s suggests that the shallowest part of the crust, i.e. the sediment layer, is not as robustly constrained by the data as the deeper structure. Lack of resolution in shallow layers could result in trade-off and thus loss of model quality for deeper structure. In a future study, the European Plate reference crustal model may be further improved by (i) replacing its current sediment information with more detailed sediment models, and (ii) replacing its current Moho map with one of the new generation of Moho maps. In particular the sediment layers could be obtained by the integration of other sources of information, such as seismic reflection/refraction profiles, geological maps, borehole data will lead to a better definition of the shallowest properties and discontinuities within the crust.

Acknowledgments.

D

  R A F T November 11, 2015, 9:13pm D R A F TThe longer wavelength patterns of the maps in Fig.4are in agreement with the lowerresolution maps of[START_REF] Verbeke | High-resolution Rayleigh-wave velocity maps of central Europe from a dense ambient noise dataset[END_REF]. At short periods we clearly recognize the effects of shallower geological features. Low-velocity anomalies (∼2.3 km/s for phase and < 1.5 km/s for group velocity) can be associated to sedimentary basins in the Po plain, known to be characterized by a low seismic velocity foredeep sedimentary basin that reaches a depth of 7-8 km and to a lesser degree in the Swiss and German Molasse basin (visible especially well in the 8s group velocity map). As expected for shallow crustal levels, the Alpine belt exhibits higher velocities than the Apennines, indicating the presence of shallow high-velocity crystalline structure in the Alps. At intermediate periods (12s for phase and 16s for group velocity) the signature of the Po Plain is still clearly visible, suggesting that deep and slow sedimentary basins affect the dispersion curves at longer periods more than estimated by theoretical maximum sensitivity. This means that, in order to get a realistic velocity 3D model in this region, we need to constrain those basins with a good a priori model. Using a finer parameterization grid, we recover the Ivrea body high-velocity zone at lon ∼ 8 • and lat ∼ 44.5 • (Figure 3). Lower phase and group velocities are found along the Apennines than along the Alps, presumably owing to the different properties of rocks forming the uppermost part of the crust under those two mountain ranges: the Apennines are predominantly characterized by Adriatic consolidated sediments with a low degree of metamorphism, as opposed to relatively high-velocity crystalline upper-crustal and metamorphic basement rocks under the Alps. High velocities appear mainly over the Tyrrhenian Sea, as a result of the shallow Moho depth in this oceanic region. D R A F T November 11, 2015, 9:13pm D R A F T X -13 Longer periods (20s and 32s for phase; 24s and 35s for group velocity) are most sensitive to lateral variations of lower crust, Moho depth and uppermost mantle, depending on location. The contrast between Tyrrhenian and Adriatic crust is strong (about 0.3-0.4 km/s), but this effect is explained to a large extent in terms of Moho depth, the Tyrrhenian crust being anomalously thin with respect to the rest of the region of interest. At periods > 30s, we can clearly distinguish the deep crustal root along the inner parts of the Alpine orogen and beneath the Apennines, and the low-velocity anomaly proposed by Di Stefano et al. [2009] as the "Central Apennine" window, based on P-wave travel-time tomography.

  ent nonlinearity. It has the advantage of widely exploring the admissible solution space, without anchoring the solution model to the reference one as would happen in a linearised D R A F T November 11, 2015, 9:13pm D R A F T inversion. However, the strong nonlinearity of the problem and the averaging properties of the dispersion measurements can always result in significantly biased solutions, especially in combination with deep sedimentary basins or wherever particularly strong velocity discontinuities are present. Naturally, where data coverage is poor, nonlinear inversion can result in strong depth variations clearly incompatible with known geological features [Saygin and Kennett, 2012]. As mentioned above, the main weakness of surface-wave inversion is the lack of sensitivity to the depth of seismic interfaces. Following Wathelet [2008], we therefore define the boundaries of the solution space to be sampled (i.e. the range of possible values for all parameters we invert for), on the basis of a priori information from independent geophysical and geological data. A priori constraints on the model search are important to speed up the inversion by limiting the volume of model space searched and to define what we judge to be physically plausible candidate models. The vertical parametrization of our 3D models is the same as that of EPcrust, including three crustal layers plus two 25-km thick mantle layers. The three crustal layers are defined as the following: a top layer which can be either sediment in the sedimentary basins (Po Plain, Molasse basin and Ligurian Sea basin), a stack of sedimentary thrust sheets in i.e Apennines or upper-most crustal like material; a middle layer corresponding to the crystalline upper crust; a lower layer corresponding to the lower crust. v S in each layer is described with a linear gradient, obtained by subdividing each layer into five sublayers. The water layer is not taken into account: this simplification, inherent limit of our inversion software, might cause biased results under Tyrrhenian Sea. Since our study is focused on continental structure, we think it is reasonable to "neglect" this layer for the time being. The allowed parameter ranges in each layer are defined based on the most D R A F T November 11, 2015, 9:13pm D R A F T X -15 recent crustal models and Moho maps of the region of interest. Upper-and lower-crustal parameters (especially v P and density) should be in the same range as EPcrust values;velocities in the mantle should be similar to EPmantle values; Moho depths are required to be close to those given by[START_REF] Spada | Combining controlled-source seismology and receiver function information to derive 3-D Moho topography for Italy[END_REF]; in the Po Plain, sediment-layer thickness and velocity should resemble those provided by the MAMBo model[Molinari et al., 2015].

Fig. 6c shows

  Fig.6cshows the geographical distribution of model misfit. The misfit is highest

Fig. 5b corresponds

  Fig. 5b corresponds to the Northern border of the Molasses basin, and is representative

  Fig. 7 b), c), and d), we plot maps of the standard deviation at three sample depths. We

  km/s) than Po basin highlighting the different evolution of the two Alpine foreland basins . The Alps and Apennines shallow velocities appear to be consistent with the current surface geology knowledge: high v S in the Alps indicating the presence of crystalline and metamorphic rocks and consolidated sediment. The Tyrrhenian back-arc basins, that has started forming in the late Miocene, is partially imaged by our tomography and shows v S around 2.4 km/s. The 10-km deep section in Fig. 8 shows a strong variability in the upper crust: distinct difference between the Alp and its Northern foreland with a uniform v S of about 3.2 km/s while South of Alps a the same depth we find the various lithologies from the deep Po Basin sediments (v S ≈ 2.8 km/s) to uppermost crystalline crust in central Apennines (≈ 3.0 km/s). The low v S values corresponding to the Po Plain and the North and Central

[

  2013]. The allowed variation is roughly within the error bar specified in the a-priori Moho. Although surface waves are only marginally sensitive to sharp discontinuities, D R A F T November 11, 2015, 9:13pm D R A F T X -23 some adjustments with respect to the a-priori Moho are expected. We show in Fig. 9 the comparison between the map of Moho depth resulting from our inversion, the EPcrcust one, and the one obtained by Spada et al. [2013] via a combination of CSS, LET and RF. Our inversion and our dataset result in Moho depths from 10 to nearly 60 km, with the highest values found along the entire Alpine arc and locally beneath the Northern Apennines. These depth estimates are generally higher than those of EPcrust (Fig. 9-b), and in better agreement with those of Gualtieri et al. [2014]. The boundary between the Adriatic and Tyrrhenian tectonic domains appears to be defined well, with an average Moho depth of about 35-40 km in the former and about 20-30 km in the latter. Crustal thickness grows from East to West across the Western Alps. The inversion of ambientnoise data has "sharpened" the Alpine Moho with respect to EPcrust, shifting it to an overall larger depth; in the Po Plain area and throughout Adria, our final Moho appears closer to that of EPcrust. Finally, the imaged thin Ligurian crust is similar to the results of Spada et al. [2013]. Vertical sections (Fig. 10) of our final model reveal several prominent tectonic and geological features. These sections provide an overall view on the crustal structure and highlight the different crustal domains present in this complex region. Our model sections are not smoothed in order to well identify parameterization and to not over-interpret our results. To facilitate the discussion, on top of each section, we plot the a-priori Moho depth and, for the AA' profile (NFP-20 West section), we also show the correspondent section from Diehl et al. [2009] and Gualtieri et al. [2014] P-models. This profile is representative of the Western-Central Alps and cross the northern part of the Ivrea body [Hunziker

  .: 3D ITALIAN CRUST FROM AMBIENT NOISE DATA about 200-240 km along the section and at 20-40 km depth. The similarity of models in Fig.10is particularly significant if one considers that they have been derived using completely different data and modelling techniques, and suggests that our overall picture of this region's structure is robust. The AA' profile documents the strong variation in crustal thickness between the European crust (25-30 km), the Alpine crustal root (55 km), the strong intrusion of Ivrea body (16-20 km), the Adriatic domain (beneath the Po Plain) with 40 km of total crustal thickness and the Tyrrhenian one (25-30 km).

  ), and, importantly, v S values consistent with geological expectations are found within the layer. The BB' section is a N-S profile across the (western part of the) Eastern Alps, east of the Giudicaria line and goes from the Pannonian basin to the Adria-Tyrrhenia Moho suture zone, crossing the Alps, the deepest part of the Quaternary and Pliocene sediment in the Po Plain and the northern Apennines. The contrast between upper and lower crust is less pronounced in the Alpine region, indicating an almost uniform crust. The CC' and DD' sections (the latter correspond to the EE' section by [Di Stefano et al., 2009]) show the Adria-Tyrrhenian Moho suture zone at an angle almost perpendicular to the strike of the plate boundary and illustrate the very large Moho offset that is an expression of strong ongoing tectonics. D R A F T November 11, 2015, 9:13pm D R A F T X -25

(

  Neighbourhood Algorithm) to obtain the v S structure under the region of interest with a nominal resolution of 0.25 • ×0.25 • . Our final model (i) is a complete and consistent model, including all the most relevant elastic parameters (v P , v S and ρ), (ii) can be considered an improvement of existing reference models like EPcrust in the Alpine and Northern Italian areas, (iii) has the same vertical parametrization of EPcrust and (iv) incorporates, as a priori information, the most recent progresses in terms of crustal structure from independent methods (LET tomography, receiver function studies and sedimentary basin modeling). Our visual comparison with published results indicates that our model of v S as a function of depth is physically consistent with current knowledge of v P structure in the same region, D R A F T November 11, 2015, 9:13pm D R A F T X -26 MOLINARI ET AL.: 3D ITALIAN CRUST FROM AMBIENT NOISE DATA independently obtained by other seismic methods. Tomographic maps presented here reflect the complexity of the crustal structure of the region and are highly correlated with the known surface geology features of this portion of the European crust: our 7-10s maps are reminiscent of the geographic distribution of deep sedimentary basins, such as the Po Plan and the Molasse Basin; deeper features, including the topography of the Moho and the three-dimensional structure of the crust under the Apennines, the Alps, Adria and the Thyrrhenian sea are resolved well by our data.

Figure 1 .Figure 6 .Figure 7 . 43 Figure 8 .Figure 9 .Figure 10 .

 167438910 Figure 1. Stations where the ambient noise analyzed in this study was recorded.

  MOLINARI ET AL.: 3D ITALIAN CRUST FROM AMBIENT NOISE DATA mology allows to measure surface-wave dispersion at shorter "epicentral" distances, and at shorter periods: in practice, this means that ambient-noise surface-wave data are sensitive to crustal and lithosphere structure but not to the mantle. Today, a number of authors apply ambient-noise interferometry to reconstruct the structure of the crust with increasing resolution, in regions covered by networks of seismographic stations. For instance,[START_REF] Delorey | Basin Shear-Wave Velocities beneath Seattle, Washington, from Noise-Correlation Rayleigh Waves[END_REF] have been able to refine a 3D v S model of the Seattle area for seismic hazard assessment purposes; Zulfakriza et al.[2014] retrived the upper crustal structure of central Java (Indonesia) from transdimensional seismic noise tomog-

	X -6		X -7
	2011] includes robust interface geometry determinations based on seismic reflection and
	refraction studies; [Spada et al., 2013] have constrained Moho depth via controlled-source
	seismology, local earthquake tomography and receiver-function analysis; the 3D structure
	D R A F T	November 11, 2015, 9:13pm	D R A F T

Crustal v S -sensitive data are much sparser than v P -sensitive ones, and current crustal models of v S are relatively unreliable. The recent introduction of seismic interferometry has allowed to map crustal v S by observing surface waves in seismic ambient noise [e.g. Boschi and Weemstra, 2015, and references therein]. As a general rule, surface waves are much more sensitive to v S than to v P . While teleseismic surface-wave observations are limited to long periods and thus mostly affected by mantle structure [e.g. Boschi and Ekström, 2002], ambient-noise seis-D R A F T November 11, 2015, 9:13pm D R A F T raphy; Saygin and Kennett [2012] imaged the Australian crust; Kao et al. [2013] imaged the crust and upper mantle v S structure of Canada and adjacent regions; Lin et al. [2008] and Ekström [2014] have studied North American crustal structure via phase-and groupvelocity maps; preliminary ambient-noise studies of Alpine crustal structure have been conducted by Stehly et al. [2009] and Fry et al. [2010]. Verbeke et al. [2012] compiled a large database of surface-wave dispersion measurements from seismic ambient noise in the Alpine and Italian regions. Their group-velocity maps at periods between 5 and 40 seconds reveal velocity anomalies with high detail, not exploited yet to define a 3D crustal model. These data have strong sensitivity to crustal v S structure, but weak sensitivity to discontinuities and their depth. The geometry of crustal seismic discontinuities under Italy and the Alps, however, has been determined in a number of studies using other observation techniques: model EPcrust [Molinari and Morelli ,

Table 1 .

 1 Data to support this article are publicly available at Orfeus web Warren, L. M., S. L.Beck, C. B. Biryol, G. Zandt, A. A. Õzacar, and Y. Yang (2013).Crustal velocity structure of Central and Eastern Turkey from ambient noise tomography. Geophys. J.Int., 194 (3), 1941Int., 194 (3), -1954. Setting of the variability range of the parameters in the inversion with respect to the a priori informations: MAMBo model[Molinari et al., 2015] in the Po sediment, EPcrust velocity range in the crust and EPmantle in the mantle.Thickness v S (km/s) v P (km/s) Density (g/cm 3 )

	site (http://www.orfeus-eu.org/), INGV databases (eida.rm.ingv.it); EPcrust model is
	D R A F T	November 11, 2015, 9:13pm	D R A F T

X -27

available at http://www.bo.ingv.it/eurorem/EPcrust; CRUST2.0 model is available at http://igppweb.ucsd.edu/ gabi/crust2.html; MAMBo model of the Po basin is available at http://www.bo.ingv.it/ molinari/MAMBo. I. M. was partially supported by a international grant of the Swiss National Science Foundation (SNSF) and has benefited from funding provided by the Italian Presidenza del Consiglio dei Ministri -Dipartimento della Protezione Civile (DPC). This paper does not necessarily represent DPC official opinion and policies. Figures have been prepared

using the Generic Mapping tools [Wessel & Smith, 1998].

X -37