Manamiary Bruno Andriamiarina
email: manamiary.andriamiarina@loria.fr

Dominique Méry
email: dominique.mery@loria.fr

Neeraj Kumar Singh
email: neeraj.singh@cs.york.ac.uk

Revisiting Snapshot Algorithms by Refinement-based Techniques

Keywords: Distributed algorithms, correctness by construction, snapshot, verification

The snapshot problem addresses a collection of important algorithmic issues related to the distributed computations, which are used for debugging or recovering the distributed programs. Among the existing solutions, Chandy and Lamport propose a simple distributed algorithm. In this paper, we explore the correct-by-construction process to formalize the snapshot algorithms in distributed system. The formalization process is based on a modeling language Event B, which supports a refinement-based incremental development using RODIN platform. These refinement-based techniques help to derive a correct distributed algorithm. Moreover, we demonstrate how this class of other distributed algorithms can be revisited. A consequence is to provide a fully mechanized proof of the distributed algorithms.

I. INTRODUCTION

The snapshot problem is a fundamental aspect of distributed computations and distributed applications, since it produces a global state of a distributed system at a particular instant. It is a photography of a global state made up of local states of each process and communication channels. Several solutions for the snapshot problem have been published, among them we consider the seminal algorithm of Chandy and Lamport [START_REF] Chandy | Distributed snapshots: Determining global states of distributed systems[END_REF][START_REF] Tel | Introduction to Distributed Algorithms[END_REF][START_REF] Yang | Global snapshots for distributed debugging: An overview[END_REF]. The snapshot computation is motivated by several applications as, for instance, the verification of stable properties like deadlock, successful termination and debugging of the distributed program using safe configuration. Snapshot algorithms constitute a pertinent collection of case studies for evaluating strengths and weaknesses of formal techniques like model-checking [START_REF] Chaudhuri | The TLA + proof system: Building a heterogeneous verification platform[END_REF][START_REF] Clarke | Model Checking[END_REF] and theorem prover [START_REF] Chaudhuri | The TLA + proof system: Building a heterogeneous verification platform[END_REF][START_REF] Owre | A brief overview of pvs[END_REF][START_REF] Wenzel | The isabelle framework[END_REF]. The correct-by-construction paradigm [START_REF] Leavens | Roadmap for enhanced languages and methods to aid verification[END_REF] offers an alternative approach to prove distributed algorithms and to derive the correct distributed algorithms through the reconstruction of a target algorithm using stepwise refinement and validated methodological techniques [START_REF] Abrial | A mechanically proved and incremental development of ieee 1394 tree identify protocol[END_REF][START_REF] Back | Stepwise refinement of action systems[END_REF]. It appears that the refinement is a key concept for organizing the re-development of an existing distributed algorithm [START_REF] Abrial | A mechanically proved and incremental development of ieee 1394 tree identify protocol[END_REF] to discover a new set of distributed algorithms [START_REF] Cansell | Designing old and new distributed algorithms by replaying an incremental proof-based development[END_REF] by reusing or replaying with the former development.

In this paper, we focus on the distributed snapshots for specific problems. The prime objective is to solve a problem using refinement techniques and to provide an evidence of correctness of given solutions, which are obtained through the correct-by-construction process. We are mainly interested by providing recipes for using the Event B framework and refinement for developing the distributed algorithms. Massingill and Chandy [START_REF] Massingill | Parallel program archetypes[END_REF] introduce archetypes for facilitating parallel program design; more recently, Chandy et al [START_REF] Chandy | Towards verified distributed software through refinement of formal archetypes[END_REF] propose the refinement of formal archetypes to produce verified distributed software using the theorem prover PVS. The conceptual idea of the archetypes is very close to the design patterns in the software engineering domain. Refinement plays a central role in the integration of different archetypes and constitutes the semantical glue for ensuring the correctness of the resulting process. This approach is based on the use of PVS, which is employed to prove the properties of problems modelled using archetypes. Our recipes are conceptually close to the notion behind the archetypes and our aims are to use the Event B framework for developing correct-by-construction distributed algorithms, and enrich a collection of complex distributed algorithms (Project RIMEL: http://rimel.loria.fr). Another objective is to show the power of the correctby-construction process and our recipes through the redevelopment and derivation of already existing and correct snapshot algorithms like the Chandy and Lamport algorithm [START_REF] Chandy | Distributed snapshots: Determining global states of distributed systems[END_REF], or the algorithm of Lai and Yang [START_REF] Lai | On distributed snapshots[END_REF]. Finally, the snapshot problem is already considered as a case study for illustrating the strength of rewriting logic [START_REF] Ogata | Specification and model checking of the chandy & lamport distributed snapshot algorithm in rewriting logic[END_REF] and we think that our development may help a reader to understand the behavioral theory of snapshot algorithms.

The paper is organized as follows. Section 2 defines the snapshot problem in distributed systems. Section 3 introduces notations of Event B and the formal activities of a global system. Section 4 presents refinement-based development of the snapshot algorithm, where we describe the OBSERVATION model for stating what we have to compute. Section 5 introduces the computation of a snapshot in the PROCESS model, which simulates the OBSERVATION model. The global architecture of the refinement-based design is similar to the classical distributed algorithms [START_REF] Chandy | Distributed snapshots: Determining global states of distributed systems[END_REF][START_REF] Lai | On distributed snapshots[END_REF]. Section 5 concludes this paper along with the future work.

II. THE SNAPSHOT PROBLEM

This section presents an abstract overview of the snapshot problem, which helps to understand our proposed solution. We consider a message passing model which formulates a distributed algorithm using a finite set of processes and channels. A direct channel connects each pair of nodes and a list of transformations is attached to each node, which performs either local actions or communications actions. The communication mechanism is supposed to be reliable, which guarantees that the channel does not lose any data packets.

For each node (process), a set of events (send, receive and internal events) is defined. A partial ordering called local causal order (denoted < p for a process (p)), induced by the local sequentiality of each process is defined. The following relationship e i < p e j , between two events e i and e j of a process (p), indicates that e i occurs before e j . A cut C of a local set of events is a subset of events satisfying the relationship :

∀p ∈ P, e, f ∈ C • f ∈ L ∧ e < p f ⇒ e ∈ C.
P is a set of processes and L is a set of pre-shot events (happening before the cut C).

Another ordering called causal order (denoted <) is defined as well. It is the smallest relation containing the local causal orders (< p ) and satisfying the send/receive ordering between processes. The relationship e m < e n , between two events e m and e n of a distributed system, means that e m occurs before e n :

1) If e m and e n are local to a process (p), then e m < p e n .

2) If e m represents the sending of a message, then e n formulates the receiving of the message. 3) There exists another event e k , such that e m < e k and e k < e n . A consistent cut C of a set of events of a distributed algorithm is a subset of events, which satisfies the following relationship : ∀e,

f ∈ C • f ∈ L ∧ e < f ⇒ e ∈ C.
A snapshot S is a global state of a distributed system, which is defined by a set of local states of nodes, and a set of channels states, produced by either internal actions or communication actions. The snapshot S is meaningful and feasible, if there exists an execution producing the global state, and a set of messages is successfully passed through each channel (p → q) of the distributed system, where a set of messages is sent by the node (p) and the sending messages are received by the node (q). The following theorem [START_REF] Tel | Introduction to Distributed Algorithms[END_REF] relates the notions of cut and snapshot :

Theorem 1 A snapshot S induced by a cut C is meaningful if, and only if, C is consistent if, and only if, S is meaningful.

The aim of the snapshot algorithm is to compute a global state of the system from the local states or equivalently a consistent cut. We investigate different steps for deriving two well-known snapshot algorithms [START_REF] Chandy | Distributed snapshots: Determining global states of distributed systems[END_REF][START_REF] Lai | On distributed snapshots[END_REF] using proof-assisted stepwise development.

III. STEPWISE DESIGN OF DISTRIBUTED ALGORITHMS

The correct-by-construction paradigm promotes the development of algorithms using a progressive and incremental approach. The key concept is the refinement which provides linking between discrete models by preserving safety properties. The Event B modeling language designed by Abrial [START_REF] Singh | Modeling in Event-B: System and Software Engineering[END_REF] borrows features from formal modeling languages like UNITY [START_REF] Chandy | Parallel Program Design A Foundation[END_REF], TLA + [START_REF] Lamport | Specifying Systems: The TLA + + Language and Tools for Hardware and Software Engineers[END_REF], action systems [START_REF] Back | Distributed cooperation with action systems[END_REF][START_REF] Back | Decentralization of process nets with centralized control[END_REF]; those modeling languages share common aspects and especially the refinement concepts. The Event B is supported by an open environment RODIN integrating formal features for developing discrete logico-mathematical models. The Event B provides structures for expressing the reactive systems as a set of actions called events and maintaining a list of assertions called (inductive) invariants. These invariants formulate safety properties. We express our design for modeling the distributed algorithms in the Event B using correct-by-construction approach, which is also our primary objective of this work. We recall basic concepts of the Event B modeling language [START_REF] Singh | Modeling in Event-B: System and Software Engineering[END_REF] and a formal development tool called RODIN [START_REF]Rigorous open development environment for complex systems[END_REF].

A. Modelling actions over states

The event-driven approach [START_REF] Singh | Modeling in Event-B: System and Software Engineering[END_REF] is based on the B notation. It extends the methodological scope of basic concepts in order to take into account the idea of formal models. A formal model is characterized by a (finite) list x of state variables possibly modified by a (finite) list of events; an invariant I(x) states properties that must always be satisfied by the variables x and maintained by the activation of the events. Here, we briefly recall definitions and principles of formal models and explain how they can be managed by tools [START_REF]Rigorous open development environment for complex systems[END_REF].

Modifications over state variables are stated by events. An event has two main parts: a guard, which is a predicate built on the state variables, and an action, which is a generalized substitution. An event can take one of the three normal forms described in figure 1 and is associated with a beforeafter predicate BA(x, x ′ ), which describes the event as a logical predicate expressing the relationship between values of the state variables just before (x) and just after (x ′ ) the "execution" of the event (see Fig. 1).

Proof obligations (INV 1 and INV 2) are produced by the tool RODIN [START_REF]Rigorous open development environment for complex systems[END_REF] from events in order to state that an invariant condition I(x) is preserved. Their general form follows immediately from the definition of the before-after predicate, BA(e)(x, x ′ ), of each event e (see Table 1). Note that it follows from the two guarded forms of the events and this obligation can be trivially discharged in case of false condition of the guard. When this is the case, the event is said to be disabled. The proof obligation FIS expresses the feasibility of the event e with respect to the invariant I.

END

We assume that M is a set of messages that can transit along channels. Each process may have a local state and a set of local states is P States. The communication network is modelled by a structure called NETWORK. The network is supposed to be fixed (channels are not modified or created or deleted) and connected.

C. Describing the current system

The snapshot algorithm captures a set of actions modifying a set of variables, through the observation of the current distributed system. Hence, our modeling process states that the existing system simulates a new set of modifications in the current state. A model SYSTEM describes the general activities of the distributed system.

These activities are a) internal and b) external (interactions between nodes) operations modelled by the following events: Internal-local: to modify a local state of a process (p); Internal-message: to modify a local set of messages using a process (p); Sending: a process (p) sends a message to a process (q);

END

Receiving: a process (q) receives a message from a process (p). After each operation, the time-stamp (o(p)) of a process (p) is incremented, and a trace of activities (either internal/local or external) is added to history (h(p)) of the process (p).

A new step expresses the observation of the current system by another process which is defined by a refinement of the current model. In the next section, we define the refinement and apply it for the observation.

IV. INCREMENTAL PROOF-BASED DEVELOPMENT

A. Model Refinement

The refinement of a formal model allows us to enrich a model in an incremental way which is the foundation of the correct-by-construction [START_REF] Leavens | Roadmap for enhanced languages and methods to aid verification[END_REF] approach. Refinement provides a way to strengthen invariants and to add details to a model. It is also used to transform an abstract model in a more concrete version by modifying the state description. This is done by extending the list of state variables (possibly suppressing some of them), by refining each abstract event into a corresponding concrete version, and by adding new events. The abstract state variables, x, and the concrete ones, y, are linked together by means of a, so-called, gluing invariant J(x, y). A number of proof obligations ensure that (1) each abstract event is correctly refined by its corresponding concrete version, (2) each new event refines skip, (3) no new event takes control for ever, and (4) relative deadlock-freeness is preserved. Details of the formulation of these proofs follows.

We suppose that an abstract model AM with variables x and invariant I(x) is refined by a concrete model CM with variables y and gluing invariant J(x, y). If BA(e)(x, x ′ ) and BA(f )(y, y ′ ) are respectively the abstract and concrete before-after predicates of the same event, respectively e and f , we have to prove the following statement, corresponding to proof obligation (1):

I(x) ∧ J(x, y) ∧ BA(f )(y, y ′ ) ⇒ ∃x ′ • (BA(e)(x, x ′ ) ∧ J(x ′ , y ′ ))
Now, proof obligation (2) states that BA(f )(y, y ′ ) must refine skip (x ′ = x), generating the following simple statement to prove (2):

I(x) ∧ J(x, y) ∧ BA(f )(y, y ′ ) ⇒ J(x, y ′ )
For the third proof obligation, we must formalize the notion of the system advancing in its execution; a standard technique is to introduce a variant V (y) that is decreased by each new event (to guarantee that an abstract step may occur). This leads to the following simple statement to prove (3):

I(x) ∧ J(x, y) ∧ BA(f )(y, y ′ ) ⇒ V (y ′ ) < V (y)
Finally, to prove that the concrete model does not introduce additional deadlocks, we give formalisms for reasoning about the event guards in the concrete and abstract models: grds(AM ) represents the disjunction of the guards of the events of the abstract model, and grds(CM ) represents the disjunction of the guards of the events of the concrete model. Relative deadlock freeness is now easily formalized as the following proof obligation (4):

I(x) ∧ J(x, y) ∧ grds(AM ) ⇒ grds(CM )
When one refines a model, one can either refine an existing event by strengthening the guard and/or the beforeafter predicate (effectively reducing the degree of nondeterminism), or add a new event in order to refine the skip event. The feasibility condition is crucial for avoiding possible states which have no successor; for instance, the division by zero. Furthermore, such refinement guarantees that a set of traces of the refined model contains (up to stuttering) traces of the resulting model. The basic foundations of the Event B modeling language along with several case studies are availbale in [START_REF] Singh | Modeling in Event-B: System and Software Engineering[END_REF][START_REF] Bjorner | Logics of Specification Languages[END_REF]. The language of generalized substitutions is very rich and allows us to express any relation between states in a set-theoretical context. The expressive power of the language leads to require helps for writing relational specifications and this is why we should provide proof-based patterns for assisting the development of Event B models.

B. General Schema for Refinement

The correct-by-construction approach is based on the use of refinement and to introduce new features in the formal models. The methodology is simply described by the following diagram, which advocates different steps for producing a distributed algorithm using the correct-by-construction approach.

• The context C states properties of graphs.

• The machine M0 expresses the problem to solve by a set of events stating a relation between initial and final states, for instance, the computation of a correct snapshot.

• The refinement of M0 into M1 expresses that the machine M1 expresses the inductive property allowing to express the computation of the snapshot by each node.

• The refinement of M1 by IM prepares the localisation phase and may require more than one refinement step.

• The next refinement of IM is a refinement for producing a set of events corresponding to the localisation of information.

• DA is derived from the M2 ; mapping checks that M2 can be translated into a distributed programming language.

However, we consider a more general schema for developing the snapshot problem, since the snapshot problem is solved by an algorithm which is able to compute the current distributed state. Next subsection starts the refinement process by introducing the first refinement related to the observation of the snapshot.

C. Introducing the OBSERVATION model

The OBSERVATION model refines the SYSTEM model and introduces the functionality, which is required by the snapshot problem: to compute a snapshot. It does not explain how to compute it but what it should compute.

The event snapshot states that a consistent cut (obtained in one-shot), namely acut, is assigned to cut: a moving message is not allowed to be part of the snapshot, if origin of the message is outside of the cut and its destination is inside of the cut. The event expresses the intention to specify the required solution. Further refinements are necessary for introducing the inductive process leading to a consistent cut. Others events are related to the previous models, which are indicated by dots. Due to space limitations, we have given sketch of the modeling. A detailed formal development is available1 .

V. ARCHITECTURE OF THE DESIGN

Figure 2 presents the complete formal development, which starts from SYSTEM and NETWORK and progressively leads to the OBSERVATION and PROCESS. We describe the model PROCESS which provides the underlying computing process to produce a consistent snapshot. Details of the two possible phases are described by the model PROCESS, an abstract model of the Lai and Yang algorithm [START_REF] Lai | On distributed snapshots[END_REF]: channels between processes are represented by sets of messages; however a message (m) is extended by a bit, which determines either if the message is pre or postsnapshot. The bit is 1, when the predicate m ∈ mark(c) holds. The model LOC-PROCESS, refining PROCESS, localizes informations and describes a model for the Lai and Yang algorithm. We can identify, in the LOC-PROCESS model, events representing the phases (A) and (B) of the Lai and Yang algorithm: The actions of this event can be associated with the steps of phase (A) :

EVENT StartingSnapshot REFINES StartingSnapshot ANY nsm ncstate nm WHERE grd1 : initiator / ∈ dom(pcut) grd2 : ncstate ∈ C → P(M ) grd3 : ncstate = cstate ∪ {d → ∅|d ∈ C ∧ prj2(d) = initiator} grd4 : nsm ⊆ C grd5 : nm ∈ C → P(M ) grd6 : nsm = send_mark ∪ {d|d ∈ C ∧ prj1(d) = initiator} grd7 : nm = {d → ∅|d ∈ nsm}
• act1 models step 1: the process (initiator) records its local state. • act2 represents step 2: the process (initiator) takes a local snapshot. • act3 indicates that the process (initiator) will record all pre-snapshot incoming messages (step 3). • Finally, act4 and act5 match step 4: the process (initiator) indicates that all outgoing messages will be labelled with the bit 1. We can see that the two phases (A) and (B) are modelled, respectively, by the events StartingSnapshot and Pro-gressingSnapshot. The other events do not describe parts of the Lai and Yang algorithm; they depict activities of the processes and the network (communications, computations, etc.).

2) The Chandy and Lamport Algorithm: The Chandy and Lamport algorithm [START_REF] Chandy | Distributed snapshots: Determining global states of distributed systems[END_REF] uses a mechanism of coloring and propagation of a red color from a white one. A white message occurs before a snapshot and a red message occurs after the snapshot. We split the two kinds of messages using a variable mark, indicating, whether or not messages (marker) have been sent by processes. The abstract model FIFO-PROCESS of this algorithm refines the model PROCESS: it is an abstract model of the Lai and Yang algorithm. Behaviours of the model FIFO-PROCESS correspond to behaviours of the model PROCESS, thanks to refinement. However, the FIFO-PROCESS introduces new features: the separation between the pre and post-snapshot messages is implemented by a FIFO communication mechanism. Channels between nodes are transformed from sets of messages to FIFO queues. Because of the clear distinction between the pre and post-snapshot phases, the bit of membership defined in the Lai and Yang algorithm can be removed; which means that the messages are less complex. However, we can observe that a strong constraint is added: in the Chandy and Lamport algorithm, FIFO communication channels are mandatory. The LOC-FIFO-PROCESS model refines the FIFO-PROCESS model: the LOC-FIFO-PROCESS model localizes events and is producing the algorithmic form of the Chandy and Lamport algorithm.

VI. DISCUSSION, CONCLUSION AND FUTURE WORK

The snapshot algorithm identifies global states in a distributed system. The result of our works on the snapshot problem is the discovery of a generic architecture which allows the derivation of various algorithms. The model SYS-TEM describes a distributed system and the activities of its processes (computations, communications, etc.). This model is generic: computations, activities, etc. can be made more specific, according to the peculiarities of studied systems. The model SYSTEM is refined by a model OBSERVATION, which introduces the notion of snapshot: an event models the global snapshot of the distributed system. The development of the snapshot is organised from the model called PROCESS, which expresses the underlying computation process and can be refined into several other algorithms. The key idea is to separate the pre-shots and the post-shots and the solution depends on assumptions on channels and messages: the mark variable is either a marker for a bit or a marker for fifo channels. The complexity of the development is measured by the number of proof obligations which are automatically/manually discharged (see table VI). The main difficulty of the development was the expression of a consistent snapshot in the machine PROCESS, therefore the establishment of the refinement relation between PROCESS and the machine OBSERVATION. A set of invariants (A,B,C) of the machine PROCESS (Fig. 3) were the keys of the development, where the generated proof obligations were quite difficult to discharge. Moreover, the snapshot algorithm is supposed to work while another process SYSTEM is working; SYSTEM is a model for another distributed system and the snapshot algorithm is an implementation of the observation of the current system. Contrary to the verification by theorem provers [START_REF] Ogata | Specification and model checking of the chandy & lamport distributed snapshot algorithm in rewriting logic[END_REF], our work provides an architecture for developing the snapshot algorithm using essential safety properties together with a formal proof that asserts its correctness. In this paper, we have experimented on fixed networks. As a part of our future efforts we consider the global family of snapshot algorithms to give a very precise description of different solutions and to link between these algorithms, as we notice that the algorithm of Chandy and Lamport is obtained from the algorithm of Lai and Yang by adding a FIFO communication. Moreover, we plan to integrate the snapshot algorithm with complex distributed systems like mobile networks.

Figure 1 .

 1 Figure 1. Events and proof obligations

AXIOMS axm1 :

 axm1 C ⊆ (P × P ) \ id . . .

  EVENT Internal-local . . . EVENT Internal-Message . . . EVENT Sending . . . EVENT Receiving . . . . . .

Figure 2 .

 2 Figure 2. General Architecture of the Design

  THEN act1 : pstate(initiator) := l(initiator) act2 : pcut(initiator) := o(initiator) act3 : cstate := ncstate act4 : send_mark := nsm act5 : mark := nm

http://www.loria.fr/~andriami/snapshot-pdf/project.html

A. Computing a snapshot

The PROCESS model (see Fig. 3) refines the OBSERVA-TION model, and presents the construction of a correct snapshot (pcut) step-by-step. A control message (marker) is introduced along with events to separate pre and postsnapshot messages for describing the development steps of the snapshot algorithm : to all of its neighbouring nodes. • ProgressingSnapshot: A node (i) receives a message (marker) from the neighbouring node and it begins to record all the incoming messages. If the node (i) receives all the messages before sending the message (marker), it records the local state and transmits the message (marker) to its neighbours. • Snapshot: All the nodes have received a message (marker). For all the nodes, the messages sent to them before a message (marker), have been received. Finally, the global state of the distributed system is saved.

The model also introduces a set of properties for describing the consistency of the cut: (A) If a message m is sent by a process (p) at a time (i), and received by a process (q) at a time (j) before the snapshot, then the time (i) belongs to the past of the cut. (B) If a message m is sent by a process (p) (which has already performed a local cut) at the time (i), received by a process (q) (which has not yet performed a local cut) at a time (j), then the time (i) belongs to the past of the cut. (C) If a message m has been sent by a process (p) to process (q) at a time (i) (before the receiving of a message (marker) by the process (p)), then the time (i) belongs to the past of the cut. The events Sending and Receiving are refined to distinguish pre-snapshot messages and/or activities from their post-snapshot counterparts:

• SendingPreSnapshot: This event describes the sending of a message (m) by a process (p), before the local cut of the process (p). • SendingPostSnapshot: This event presents the sending of the message (m) by the process (p), which follows the local cut of the process (p). The message (m) is marked as being sent after the local cut of the process(p).

• ReceivingPreSnapshotMessages:

This event demonstrates the receiving of the message (m) (sent by the process (p) before the local cut of the process (p)) by a process (q), after receiving a message (marker) by the process (q). The incoming message (m) is recorded by the process (q).

• ReceivingPostSnapshotMessages:

This event shows the receiving of a message (m) (sent by a process (p) after the local cut of the process (p)) by a process (q), after the process (q) has performed a local cut.

• ReceivingBeforeTheSnapshot: This event describes the receiving of a message (m) (sent by a process (p) before the local cut of the process (p)) by a process (q), before the process (q) performs a local cut.

B. Deriving Snapshot Algorithms

1) The Lai and Yang Algorithm: The Lai and Yang algorithm [START_REF] Lai | On distributed snapshots[END_REF] is a two-phases protocol: either (A) one special process (called initiator) initiates the snapshot, or (B) another process among non-initiator processes extends the snapshot. Due to their similarities, we will focus on phase (A), depicted by the following steps: process (initiator) :


Philippe Chouteau

Nicole Defer

Alexandre Florimond

Julien Caldéraro

Martin Higgs

Aurore Gaudin

Emilie Mérour

Daniel Dhumeaux

Hervé Lerat

Jean-Michel Pawlotsky
email: jean-michel.pawlotsky@hmn.aphp.fr

Hepatitis C Virus (HCV) Protein Expression Enhances Hepatic Fibrosis in HCV Transgenic Mice Exposed to a Fibrogenic Agent

Keywords: HCV, hepatitis C virus, ORF, open reading frame, ECM, extracellular matrix, CCl 4 , carbon tetrachloride, wt, wild-type, qPCR, quantitative PCR, hepatic stellate cells, HPCs, hepatic progenitor cells, PBS, phosphate buffer saline, CYP2E1, cytochrome P450 2E1, ROS, reactive oxygen species, BrdU, bromodeoxyuridine, ALT, alanine aminotransferase, AST, aspartate aminotransferase, hepatitis C virus, fibrosis, hepatocyte proliferation, reactive oxygen species, ductular reaction, hepatic progenitor cells

Background & Aims: During chronic HCV infection, activation of fibrogenesis appears to be principally related to local inflammation. However, the direct role of hepatic HCV protein expression in fibrogenesis remains unknown.

Methods:

We used transgenic mice expressing the full-length HCV open reading 4 ). Both acute and chronic liver injuries were induced in these mice by CCl 4 injections. Liver injury, expression of matrix re-modeling genes, reactive oxygen species (ROS), inflammation, hepatocyte proliferation, ductular reaction and hepatic progenitor cells (HPC) expansion were examined.

Results: After CCl 4 treatment, HCV transgenic mice exhibited enhanced liver fibrosis, significant changes in matrix re-modeling genes and increased ROS production compared to wt littermates despite no differences in the degree of local inflammation. This increase was accompanied by a decrease in hepatocyte proliferation, which appeared to be due to delayed hepatocyte entry into the S-phase. A prominent ductular reaction and hepatic progenitor cell compartment expansion were observed in transgenic animals. These observations closely mirror those previously made in HCVinfected individuals.

Conclusions: Together, these results demonstrate that expression of the HCV proteins in hepatocytes contributes to the development of hepatic fibrosis in the presence of other fibrogenic agents. In the presence of CCl 4 , HCV transgenic mice display an intra-hepatic re-organization of several key cellular actors in the fibrogenic process.

INTRODUCTION

Hepatic fibrosis, a result of active fibrogenesis, is a frequent feature of chronic hepatitis C virus (HCV) infection. Fibrogenesis is classically thought to be triggered principally by the local immune response. The role of HCV infection in fibrogenesis, in particular HCV protein expression in the liver, is unknown. Mice of the FL-N/35 lineage express the entire open reading frame (ORF) of a genotype 1b isolate of HCV in a liverspecific fashion [START_REF] Lerat | Steatosis and liver cancer in transgenic mice expressing the structural and nonstructural proteins of hepatitis C virus[END_REF]. In this model, the HCV proteins are expressed within hepatocytes at levels close to those observed in human infection, without infectious virus production or an antiviral immune response. These mice develop lesions similar to those observed during natural infection, including hepatic steatosis and hepatocellular carcinoma [START_REF] Disson | Impaired clearance of virus-infected hepatocytes in transgenic mice expressing the hepatitis C virus polyprotein[END_REF][START_REF] Lerat | Hepatitis C virus proteins induce lipogenesis and defective triglyceride secretion in transgenic mice[END_REF][START_REF] Nishina | Hepatitis C virus-induced reactive oxygen species raise hepatic iron level in mice by reducing hepcidin transcription[END_REF][START_REF] Simonin | Calpain activation by hepatitis C virus proteins inhibits the extrinsic apoptotic signaling pathway[END_REF][START_REF] Higgs | Downregulation of Gadd45beta expression by hepatitis C virus leads to defective cell cycle arrest[END_REF].

Preliminary observations suggested that FL-N/35 mice may be of interest in the study of liver fibrosis [START_REF] Lerat | Steatosis and liver cancer in transgenic mice expressing the structural and nonstructural proteins of hepatitis C virus[END_REF]. However, this model lacks the concomitant fibrogenesis triggers (such as liver inflammation) observed in HCV-infected individuals. Therefore, the effect of HCV protein expression on hepatic fibrosis in this model must be studied in the context of a

The conventional paradigm of fibrogenesis in the liver is largely based on activation of fibrogenic processes associated with transformation of hepatic stellate cells (HSCs) into myofibroblast-like cells [START_REF] Leeuw | Purified rat liver fat-storing cells in culture divide and contain collagen[END_REF][START_REF] Friedman | Mechanisms of disease: Mechanisms of hepatic fibrosis and therapeutic implications[END_REF][START_REF] Friedman | Isolation and culture of hepatic lipocytes, Kupffer cells, and sinusoidal endothelial cells by density gradient centrifugation with Stractan[END_REF][START_REF] Kent | Vitamin A-containing lipocytes and formation of type III collagen in liver injury[END_REF]. However, it remains paradoxical that, whereas HCV infection is present largely within hepatic lobules [START_REF] Liang | Visualizing hepatitis C virus infections in human liver by two-photon microscopy[END_REF], fibrosis predominates in portal areas in chronically infected patients. Currently, there are no explanations for this observation, and the surrounding mechanisms remain uninvestigated. One possible explanation is that viral particles produced within intralobular hepatocytes might directly activate periportal HSCs. Another non-exclusive explanation is that HCV infection may be accompanied by ductular proliferation [START_REF] Roskams | Nomenclature of the finer branches of the biliary tree: canals, ductules, and ductular reactions in human livers[END_REF].

In the normal liver, the replacement of necrotic and apoptotic hepatocytes occurs through replication of adjacent hepatocytes within the lobules. However, this primary pathway is impaired by a variety of insults, including viral infections [START_REF] Marshall | Relation between hepatocyte G1 arrest, impaired hepatic regeneration, and fibrosis in chronic hepatitis C virus infection[END_REF][START_REF] Wagayama | p21WAF1/CTP1 expression and hepatitis virus type[END_REF]. These situations have been shown to lead to proliferation of hepatic progenitor cells (HPCs) [START_REF] Oben | Sympathetic nervous system inhibition increases hepatic progenitors and reduces liver injury[END_REF][START_REF] Bissell | Transforming growth factor beta and the liver[END_REF][START_REF] Yang | Oval cells compensate for damage and replicative senescence of mature hepatocytes in mice with fatty liver disease[END_REF]. Such cells reside primarily in the periportal region and become the source of regenerating hepatocytes, as well as cholangiocytes and draining ductules [START_REF] Oben | Sympathetic nervous system inhibition increases hepatic progenitors and reduces liver injury[END_REF][START_REF] Roskams | Hepatic OV-6 expression in human liver disease and rat experiments: evidence for hepatic progenitor cells in man[END_REF]. A by-product of the activation of this secondary proliferative pathway is a ductular reaction [START_REF] Oben | Sympathetic nervous system inhibition increases hepatic progenitors and reduces liver injury[END_REF], which has been linked to fibrogenesis [START_REF] Glaser | Cholangiocyte proliferation and liver fibrosis[END_REF][START_REF] Grappone | Expression of platelet-derived growth factor in newly formed cholangiocytes during experimental biliary fibrosis in rats[END_REF][START_REF] Herbst | Heterogeneity of liver cells expressing procollagen types I and IV in vivo[END_REF][START_REF] Malizia | Growth factor and procollagen type I gene expression in human liver disease[END_REF][START_REF] Milani | Cellular localization of type I, III and IV procollagen gene transcripts in normal and fibrotic human liver[END_REF][START_REF] Paradis | Expression of connective tissue growth factor in experimental rat and human liver fibrosis[END_REF][START_REF] Pinzani | Endothelin 1 is overexpressed in human cirrhotic liver and exerts multiple effects on activated hepatic stellate cells[END_REF][START_REF] Ramm | Contribution of hepatic parenchymal and nonparenchymal cells to hepatic fibrogenesis in biliary atresia[END_REF][START_REF] Sedlaczek | Proliferating bile duct epithelial cells are a major source of connective tissue growth factor in rat biliary fibrosis[END_REF][START_REF] Wynn | Macrophages: master regulators of inflammation and fibrosis[END_REF].

A strong correlation has been reported between HCV-related portal fibrosis and a periportal ductular reaction, with a relationship between the number of proliferating HPCs and the number of hepatocytes in replication arrest [START_REF] Clouston | Fibrosis correlates with a ductular reaction in hepatitis C: roles of impaired replication, progenitor cells and steatosis[END_REF]. These observations support the hypothesis that portal fibrosis during chronic HCV infection may result from a periportal ductular reaction, possibly as a consequence of altered hepatocyte proliferation.

We illustrate below, using the FL-N/35 HCV transgenic mouse model in conjunction with an exogenous chemical fibrogenic agent, that the expression of HCV proteins in vivo plays a contributory role in the fibrogenic process, and is accompanied by a ductular reaction and a replicative arrest of intra-lobular hepatocytes concomitant with enhanced reactive oxygen species (ROS) production, in the absence of enhanced inflammation.

MATERIALS AND METHODS

Chemicals and antibodies

Carbon tetrachloride (CCl 4 ) and olive oil were purchased from Sigma-Aldrich (St.

Louis, MO). Primary antibodies are described in more details in Supplementary Materials and Methods.

Animals

Wild-type mice (wt) and those transgenic for the entire HCV ORF (FL-N/35 lineage) were from the same genetic background (C57/Bl6) [START_REF] Lerat | Steatosis and liver cancer in transgenic mice expressing the structural and nonstructural proteins of hepatitis C virus[END_REF]. They were used in conformation with the European Community Council directive. Animals were bred and housed as previously described [START_REF] Disson | Impaired clearance of virus-infected hepatocytes in transgenic mice expressing the hepatitis C virus polyprotein[END_REF]. Studies were performed on age-matched 7-to 10month old males.

Chronic CCl 4 treatment

Animals were injected intraperitoneally twice a week for 4 weeks with CCl 4 (0.5 g/g of body weight) diluted in 5% olive oil, obtained the day of injection. Control mice were injected with an equal volume of olive oil. Twenty-four hours after the final injection, animals were sacrificed by CO 2 inhalation, and body and liver weights were measured. Sera (100 L/mouse) and livers were immediately processed for enzymatic assays and histological determination, or kept at -80 °C until processing.

Experimental acute liver injury and measurement of hepatocyte DNA synthesis

Mice were treated with a single intraperitoneal injection of CCl 4 (795 mg/kg body weight diluted in 5% olive oil). They were sacrificed at different time points after the injection. Bromodeoxyuridine (BrdU) was injected intraperitoneally (150 mg/kg of body weight) two hours prior to sacrifice. Hepatocyte DNA synthesis was measured by means of immunodetection of BrdU incorporation as described in Supplementary Materials and Methods.

Western blotting

Frozen liver tissues were processed as previously described [START_REF] Higgs | Downregulation of Gadd45beta expression by hepatitis C virus leads to defective cell cycle arrest[END_REF]. The detailed procedure is described in Supplementary Materials and Methods.

Serum alanine aminotransferase and aspartate aminotransferase level measurements

Levels of alanine aminotransferase (ALT) and aspartate aminotransferase (AST) in the serum of mice were measured on a Cobas ®. 6000 analyzer (Roche, Diagnostics,

Liver histology and immunohistochemistry

Fresh liver tissues were fixed in 10% buffered formalin, paraffin-embedded, and 5 m sections were prepared. Standard histology and immunostainings are described in Supplementary Materials and Methods.

Quantification of hepatocyte reactive oxygen species (ROS)

Frozen liver sections (10 m) from wt and FL-N/35 mice were assessed for the presence of ROS, as previously described [START_REF] Nishina | Hepatitis C virus-induced reactive oxygen species raise hepatic iron level in mice by reducing hepcidin transcription[END_REF]. The percentage of ROS-specific hepatocytes was calculated, and normalized to that in wt controls. In all cases (CCl 4treated and untreated mice), only large cells with round nuclei present within the parenchyma were considered as hepatocytes.

RNA isolation and quantitative real-time PCR analysis

Total RNA and complementary DNA were purified and synthesized, respectively, as previously described [START_REF] Higgs | Downregulation of Gadd45beta expression by hepatitis C virus leads to defective cell cycle arrest[END_REF]. Quantitative PCR was performed with an Applied Biosystems 7300 Thermal Cycler using Taqman reagents (Applied Biosystems), as described in Supplementary Materials and Methods.

Measurement of CCL5 protein in liver tissues

10

CCL5 protein was quantified in frozen liver tissues according to the procedure described in Supplementary Materials and Methods.

Image analysis

Tissue sections were photographed using a Zeiss Axioskop 40 microscope in conjunction with a Zeiss MRc5 Axiocam and Axiovision LE software (Zeiss, Jena, Germany). Image analyses were performed as described in Supplementary Materials and Methods.

Statistical analyses

Statistical analyses were performed using Prism software (GraphPad Software Inc., La Jolla, CA). Results are expressed as mean±standard error of the mean (SEM).

Box-and-whisker graphs are used; the line in the middle is the median, the box extends from the 25th to the 75th percentile, and the whiskers extend to the lowest and highest values. To determine the statistical significance of the data, Mann-Whitney nondetermine correlations between continuous normally distributed variables. All P values were two-tailed, with P values less than 0.05 considered as significant.

RESULTS

Hepatic expression of the full-length HCV ORF enhances liver fibrosis induced by CCl 4 in HCV transgenic mice

The extent of extracellular matrix (ECM) deposition occurring within the liver of wt and FL-N/35 mice chronically exposed to CCl 4 was determined by picrosirius red staining of formalin-fixed, paraffin-embedded liver sections. As shown in Fig. 1A and1B, ECM deposition was observed only in normal anatomical structures such as portal tracts in untreated FL-N/35 and wt mice. Thus, in the absence of an exogenous fibrogenic stimulus, expression of the HCV proteins does not per se stimulate ECM deposition at a level detectable using picrosirius staining.

In CCl 4 -treated wt and FL-N/35 animals, picrosirius red staining demonstrated established fibrosis with distinctive septa-like morphologies (Fig. 1A and1B). In both transgenic and nontransgenic animals, the quantity of ECM was significantly greater than in the corresponding untreated animals (Fig. 1B). In CCl 4 -treated mice, the quantity of ECM was significantly greater in FL-N/35 than in wt animals (median collagen deposition: 1.7, range 1.0-2.8 vs 1.2, range, 0.9-2.4; P=0.0039) (Fig. 1B).

As differences in the expression of cytochrome P450 2E1 (CYP2E1), the enzyme responsible for bioactivation of CCl 4 , could be responsible for the observed difference [START_REF] Weber | Hepatotoxicity and mechanism of action of haloalkanes: carbon tetrachloride as a toxicological model[END_REF], we quantified CYP2E1 expression by western blotting in HCV transgenic and wt animals. No difference was found between the two groups (Supplementary Fig. S1).

Overall, these results suggest that intrahepatic expression of the HCV proteins in vivo potentiates the fibrogenic effect of the exogenous agent CCl 4 .

Increased liver fibrosis induced by CCl 4 in transgenic mice is not due to a higher degree of necroinflammation in the presence of HCV proteins

We examined the role of HCV protein expression in liver necroinflammation in the presence and absence of CCl 4 . Hematoxylin-eosin staining of liver tissues showed normal hepatic architecture in wt and FL-N/35 mice that did not receive CCl 4 (Supplementary Fig. S2). In contrast, CCl 4 -treated animals showed remnants of degenerated and ballooned/necrotic hepatocytes, equivalently present in wt and FL-N/35 mice. Mild mononuclear cell infiltration in the same areas was also evenly present in these animals.

Expression of F4/80 mRNA, a marker of resident and recruited macrophages, did not differ between untreated wt and FL-N/35 animals. F4/80 mRNA expression was induced to the same degree in both transgenic and non-transgenic mice after chronic CCl 4 administration (Supplementary Fig. S3). Immunostaining of liver tissues with the pan-T lymphocyte marker CD3 revealed similar degrees of T lymphocyte infiltration in wt and FL-N/35 mice exposed to CCl 4 , with CD3-positive cells present along hepatic septa (Supplementary Fig. S4).

The chemokine CCL5 is secreted by T-cells and macrophages and could play a role in fibrosis by stimulating hepatic stellate cells [START_REF] Berres | Antagonism of the chemokine CCl5 ameliorates experimental liver fibrosis in mice[END_REF]. CCL5 expression did not differ between wt and FL-N/35 animals, both in the presence and absence of CCl 4 (Supplementary Figs. S5 andS6).

Taken together, these results suggest that enhanced fibrosis in HCV-transgenic mice exposed to CCl 4 is not mediated by an increased necroinflammation.

Increased liver fibrosis induced by CCl 4 in transgenic mice is associated with alterations in the expression of genes involved in ECM remodeling

We measured the hepatic expression of a number of ECM remodeling genes, including genes coding for ECM components (collagens), proteins involved in ECM production/degradation (matrix metalloproteinases [MMP]) and regulators of MMPs (tissue inhibitors of metalloproteinase [TIMP]) in the different groups of mice. As shown in Fig. 2, in the absence of an exogenous fibrogenic stimulus, the expression of HCV proteins in hepatocytes was not associated with higher levels of expression of these genes. In CCl 4 -treated wt animals, expression of all of the tested mRNA levels was significantly modified compared to the untreated mice, but in various directions (Fig. 2).

Among the different collagen genes tested, only collagen 1 1 expression was notably enhanced in FL-N/35 compared to wt CCl 4 -treated mice, although the results did not reach statistical significance (p = 0,055). The expression of the other collagens showed no difference (Fig. 2A). MMP7 mRNA levels were significantly lower in HCV transgenic than in non-transgenic CCl 4 -treated animals, whereas the expression of MMP13, MMP3 and TIMP1 was notably but not significantly lower (p values between 0.052 and 0.055, Fig. 2B and2C). These results were in keeping with the increase in ECM deposition observed in HCV transgenic animals treated with CCl 4 .

Liver fibrosis is associated with decreased hepatocyte proliferation in HCV transgenic mice chronically exposed to CCl 4

Since hepatic fibrosis in HCV-infected patients has been associated with increased hepatocyte replicative arrest [START_REF] Clouston | Fibrosis correlates with a ductular reaction in hepatitis C: roles of impaired replication, progenitor cells and steatosis[END_REF], we next examined the extent of hepatocyte proliferation in wt and FL-N/35 mice in the presence and absence of CCl 4 . Hepatocyte proliferation was evaluated by immunohistochemistry for Ki67, a nuclear antigen that is expressed in G1, S, G2 and M phases of the cell cycle, but absent in G0 or quiescent phase. In the absence of chronic CCl 4 exposure, a very low proportion of proliferative hepatocytes was observed in both wt and FL-N/35 mice, with no differences between these two groups, suggesting low-level basal renewal of the mature hepatocyte pool in the parenchyma (Fig. 3A and3B).

As a consequence of chronic exposure to CCl 4 , hepatocyte proliferation was significantly increased in both wt and FL-N/35 mice compared to non-exposed animals (Fig. 3A and3B). As shown in Fig. 3B, hepatocyte proliferation was significantly lower in CCl 4 -exposed FL-N/35 than in wt mice (median positive hepatocytes, 25.1 %, range 7.1-65.7 %, vs 30.3 %, range 5.9-49.2 %, respectively; P=0.002). No difference in the distribution of proliferating hepatocytes within the parenchyma was observed between treated wt and FL-N/35 animals.

In HCV-transgenic mice exposed to CCl 4 , a significant inverse relationship between the number of Ki67 positive hepatocytes and the extent of ECM deposition was observed (r=0.893, P=0.012; Fig. 3C). In contrast, no correlation was found in CCl 4exposed wt mice (r=0.1022, P=0.81; Fig. 3D).

In concert, these results suggest that fibrosis induced by CCl 4 exposure in the context of HCV protein expression is concomitant with a lowered capability of hepatocytes to regenerate.

A prominent ductular reaction is present in HCV transgenic mice chronically exposed to CCl 4

Since decreased hepatocyte proliferation has been linked with the development of a ductular reaction in several hepatic disorders, in particular in HCV infection [START_REF] Clouston | Fibrosis correlates with a ductular reaction in hepatitis C: roles of impaired replication, progenitor cells and steatosis[END_REF][START_REF] Richardson | Progressive fibrosis in nonalcoholic steatohepatitis: association with altered regeneration and a ductular reaction[END_REF],

we next studied the ductular reaction in both wt and FL-N/35 mice by immunochemistry for cytokeratin 19 (CK19), a common bile duct, ductular epithelium and HPC marker in murine tissues. CK19-positive staining was limited to bile duct cholangiocytes in untreated wt and FL-N/35 mice, with no differences between the two groups (Fig. 4A and4B).

Exposure of wt animals to CCl 4 did not modify the quantity and distribution of CK19-positive biliary epithelium (Fig. 4A and4B). In contrast, HCV transgenic animals chronically exposed to CCl 4 presented a prominent positive staining for CK19, distributed at the periphery of the portal areas, in chords, clumps and rings, quite distinct from the anatomical bile ducts (Fig. 4A). The area occupied by CK19-positive biliary epithelium, comprising both anatomical bile ducts and the ductular reaction, was increased nearly 3-fold compared with CCl 4 -exposed wt mice (0.59% and 0.18% respectively, P=0.0016; Fig. 4B).

Altogether, these results suggest that fibrosis induced by CCl 4 exposure in the context of HCV protein expression is concomitant with a ductular reaction, which is absent in similarly treated wt animals.

The ductular reaction is associated with expansion of the HPC population in HCV transgenic mice chronically exposed to CCl 4

Since hepatic fibrosis in HCV-infected patients has been associated with increased HPC expansion [START_REF] Clouston | Fibrosis correlates with a ductular reaction in hepatitis C: roles of impaired replication, progenitor cells and steatosis[END_REF], we assessed whether the increased ductular reaction was associated with expansion of the HPC population in HCV transgenic animals exposed to CCl 4 . HPCs were distinguished from cholangiocytes as being CK19-positive cells distal to sites of ductular reaction and isolated within the parenchyma, without the cord-like arrangement of the ductules. In the absence of CCl 4 , a few HPCs were visible in the livers from either wt or FL-N/35 mice (Fig. 4A and4C). After chronic CCl 4 treatment, a non-significant trend towards a higher number of isolated CK19-positive cells than in the untreated animals was observed in wt mice (Fig. 4A and4C). In CCl 4treated FL-N/35 mice, a statistically significant increase in CK19-positive cells was observed when compared to CCl 4 -treated wt mice (P=0.0016; Fig. 4C).

We observed significant correlations between the number of HPCs per portal tract and the extent of ECM deposition (r=0.71, P=0.0062; Fig. 4D), and between the number of HPCs and the surface of the ductular reaction (r=0.7984, P=0.0011; Fig. 4E), which were independent of HCV protein expression. However, FL-N/35 animals displayed increased ECM deposition, an increased number of HPCs per portal tract, and a larger ductular reaction when compared with wt animals, suggesting that the viral proteins may exacerbate these phenomena.

Together, these data indicate that the increased ductular reaction observed in HCV transgenic mice is associated with expansion of the HPC population.

The expansion of the HPC population leads to normal liver reconstitution in HCV transgenic mice chronically exposed to CCl 4

As shown in Table 1, despite the decreased hepatocyte proliferation in FL-N/35 transgenic mice chronically exposed to CCl 4 shown in Figs. 3A and3B, no difference was observed in body or liver weights between olive oil-and CCl 4 -treated animals in both wt and FL-N/35 groups, suggesting that liver tissue reconstitution is not substantially impaired in HCV transgenic mice.

Hepatocyte cell cycle progression is impaired after acute liver injury in HCV transgenic mice

In order to assess whether HCV protein expression impairs liver regeneration, hepatocyte proliferation was measured in both wt and FL-N/35 mice during the course of acute CCl 4 -induced liver injury (Fig. 5A). Analysis of BrdU incorporation showed no or very few BrdU-positive cells in wt and HCV transgenic mouse livers before CCl 4 injection (0h), indicating that the majority of liver cells were quiescent in G0. As shown in Fig. 5A and 5B, both wt and HCV transgenic animals showed a significant increase of BrdUpositive hepatocytes after CCl 4 injection, suggesting entry into the S-phase of the cell cycle. However, this phenomenon was delayed in HCV transgenic animals, with a peak of BrdU incorporation reached at 48 hours post-injection, compared to 40 hours postinjection in wt animals (Fig. 5B). These findings indicate that HCV protein expression is associated with a delay in early cell cycle progression after acute liver injury.

ROS production is enhanced in HCV transgenic mice treated or not with CCl 4

Since oxidative stress has been reported to modulate the fibrogenic response and elevated ROS production is frequently observed in HCV infected cells [START_REF] Novo | Redox mechanisms in hepatic chronic wound healing and fibrogenesis[END_REF][START_REF] Simula | Hepatitis C virus-induced oxidative stress and mitochondrial dysfunction: a focus on recent advances in proteomics[END_REF], we measured ROS levels in the livers of wt and FL-N/35 mice. Using dihydroethidium (DHE) as a marker for intracellular ROS, we found that hepatocyte-specific ROS levels were significantly higher in frozen liver sections from HCV transgenic mice compared to their wt littermates in the absence of CCl 4 treatment (Fig. 6A, upper panels and Fig. 6B), In CCl 4 -treated animals, ROS levels were significantly higher than in untreated animals in both the wt and FL-N/35 groups (Fig. 6A, lower panels), principally due to infiltrating cells. However, when ROS production was measured only in hepatocytes, the levels were significantly higher in CCl 4 -exposed FL-N/35 mice than in their wt counterpart animals (Fig. 6A, lower panels and Fig. 6B). These results show that intrahepatic expression of the HCV proteins is associated with enhanced baseline ROS levels and that this phenomenon is amplified by CCl 4 treatment.

DISCUSSION

Several in vitro reports have suggested that HCV proteins can directly induce fibrogenetic processes. For example, it has been shown that the culture medium of Huh7 cells harboring the HCV subgenomic replicon is able to activate in vitro-cultured HSCs, demonstrating that virus production is not a pre-requisite for such activation [START_REF] Schulze-Krebs | Hepatitis C virus-replicating hepatocytes induce fibrogenic activation of hepatic stellate cells[END_REF].

Moreover, the core and nonstructural 5A (NS5A) proteins have been suggested to play a direct role in the alteration of the hepatocyte metabolism, partly via mitochondrial deregulation which generates ROS, strong inducers of pro-fibrogenic cytokines within the liver [START_REF] Lerat | Steatosis and liver cancer in transgenic mice expressing the structural and nonstructural proteins of hepatitis C virus[END_REF][START_REF] Gong | Human hepatitis C virus NS5A protein alters intracellular calcium levels, induces oxidative stress, and activates STAT-3 and NF-kappa B[END_REF][START_REF] Moriya | Oxidative stress in the absence of inflammation in a mouse model for hepatitis C virusassociated hepatocarcinogenesis[END_REF].

The mouse model used in this study is ideal to assess the effect of HCV protein expression on a liver phenomenon. Indeed, these mice specifically express the different HCV proteins in the liver; however, they are unable to reproduce the complete HCV life cycle, because the transgene is composed of a cDNA corresponding to the full-length genome necessary for replication of viral RNA are lacking [START_REF] Lerat | Steatosis and liver cancer in transgenic mice expressing the structural and nonstructural proteins of hepatitis C virus[END_REF].

Our findings suggest that HCV protein expression per se is not able to induce fibrosis at a level detectable by common histological and molecular techniques.

Nevertheless, we demonstrate for the first time that hepatic expression of the full-length HCV ORF in vivo is able to enhance fibrosis induced by another fibrogenic agent, a context similar to chronic human infection where a number of fibrogenic triggers are present in the liver. Importantly, this effect is independent of the degree of local inflammation. Our finding that ROS production is significantly increased in HCV transgenic hepatocytes, both in the absence and presence of CCl 4 treatment, could at least partly explain that HCV transgenic mice are more susceptible to the development We show that enhanced liver fibrosis in HCV transgenic animals is associated with a deregulation of the expression of several matrix remodeling genes. This includes down-regulation of the expression of MMP13, a protease that specifically degrades collagen 1, TIMP1, a protein that inhibits MMPs active forms [START_REF] Denhardt | Tissue inhibitor of metalloproteinases (TIMP, aka EPA): structure, control of expression and biological functions[END_REF], and MMP3, an activator of pro-MMPs. Thus, HCV transgenic animals seem to be less able to degrade collagen 1, thereby favoring ECM deposition. In addition, the expression of MMP7, a protease implicated in nerve growth factor-dependent myofibroblast survival [START_REF] Kendall | p75 neurotrophin receptor signaling regulates hepatic myofibroblast proliferation and apoptosis in recovery from rodent liver fibrosis[END_REF], was reduced in CCl 4 -treated HCV mice, whereas a similar trend was found in untreated transgenic animals, suggesting that HCV protein expression could protect hepatic myofibroblasts from apoptosis, thus prolonging fibrosis signals.

In our study, the enhancement of fibrosis induced by another fibrogenic agent in transgenic mice expressing the full-length HCV ORF is accompanied by reduced hepatocyte proliferation, which correlates with the stage of fibrosis. The replacement of hepatocytes lost from normal hepatic parenchyma is known to occur through replication of mature hepatocytes [START_REF] Bissell | Transforming growth factor beta and the liver[END_REF]. Inhibition of hepatocyte replication by drugs [START_REF] Bissell | Transforming growth factor beta and the liver[END_REF], alcohol [START_REF] Crary | Expression of cyclin-dependent kinase inhibitor p21 in human liver[END_REF], steatosis [START_REF] Oben | Sympathetic nervous system inhibition increases hepatic progenitors and reduces liver injury[END_REF] or viral infection [START_REF] Wagayama | p21WAF1/CTP1 expression and hepatitis virus type[END_REF][START_REF] Clouston | Fibrosis correlates with a ductular reaction in hepatitis C: roles of impaired replication, progenitor cells and steatosis[END_REF] promotes the activation of a secondary replicative pathway involving bipotential HPCs [START_REF] Bissell | Transforming growth factor beta and the liver[END_REF]. The activation of HPCs subsequently leads to the production of both hepatocytes and cholangiocytes, and the onset of a ductular reaction. The results presented here show that hepatocytes expressing the full HCV ORF exhibit defective replication after treatment with CCl 4 . Our acute liver injury experiments suggest that this effect is, at least in part, due to a delayed entry of hepatocytes into the S-phase of the cell cycle.

The defective replication of HCV-expressing hepatocytes leads to the activation of the HPC pathway and subsequent amplification of the HPC population. In keeping with this hypothesis, we observed reduced proliferation of mature hepatocytes together with a marked increase in the number of activated HPCs and a prominent ductular reaction in CCl 4 -treated FL-N/35 mice. A strong relationship between hepatic fibrosis severity and the intensity of the ductular reaction has been reported in both rodents and humans [START_REF] Clouston | Fibrosis correlates with a ductular reaction in hepatitis C: roles of impaired replication, progenitor cells and steatosis[END_REF][START_REF] Richardson | Progressive fibrosis in nonalcoholic steatohepatitis: association with altered regeneration and a ductular reaction[END_REF][START_REF] Lowes | Oval cell numbers in human chronic liver diseases are directly related to disease severity[END_REF][START_REF] Knight | Attenuated liver progenitor (oval) cell and fibrogenic responses to the choline deficient, ethionine supplemented diet in the BALB/c inbred strain of mice[END_REF]. A similar relationship is shown here in the FL-N/35 mouse strain in the context of HCV protein-induced liver fibrosis [START_REF] Clouston | Fibrosis correlates with a ductular reaction in hepatitis C: roles of impaired replication, progenitor cells and steatosis[END_REF].

In summary, we have shown that transgenic mice expressing the full-length HCV ORF develop more severe hepatic fibrosis after chronic CCl 4 exposure than nontransgenic animals. This effect is not linked to local inflammation alterations induced by HCV proteins. Like during chronic HCV infection in humans, enhanced fibrosis in HCV transgenic mice is associated with a pronounced ductular reaction, HPC activation and a concomitant reduction in hepatocyte proliferation that appears to be in part due to a delayed entry of hepatocytes into the S-phase of the cell cycle. In addition, HCVrelated fibrosis is associated with deregulation of the expression of several matrix remodeling genes and enhanced ROS production that likely participate in the fibrogenic process. Overall, our findings in HCV transgenic mice show that expression of the HCV proteins in hepatocytes contributes to the development of hepatic fibrosis in the presence of other fibrogenic agents, a situation close to human infection.

Fig 1 .

 1 Fig 1. Histological analysis of liver fibrosis in wt and FL-N/35 mice in the absence

Fig. 2 .

 2 Fig. 2. mRNA level quantification of genes involved in ECM remodeling in the

Fig. 3 .Fig. 6 .

 36 Fig. 3. Hepatocyte proliferation in wt and FL-N/35 mice in the absence or presence

Table 1 .

 1 Age, body and liver weights and ALT/AST levels in wt and FL-N/35 mice chronically exposed or not to CCl 4 . Mean±SEM values are shown. NS: not significant.

  Figure 2A

Conflict of interest:

The authors declare that they have nothing to disclose regarding conflict of interest with respect to this manuscript.


Valérie Mauroy

Wilfried Blanc

Michèle Ude

Stanislaw Trzesien

Bernard Dussardier

Growth of rare-earth doped oxyde nanoparticles in silica fibers", 9th Symposium "SiO2: Advanced Dielectrics and Related Devices

Keywords: silica, nanoparticles, erbium, alkaline earth

INTRODUCTION

Developing of new rare-earth (RE)-doped optical fibers for power amplifiers and lasers requires continuous improvements in the fiber's spectroscopic properties (like gain and efficiency characteristics, resistance to spectral hole burning and photodarkening,…) besides reduction in device size and economical efficiency. Silica glass as a host material for fibers has proved to be very attractive. However some potential applications of RE-doped fibers suffer from limitations in terms of spectroscopic properties resulting from clustering or inappropriate local environment when doped into silica.

The route of interest here consists of using silica as a mechanical host and support of the fiber optical waveguide, and of embedding RE-ions within oxide nanoparticles of composition and structure different from those of silica, and small enough to induce acceptable scattering loss. We have proposed a straightforward technique allowing to embed RE ions within in-situ grown oxide nanoparticles in silicabased preforms [1]. The implemented principle is the spontaneous phase separation process. Two key advantages of this process are that (i) nanoparticles are grown in-situ during the course of the fabrication process and (ii) there is no need (and associated risks) of nanoparticles manipulation by an operator. Further, the process takes advantage of the high compositional control and purity typical of the MCVD technique.

In the present paper, we report on the growth of erbiumdoped MO-silicate nanoparticles, that are stable after the fiber drawing stage using the MCVD and solution doping techniques. This demonstrates the potentiality of this fabrication technique for applications such as fiber amplifiers.

EXPERIMENTAL DETAILS

Preforms were fabricated by the conventional MVCD technique. In this process, gaseous chlorides (SiCl 4 , GeCl 4 , POCl 3 ) are passed through a rotating silica tube, heated by an external burner in translation along the tube. Due to the high temperature, chlorides oxidize, forming particles which deposit on the inner wall. This porous layer turns into a glassy layer when the burner passes over it (the tube external temperature is around 1500 °C). In the final stage, the tube is collapsed into a rod at a temperature higher than 1800°C. fibers were obtained by stretching preforms in a drawing tower at temperatures higher than 2000 °C under otherwise normal conditions. Opto-geometric properties of the perform (or fiber) are determined by adjusting the composition and number of layers. In our samples, phosphorous and germanium concentrations are ~0.5 mol% and 1 mol%, respectively.

Erbium and alkaline-earth ions were incorporated through the solution doping technique. An alcoholic solution (of desired strength of ErCl 3 .6H 2 O or MCl 2 .6H 2 O) is soaked for two hours in the unsintered core layer. After removing the solution, the layer is dried and sintered. Erbium concentration is estimated through absorption spectra to be around 300 ppm Is is comparable with the concentration in standard Erbium-Doped Fiber Amplifier. Two alkaline-earth concentrations in the solution were prepared: 0.1 and 1 mol/l. The core diameter in the preforms was measured with a preform analyzer (York Technology P 101) to be 1 mm. It is about 8 µm in fibers.

NANOPARTICLES CHARACTERIZATIONS

Nanoparticles were characterized through scanning electron microscopy (SEM) in the backscattered electrons mode. Typical SEM picture from the exposed core section of cleaved fibers is shown on Fig. 1 (Mg concentration in the solution is 0.1 mol/l). The gray disk corresponds to the fiber core. Nanoparticles, visible as bright spots, are only observed when alkaline-earth ions (Mg, Ca or Sr) are added. They show an important compositional contrast compared to the silica background. The dark central part of the core is caused by the evaporation of germanium element; this is a common artifact of the MCVD technique that can be corrected through process optimization.

The statistical histograms of the size distribution of the NP for 0.1 mol/l Mg-doped preform and fiber are presented in Fig. 2. The mean particle size is 50 nm in the preform and 40 nm in the fiber. Those histograms show that the NP are preserved during the drawing step, in spite of the high temperature of this stage (~2000 °C). Moreover, the size distribution is slightly affected by this step : the mean size decreases from 50 nm downto 40 nm, in the preform and the fiber, respectively, while the core diameter is divided by 100.

When the Mg solution concentration increases from 0.1 to 1 mol/l, the mean particle diameter almost doubles to reach 80 nm. In this fiber, NPs up to 160 nm were observed. Ca and Sr incorporations lead also to particle with a mean diameter of 100 nm, even for a concentration in the solution of 0.1 mol/l.

Regarding light attenuation, fibers prepared with 0.1 mol/l of Mg are compatible with applications as losses as low as 0.4 dB/m were measured [2]. Other fibers, with 100nm NP, lead to high attenuation level, above 100 dB/m. Erbium spectroscopy is modified by the presence of the NP. Two behaviors are observed : in the case of low Mg concentration, Erbium spectroscopy is related to silicabased sample, while for high Mg concentration, Er spectroscopy is clearly related to phosphate environment [2].

During the presentation, we will discuss the influence of the MCVD parameters (alkaline-earth concentrations, deposit temperature, sintering temperature, collapsing stage) on the growth of NP in order to control their sizes. Relation with erbium spectroscopy will also be reported.

CONCLUSION

A method to fabricate nanostructured Er 3+ -doped fibers entirely through the MCVD process is demonstrated. By adding magnesium to the silica-based composition, nanoparticles of 40 nm in diameter are obtained through in situ growth without requiring a separate process to realize nanoparticles (such as post-process ceramming). Such fibers have low-loss. Moreover, a broadening of the emission spectrum by as much as almost 50% is observed with attractive features to realize gain flattened fiber amplifiers. More generally, this concept has great potentials as possible solutions to nowadays issues in amplifying fibers, including (but not limited to) amplifiers intrinsic gain flattening and/or spectral hole burning, amplifiers irradiation strengthening, photodarkening in fiber lasers, etc.

ひ ß̶ "5 OEıaeoeAEOE"5AEど に" #¸©̇º˚̋¸"&AE̋Ø̋˚ßøAE˚oe"̇º¸"4̋Ø̇ß̋¸"&̋©AE˚̋oe" !"#$%&'()#"*#"+,#-$"."/01"#$"23"4-5#6" なば にど",º̋"にどなに" " " " " " " "

Figure 1 :

 1 Figure 1: SEM picture of a Mg-doped fiber

Figure 2 :

 2 Figure 2: Histograms of the particle size in Mg-doped preform (top) and optical fiber (bottom).