Atif Mashkoor

Jean-Pierre Jacquot

Guidelines for Formal Domain Modeling in Event-B

Keywords: Formal methods, Domain modeling, Event-B

In this paper, we explore the possibility to use Event-B as a formal domain modeling tool. We identify the areas where domain modelers can struggle and present some guidelines to avoid these pitfalls. We mainly address three questions about domain modeling: what to specify, how to refine, and how to verify. We discuss the strategy to express domain assumptions, protocols, time, and temporal properties.

We also analyze the refinement and proof system of Event-B in this realm. We advocate small incremental steps and alternative refinement mechanisms, such as "observation levels." We find animation a very helpful activity to complement the verification process.

I. INTRODUCTION

Domain is a universe of discourse, an area of human and societal activity for which some support in the form of computing may be desired [START_REF] Bjørner | Domain engineering[END_REF]. Examples of domains are transport, finance, health care, etc. Domain modeling is the process to document the key concepts of a particular domain, such as entities, their inter-relationships, static and dynamic properties, operations, events, and behaviors. System modeling, on the other hand, is the process in which different models, such as domain analysis, are used to design and construct systems.

A well-founded domain model provides a clear picture of the problem domain to all stakeholders. On the one hand, it helps drawing the underlaying systems' boundaries and on the other hand, it provides a vocabulary which keeps the meaning of the domain's concepts harmonious to everyone.

We can model a domain in a number of ways, either textually, graphically, or formally. While modeling highassurance domains, we prefer the formal approach. Though this choice requires advanced skills with some formal notation, yet it yields several notable advantages. First, a formal specification of the model is amenable to verification and testing which should result into a trustworthy software. Second, it helps to engineer the right software. The systematic derivation of requirements from formal domain models ensures that the resulting software is exactly what the customer want; ambiguities are eliminated right from the start.

The appeal of model-based, i.e., graphical, method is mainly due to an apparent ease of use of the tools and documents. In contrast, formal techniques are often caricatured as ascetic and out-of-reach of average developers.

However this is just a perception, not a reality. Thanks to sophisticated and easy-to-use tools, many complexities tied to the application of formal methods can be abstracted away behind convivial interfaces. Execution techniques of specifications, like animation, can also involve customers into the development at earlier stages. Specification errors do not trickle down the development chain in this fashion. Specification techniques based on mixing formalism, such as [START_REF] Idani | Dynamic Graphical UML Views from Formal B Specifications[END_REF], [START_REF] Mashkoor | Towards Validation of Requirements Models[END_REF], also help requirements engineering. Providing developers with practical guidelines for developing formal models is also an effective mean of promoting their use.

We present here our experience of domain modeling with the formal method Event-B [START_REF]Modeling in Event-B: System and Software Engineering[END_REF]. Event-B is an evolution of the B method [START_REF]The B Book[END_REF] for system-level modeling and analysis of large reactive and distributed systems. We believe that using Event-B is equally suitable for modeling environments and domains where such systems are assumed to operate.

We have gathered our observations while modeling a high assurance domain: land transportation. Our work took place within the framework of the projects TACOS 1 and CRISTAL 2 . These projects aim at studying new transportation systems using autonomous and self-service vehicles known as CyCabs [START_REF] Baille | Le cycab de l'INRIA rhônes-alpes[END_REF]. CyCabs are small computercontrolled electric cars. They can move in three modes: driven by a human, driven by their inboard computer, or within a platoon. In the last mode, several CyCabs assemble as a train without material connections between the cars.

Transportation is defined as the movement of people and goods from one location, called a hub, to another with the use of vehicles. We suppose the existence of a network composed of stations (hubs where vehicles can stop to be loaded and unloaded), junctions (hubs where roads join), and paths which connect stations and junctions together. Movements are constrained by the topology of the network: a vehicle must follow a route, a sequence of adjacent paths, in order to travel from its origin to its destination.

We modeled two general properties of transportation, safety and travel-time. The first is the idea that collisions between vehicles must be avoided. The second reflects the fact that travel time is at the root of nearly all decisions made about transportation, either individually or socially.

In this paper, based on our experience, we present some guidelines for formal domain modeling with Event-B. Section II presents a brief overview of the employed formal method. In Section III, we discuss that what a domain model should be comprised of. Sections IV and V analyze the refinement and verification process of domain modeling in Event-B respectively. Section VI presents some related work. Finally, Section VII concludes the paper and indicates some future work directions. The fully-verified version of the transport domain model which is used as the reference specification is available at the following web address: http://dedale.loria.fr/?q=transport-domain.

II. EVENT-B Event-B is a formal language for modeling and reasoning about large reactive and distributed systems. Event-B is based on set theory and standard first-order predicate logic. Event-B is provided with Rodin 3 , a platform which supports the writing and proving of specifications.

A. Structuring

An Event-B model is composed of two constructs: machines and contexts. Machines, which define the dynamic behavior of the model, contain the system variables, invariants, variants, and events. Variables are typed; their values may be integers, sets, relations, functions or any other settheoretical construct. Invariants define the state space of the variables and their safety properties. Variants are related to the correction of refinements.

An event defines transitions from one state to another. It is composed of guards and actions. A guard is a predicate and an action is an assignment statement to a state variable and is achieved by a generalized substitution. Events can be triggered when their guard is true; the choice of the event to fire is non-deterministic. The actions of a particular event are executed simultaneously. Contexts, which define the static elements of the model, contain carrier sets, constants, axioms, and theorems. The last two are predicates expressed within the notation of first-order logic and set theory.

B. Refinement

Event-B embeds the concept of refinement which is then the basic element of the specification development process. A refinement consists of introducing new variables and events. Abstract events are refined by strengthening their guards and adding actions to the new variables.

Variants can be introduced to guarantee that some new events (called convergent) do not prevent older ones from triggering. They are either a natural number expression which must be decreased or a set which must be made smaller, by each convergent event and not be increased by each anticipated (new but not convergent) event.

A machine can be refined into another machine which then contains a more detailed or concrete description of the model. A context can be refined (extended) into one or 3 http://rodin-b-sharp.sf.net more contexts. It contains the static pieces of information of a model associated to the refinement. A machine can see several contexts, that is, use the names and properties it contains. A context can be seen by several machines.

C. Proofs

The semantics of refinement is given by proof obligations. Proving a refinement correct amounts to prove that concrete events maintain the invariant of the abstract model, maintain the abstraction invariant, and, when appropriate, decrease variants monotonically.

Proofs also ensure that specifications meet essential system properties, such as well-definedness and invariantpreservation. The proof obligations generated by the tool are required to be discharged using provers, either automatically or interactively.

III. WHAT TO SPECIFY?

A domain specification is an abstract description of a domain. This document intends to specify the domain's intrinsic and extrinsic assumptions, protocols, properties, etc. In this section, we discuss what a typical domain model should be comprised of and how to model it in Event-B.

A. Model assumptions

A domain model is the composition of different assumptions about the particular domain. These assumptions can be classified into three categories: structural facts, behavioral laws, and enforceable properties. While always expressed as predicates on the state, these assumptions can be written in the specification either as invariants in machines, axioms in contexts, or guards in events.

Structural facts are the constants of a domain. So, they naturally fit into Event-B contexts. We use axioms to express the structural properties of the model. For instance, in transportation domain, contexts are used to define facts, such as "vehicles have bounded speed and acceleration," "a route is an acyclic sequence of adjacent paths," or position(t + dt) = accel(t)dt 2 /2 + speed(t)dt + position(t).

Behavioral laws are described by events and particularly by their guards. For example, as shown in Figure 1, the law of movement as displacement of vehicles to new locations is modeled with the event travel. Further precisions, such that departure and arrival must be stations and be connected by a route are straight refinements of the event.

Enforceable properties are properties which are necessary for a domain to be well-behaved. They are expressed by invariants. We express the absence of collision this way. Of course, the expression depends on the level of abstraction and is subjected to refinement. For instance, we define a collision on a hub as "too many vehicles on a hub at the same time." When finer movements on a path of the network are described, it is refined to the intuitive definition of "no two vehicles at the same place at the same time."

Whether a particular domain assumption should be expressed as a behavioral law or as an enforceable property is a difficult choice to make. For example, consider the absence of collisions which has been modeled by invariants. We could get the same by modeling this assumption as a special collide event. Formally, there is a strong relationship between the two descriptions: the guard of the hypothetical collide event is the negation of the invariant.

¬Guard(Collide) ⇒ Invariant(NoCollision)

The choice between the two expressions depends on the kind of system one has to develop. For instance, developers of a road traffic monitoring system will likely prefer collide events since their system will have to deal with such situations. Developers of a traffic light control system will likely prefer invariant expressions as it is one of the goals of their system.

B. Define protocols

A domain exhibits several protocols. For instance, travel must be realized in a specific sequence of crossing hubs and traversing paths.

travel ≡ (startTravel; (crossHub; traversePath)+)

This reflects a protocol induced by the network topology and an implicit constraint of land transport. The protocol for crossing a hub must itself be decomposed for collision free traveling: crossHub ≡ (wait * ; enterHub; leaveHub) So as the protocol of traversing a path which can be defined as follows:

traversePath ≡ (waitToEnterOnPath * ; leaveHub;

(waitToMoveOnPath| moveOnPath) * )

Unfortunately, Event-B does not provide us with an easyto-use notation to model the protocols defined above with regular-expression-like formulas. We need to use the standard mechanisms of events and guards. In practice, this mean that we need explicit control predicates over these events so that they can be orderly fired with certain parameters to realize the respective protocols correctly.

Current research on CSP||Event-B [START_REF] Schneider | A CSP Approach to Control in Event-B[END_REF] or atomicity decomposition [START_REF] Butler | Decomposition Structures for Event-B[END_REF] is promising and will lead to elegant solutions to this issue in the future. Meanwhile, we must resort to hand-coded causal orders.

We use two basic techniques: control sets and state markers. For instance, the correct sequence of crossHub and traversePath to decompose a travel is controlled by the set of hubs and paths that still remain to cross and traverse respectively: each event removes one easily characterized element from the set. Crossing hubs is controlled by a discrete marker associated to the vehicles with respect to hubs, where each event sets the marker: vehicleState ∈ Vehicles × Hubs → {initial, entering, onHub, leaving, crossed} Both techniques have some advantages and disadvantages. In the first approach the variant is quite easy to define but at the expense of complex computations (or definitions) of the sets. In the second technique, state markers are easy to use in guards and they make the sequence of events easy to understand. However, it is difficult to set up the variants and, generally, to connect state markers to invariants. Our longest proofs were associated with state markers.

C. Specify time

Time is an important property in high assurance domains; transportation is no exception. A difficulty with time is that it comes in several flavors, most notably discrete and continuous; transportation exhibits both. For instance, modeling travel-time requires discrete time (two readings of a clock), whereas modeling the movement on a path requires continuous time for the kinematics of vehicles. Event-B has no built-in notion of time.

In our models, we use the technique inspired by [START_REF] Cansell | Time Constraint Patterns for Event B Development[END_REF]. It is an instance of event-queue simulation techniques. It uses a global clock which can go only forward (see figure 2 and 3 for the abstract and refined versions), and an eventqueue, activationTime. The introduction of time follows a regular pattern:

1) pick an event to "time" 2) add the guard vehicle∈dom(activationTime) ∧ time=activationTime(vehicle)

3) add the action

activationTime := activationTime ⊳ -{vehicle → time + timeInc}.
timeInc is, of course, dependent on the particular event.

It can be a constant, an arbitrary value or a computation on the event queue. The technique works well both for the discrete time which we use for the abstract protocol of crossing hubs and the continuous time which we use for the kinematics. Events are now synchronized and can only be fired at their appropriate time. Of course, we do not use real continuous time, but a discrete approximation through the choice of a small fixed tick for timeInc.

D. Express temporal properties

Temporal properties, such as safety and liveness, are essential to safety critical and high assurance systems. A safety property states that something bad never happens, whereas a liveness property states that something good eventually happens [START_REF] Lamport | Proving the Correctness of Multiprocess Programs[END_REF]. We need to model temporal properties in both domains and systems, but they play different roles.

A safety property is easily stated in Event-B, as long as it can be expressed as an invariant. No-collision is a typical safety property. While modeling domains, this is adequate: the proof that all events maintain the invariant is sufficient to establish that the domain is well-behaved. Of course, it would not suffice for a system: we must ensure that it is free of deadlocks and divergences.

In fact, we know that the real domain of land transportation is subjected to gridlocks (traffic jams), which are a form of local deadlocks, and, hence to a form of divergence: a vehicle can wait infinitely. So, a good model of the domain must include these facts.

In our transportation model, the gridlocks are actually modeled as special events (lockXXX). The guards of these events state the conditions for systems implemented to work within the domain to keep them free-flowing. Interestingly, the lockXXX events popped out naturally when we introduced the time: some proof obligations could not be discharged without introducing the negation of the gridlock condition.

It is to be noted that the usual techniques to guarantee deadlock-freeness and non-divergence in Event-B specifications [START_REF] Yadav | Verification of Liveness Properties in Distributed Systems[END_REF] are not useful in our case. Introducing the wait event (wait's action is SKIP) is essential for ensuring nocollision. This ensures that the disjunction of the guards of all events is true but makes variant clauses impossible. Since a vehicle can wait an indefinite period of time, we cannot prove that the wait event does not prevent other events from happening.

Unfortunately, it is not always possible to express finer liveness properties in Event-B. Presently, we do not know how to state that a vehicle which has started a travel will eventually reach its destination. Though not really critical for land transport, it is for air transport. For such properties, we need to resort to model checking or animation.

IV. HOW TO REFINE?

As any text, a formal domain model is only the endproduct of a complex thought-process. Its role is to present most of the knowledge necessary to construct software pieces which operate harmoniously and safely. However, readers trying to extract the knowledge out of this formal piece of text are often confronted with a very difficult task.

Sometimes, a domain fact hides under cryptic notations, sometimes it is spread over several parts of the model, or sometimes, it is implicit. Understanding a formal text of some complexity is often equivalent to re-inventing the process of its construction and figuring out the rationale of the development steps.

Event-B, like B, embodies a process idea: formal refinement. Refinements have two roles. On the formal hand, they help master the proof of implementation correctness by breaking a big intractable proof into many manageable small ones. On the methodological hand, they help structure and organize the development process. Linking both roles together is adequate in B where the aim of the development is to produce a working code from a given specification. A refinement in B is a process step where we transform an abstract representation of a piece of information into a concrete and computable representation.

When modeling a domain, we prefer to see refinements as process steps where a new piece of information is added to the model. We find useful to classify refinements in two different categories:

1) state enrichment: a new concept or a new constraint on the state is added. Contexts are extended and the events concerned by the novelty are refined (guards and actions are changed). The structure of the specification is not changed. 2) event decomposition: a "large" event is decomposed into several "smaller" ones. The structure of the model is altered. The second kind of refinement corresponds to a change of "observation level." Observation levels [START_REF] Mashkoor | Domain Engineering with Event-B: Some Lessons We Learned[END_REF] are a way to provide a specification with a super-structure which eases its understanding. They reflect either the "natural" structure of the objects or the structure of the behavior. For instance, decomposition of a protocol into a sub-protocol refers to a change of observation levels. It provides us with an easy way to introduce a new property into the model. This notion is important at the methodological level.

A. Refine slowly

We advise to use small incremental steps while developing domain models. Ideally, only one new fact should be introduced per refinement.

Recording rationales for refinements is essential for later understanding of the formal text. Currently, Rodin provides only minimal abilities in this domain: simple comments. They are not well fitted for long explanations. We make use of this small-step approach to introduce the vocabulary of transportation network, for instance.

More importantly, while some facts will appear at a unique place like a new invariant or a couple of axioms, many will be scattered over the text. Behavioral laws are typical of this. For instance, understanding the protocols which prevent collisions requires to consider the guards of two different sets of events. Expressing each type of collision by one specific refinement eases the work.

Last, expressing only one feature of the domain at a time helped us finding patterns, such as timing (cf. Section III-C), in the refinements of events. Again, this kind of regularity in the expression makes later analysis of the text easier. We should also note that small refinement steps are well supported by Rodin. They do not cost much.

B. Refine unconventionally

The observation levels should be used to organize the development rather than the implicit linear view of refinements.

Event-B has inherited from B the view that a development is a sequence of refinements. This conception is adequate in B, less so in Event-B. The problem with the linear sequence is that when we introduce a new property, we need to do this into a complex piece of text. For instance, if we wanted to introduce the notion of energy consumption, we would like to start the new feature analysis as depicted in Figure 4. From this, we could refine the notion along the observation levels and merge the resulting model with the current specification. Instead, Event-B's flat refinement structure would force us to write the travel event as illustrated by figure 5 and to introduce in all other events a dummy action of the form:

meter ∈| meter'(n) ≥ meter(n)
This action simply states that meter is susceptible to be modified by future refinements. Even if the addition of such an action does not pose any problem, it tends to clutter the text and causes distraction.

Organizing the introduction of a new feature along the observation levels (at least, one refinement per level) has several advantages:

• we make "small" steps, focusing on a small and specific set of events, • we can relate more easily failures during the proofs to incompatibilities between the feature's definition and the existing model, • the levels point "naturally" to the feature's facets we need to analyse. We used this guideline when introducing the notion of time. On the first level, time is only travel-time, something which just needs a readable clock and an event to make it tick. On the second level, time is the same and nothing new is needed (no refinement). On the third level, time becomes a computable quantity and the event-queue technique is introduced. On the fourth level, time becomes continuous and needs to be discretized because of the absence of the abilities to model R in Rodin. The path was easy to follow but is not reflected in the sequence of refinements.

V. HOW TO VERIFY? Verification of a domain amounts to assert that the specified facts, laws and properties about the particular domain are consistent, checkable and provable. A verified domain model is, therefore, considered as a consistent set of assumptions about the domain. In fact, this hypothesis does make sense as an unprovable model, of course, can not be trusted.

Refinements serve different purposes in system development than in domain modeling. In the former case, the refinement is a more concrete description of the same model. We need to prove that the new description enjoys the same functional properties. In the latter case, the refinement is an enrichment of the model. We need to show that the new feature is consistent with the previous ones. Although based on the same set of proof obligations, the proving process needs to be observed from another point of view.

A. Beware of easy proofs!

Asserting the consistency of an assumption expressed as an invariant is relatively easy. Either the invariant related proof obligations can be discharged or not. This is safe. However, when an assumption is expressed as an axiom, it is hard to prove its consistency. Proof obligations assert well-formedness and well-typing, but not consistency. We are then always at a risk to introduce a fact which is contradicting with the rest of the model. Although hard, the ability to detect contradiction among axioms is crucial for the correctness of the model.

Unfortunately, Rodin does not warn us when axioms are inconsistent. One should always keep a skeptical eye on the proofs. If proofs become mysteriously easy to discharge, beware! The introduction of an axiom or a theorem, such as TRUE = FALSE is a useful heuristic. Success in the proof signs a contradiction, failure provides us only with reasonable assurance.

B. Beware of obvious truth!

Discharging a proof obligation using a tool may not always be possible. A proof which cannot be carried out by a prover is not always the sign of an error in the specification. In such cases, a pen-and-paper proof may work.

In Rodin, we can make "approximations" by declaring the goals as "reviewed." While legitimate in certain situations, in particular due to shortcomings of current provers, reviewing an "obvious" goal may lead to a surprise. For instance, assuming x(y/z) = (xy)/z seems natural, except that this is true in R, not in N. Though numerically correct as the difference becomes actually negligible when numerators are much bigger than denominators, this approximation is yet formally incorrect.

One should always be careful while making approximations and going outside the tool to prove an hypothesis. Investing time in proving "the obvious truth" is worth it. Dynamic testing techniques, such as animation with realistic values, can give insight on the validity of the approximations and on the solidity of the model.

C. Use animation to complement provers

Animation allows specifiers to check the behavior of the specification by observing its execution. Non-provable safety and liveness properties can be assessed by analyzing state values and event-enabledness status. We can make solid observations on the behavior of a model by a trace analysis of the simulated scenarios.

Animation cannot show that a property always hold, but it may help to generate counter examples which show that the model is partly incorrect. Animation and model-checking play a similar role, in fact, ProB [START_REF] Leuschel | ProB: A Model Checker for B[END_REF] offers both functions.

A very useful side-effect of animation is to help get better insights on the model. Implicit properties and unexpected behavior, either good or bad, will become apparent. We did even use it as a prototyping tool to fix the expression of tricky protocols. The execution of the specification (without translation into code) identifies right away any undesired transitions in the model's behavior.

Nevertheless, the most important role of animation is to participate in the validation of the model, i.e., to assess that the model is an adequate abstract mathematical representation of the real domain. Ideally, animation should be used after each refinement, at least, after each introduction of a new observation level. The catch is that well-written specifications often contain traits that can not be dealt with by animators. We have then developed behavior-preserving transformations [START_REF] Mashkoor | Formal Domain Engineering: From Specification to Validation[END_REF] for some of these traits which are costeffective enough to be used intensively.

VI. RELATED WORK

A. Domain modeling in RAISE

In recent times, Dines Bjørner's work [START_REF] Bjørner | Development of Transportation Systems[END_REF], [START_REF]Train: The railway domain -a "grand challenge" for computing science & transportation engineering[END_REF] is most notable in the field of formal domain modeling. He uses RAISE Specification Language (RSL) [START_REF]Specification Case Studies in RAISE[END_REF] for the description of domains and concentrates towards the formalization of as many domain facts as possible.

Our research differs from his work on two main fronts. First, we head towards the enrichment of domain models while paying as much attention to verification and validation as specification. Second, our concerns are also to check the capability of Event-B as a domain modeling tool and to point out and address (where possible) the issues with which we confront during this exercise. The choice of formal method can be another difference. A brief comparison of both languages, Event-B and RAISE [START_REF] Group | The RAISE specification language[END_REF], is available in [START_REF] Mashkoor | Utilizing Event-B for Domain Engineering: A Critical Analysis[END_REF].

B. Modeling of the transportation domain in Event-B

Previously, Event-B has been used for the development of transportation systems, see for instance [START_REF] Papatsaras | Global and Communicating State Machine Models in Event Driven B: A Simple Railway Case Study[END_REF], [START_REF] Butler | A System-Based Approach to the Formal Development of Embedded Controllers for a Railway[END_REF], [START_REF] Essamé | Handling Safety Critical Requirements in System Engineering Using the B Formal Method[END_REF], but most of the time the role of this language was limited to system modeling of a particular component. Our work is different in a sense that we are modeling the domain, where such systems are assumed to operate. The specifications of these aforementioned railway systems do contribute towards the completion of the land transport domain model, but as a part of the whole. Our model is more general and could be used for different kind of transportation systems, such as road, railways, conveyors, etc.

C. Alternate refinement mechanisms in Event-B

Linear refinements are the de facto standard of specification development in Event-B. Their counterparts, other than observation levels, are Retrenchments [START_REF] Banach | Retrenchment: An Engineering Variation on Refinement[END_REF], Feature development [START_REF] Poppleton | Towards Feature-Oriented Specification and Development with Event-B[END_REF] and Parallel refinements [START_REF] Abrial | Refinement, Decomposition, and Instantiation of Discrete Models: Application to Event-B[END_REF].

Retrenchment was proposed as a liberalization of the notion of refinement to capture more informal aspects of development within a formal framework. A retrenchment step from an abstract to a concrete level of abstraction allows strengthening of the precondition, weakening of the postcondition, and mixing of state and I/O information between the levels of abstraction by mediation of two extra predicates per retrenchment. In particular, it allows nonrefinement-like behavior to be expressed via the weakened postcondition. This allows the specification of low level details of the model without cluttering up the formal text by unnecessary code which is mandatory to discharge proofs.

Feature-oriented specification development is a mechanism to specify the behavioral variability of the model. A feature, in this case, is a simple B machine which is atomic with respect to other functionalities. The composition of several machines, each highlighting distinctive features, forms the final model. The composition of these features is still a difficult issue. The development is supported by the Rodin plugin [START_REF] Gondal | Feature Composition -Towards Product Lines of Event-B Models[END_REF].

Parallel refinements is another idea of model decomposition to handle the complexity introduced by linear refinements. In this technique, the large model is cut into several smaller components. The model decomposition is either based on shared variables [START_REF] Abrial | Refinement, Decomposition, and Instantiation of Discrete Models: Application to Event-B[END_REF] or on shared events [START_REF] Butler | Decomposition Structures for Event-B[END_REF]. The tool support is presented by [START_REF] Silva | Decomposition Tool for Event-B[END_REF].

Our view on refinement of Event-B models by grouping them into observation levels is different from all of the aforementioned methods. They require intricate proof obligations to measure the correctness of the model and a change in the language. Our approach can be adopted without touching the semantics of the formalism and by just providing a visual modification at the level of tool.

D. Timing and temporal properties in Event-B

The specification of timing and temporal properties in Event-B is known to be a challenging task. The expression of these properties, a key element for use of formal methods in the automotive sector, is currently non-standard in Event-B. Correctness of such specifications thus becomes an issue.

Like us, [START_REF] Bryans | Patterns for Modelling Time and Consistency in Business Information Systems[END_REF] reuses and adapts the timing pattern of Event-B proposed by [START_REF] Cansell | Time Constraint Patterns for Event B Development[END_REF]. Similarly, the pattern of Joochim et al. [START_REF] Joochim | Timing Diagrams Requirements Modeling Using Event-B Formal Methods[END_REF] proposes the use of global time and also interacts with a number of active times. This pattern formalizes the Timing Diagram of UML and does not address timing properties in general. In addition, its usage is recommended at abstract stages rather than in later refinements.

Abrial et al. [START_REF] Abrial | Introducing Dynamic Constraints in B[END_REF] propose the use of temporal properties to model the dynamic behavior in Event-B specifications. In its continuation, [START_REF] Groslambert | Verification of LTL on B Event Systems[END_REF] proposes the use of Linear Temporal Logic (LTL) for such modeling. Like others, [START_REF] Bicarregui | Towards Modelling Obligations in Event-B[END_REF] also proposes an extension of Event-B to incorporate three LTL operators: next, eventually, and bounded eventually. In this work, standard Event-B structures, WHEN, THEN and END are modified to represent these operators. Such models deviate from the standard Event-B notations and their verification and validation are a major challenge. The point is that expressing temporal properties is still a challenge in Event-B. Approaches based on mixing formalism, such as fusion of KAOS with Event-B [START_REF] Mashkoor | Towards Validation of Requirements Models[END_REF] seems a promising solution.

VII. CONCLUSION AND FUTURE WORK

In this paper, we have proposed some guidelines to use Event-B as an effective tool for formal domain modeling. Induced from our experience with transportation, they should, of course, be tested and validated on other domains. Nonetheless, we think that the notion of observation levels, the alternate viewpoint on refinement, the analysis of the role of proofs, and the importance of animation are good premises for a method of domain modeling with Event-B.

Though we have found Event-B an adequate language for domain modeling, yet there are few questions which must be answered. They are mainly about the expression of temporal properties, the tools and the validation of models.

In Event-B, we cannot straightforwardly express and prove properties such as deadlock freeness, liveness, fairness, etc. We consider this an important shortcoming of the language. At the level of tool, Rodin is still in development stages and still needs to be matured for industrial use.

The validation of models is as important as their verification. As formal refinements structure the development and verification process, we believe they can also help structure the validation process. Not all specifications are by default animatable; some needs to be transformed. Work presented in [START_REF] Mashkoor | Formal Domain Engineering: From Specification to Validation[END_REF], [START_REF] Mashkoor | Transformation Heuristics for Formal Requirements Validation by Animation[END_REF] is a preliminary exploration of this idea.

The unprecedented level of complexity of the domain has made it quite difficult to ensure its resilience feature, the ability of the system working within to stay dependable while facing changes. Absence of these properties may lead to devastating accidents unless they are explicitly specified and proved. In future, we are contemplating to model the resilience properties of the domain.

Another challenging task is to observe how different transportation applications can be derived from this complex domain model.

Figure 1 .

 1 Figure 1. Event travel

  Figure 2. ticTac

INVARIANTmeter∈Figure 4 .

 4 Figure 4. Introduction of energy consumption: what we want

INVARIANTmeter∈Figure 5 .

 5 Figure 5. Introduction of energy consumption: what we have

http://tacos.loria.fr

http://www.projet-cristal.org


Professor Annie Scott Anderson
email: a.s.anderson@dundee.ac.uk

Angela M Craigie

PhD Maureen Macleod

BSc Karen L Barton

MSc Shaun Treweek

Alison Kirk

Anne Ludbrook

Andrew Symon

Brian Williams

Supporting postpartum weight loss in women living in deprived communities -design implications for a randomised control trial

Keywords: postpartum, pregnancy, feasibility trial, obesity, weight loss

Introduction

Current projections within the UK suggest that 36% of women will be obese and 32% will be overweight by 2020 [START_REF] Brown | A prediction of obesity trends for adults and their associated diseases[END_REF]. Pregnancy is a life stage where excess weight gain may occur and the postpartum period is often characterised by weight retention or further increase [START_REF] Gore | The role of postpartum weight retention in obesity among women: a review of the evidence[END_REF]. For the overweight mother, weight loss is desirable to meet the physical demands of parenting, to reduce the risk of complications in subsequent pregnancies and reduce the risk of cardiovascular disease and diabetes in later life [START_REF] Galtier-Dereure | Obesity and pregnancy: complications and cost[END_REF].

It is estimated that at 6 weeks postpartum, two thirds of women still weigh more than their pre-pregnancy weight [START_REF] Walker | Do low-income women attain their pre-pregnant weight by the 6th week of postpartum?[END_REF] and at 6 to 18 months, 15-20% of women have retained at least 5kg [START_REF] Calfas | Postpartum weight retention: a mothers weight to bear[END_REF]. In addition to concerns over weight retention, [START_REF] Villamor | Interpregnancy weight change and risk of adverse pregnancy outcomes: a population-based study[END_REF] have demonstrated that weight gain between pregnancies is associated with maternal and perinatal complications such as gestational diabetes, preeclampsia, macrosomia and stillbirth.

Moreover, data collected from antenatal clinics have demonstrated that a significantly greater proportion of women from areas of high deprivation are obese [START_REF] Heslehurst | A nationally representative study of maternal obesity in England, UK: trends in incidence and demographic inequalities in 619 323 births, 1989-2007[END_REF].

Current guidance on postpartum weight loss recommends that advice for mothers should be tailored to personal circumstances and take account of the demands of caring for a baby including fatigue and any co-existing health problems (NICE, 2010a). A systematic review commissioned by NICE (2010b) included five randomised control trials (RCTs) [START_REF] Leermakers | Reducing postpartum weight retention through a correspondence intervention[END_REF][START_REF] Lovelady | The effect of weight loss in overweight, lactating women on the growth of their infants[END_REF][START_REF] O'toole | Structured diet and physical activity prevent postpartum weight retention[END_REF][START_REF] Ostbye | Active mothers postpartum: a randomized controlled weight-loss intervention trial[END_REF][START_REF] Kuhlmann | Weight management interventions for pregnant or postpartum women[END_REF] that examined postpartum weight loss interventions but all were based in the US and not noted to recruit specifically from disadvantaged groups.

It is likely that adherence to weight loss programmes will be more challenging for low income mothers and studies suggest that the transition from pregnancy to the postpartum phase may be associated with a poorer diet [START_REF] George | Food choices of low-income women during pregnancy and postpartum[END_REF]. There are many challenges in identifying ways to increase physical activity, restrict intakes of food and drink (when home based) and cope with the demands of child rearing. Multiple physical (and often psychological) morbidities and social isolation may mean that a standard weight loss regime is less acceptable [START_REF] Peterson Ke Sorenson | Design of an intervention addressing multiple levels of influence on dietary and activity patterns of low-income, postpartum women[END_REF]. Little is known about the response of low income, postpartum women to weight loss interventions in the UK and evidence from trials is absent.

However, undertaking behavioural interventions trials in disadvantaged communities is often characterised by recruitment difficulties and robust design strategies for full trials would benefit from exploratory work as described in the MRC guidance for complex interventions (Craig et al., 2008).

The aim of the current work was to evaluate the feasibility of undertaking a randomised controlled trial of a weight loss programme (WeighWell) in postpartum women living in areas

Methods

The study aimed to recruit 60 women who were not pregnant, were 6-18 months postpartum with a BMI >25kg/m 2 and living in areas of moderate to high deprivation (Scottish Index of Multiple Deprivation (SIMD) deciles 1-5) (Scottish Government, 2009) based on postcode.

Sample size was chosen to represent 10% of that required to demonstrate a difference in 5% weight loss at 95% power in a definitive trial. This had been estimated to be 303 subjects in each group, based on the body weight variation of 16-50 year old women with a BMI over 25kg/m 2 in the 2003 Scottish Health Survey.

Recruitment strategies comprised visits to community groups; writing to GP practices who have at least 30% of their patients classified as living within the most deprived 15% of SIMD (GP, health visitor and practice manager) and support workers (who wrote directly to postpartum women living in appropriate SIMD areas); newspaper advertising and posters in community settings. Recruitment materials offered a Freephone number. Interested individuals were telephone screened for eligibility [by AC], sent a participant information sheet and given a baseline appointment.

The primary outcomes of the study were to assess the feasibility and acceptability of the study procedures (including assessment method and intervention delivery). The following procedures were undertaken at baseline and follow-up.

• Height, weight, waist circumference and skinfold measures

• Physical activity assessment using a SenseWear TM physical activity monitor (Bodymedia Inc., Pittsburgh, PA, USA) worn for 7 days prior to assessment

• Fasting blood sample (for plasma vitamin C analysis)

• Questionnaires on socio-demographic background, dietary intake, physical activity, and psychosocial parameters (self efficacy and the theory of planned behaviour constructs on diet and physical activity).

Only the results from the first two of these are reported in this paper. Participants were then randomised to an intervention or comparison group using a 1:1 random sampling procedure in SPSS (Version 17.0, SPSS Inc., Chicago, IL, USA) by the trial manager. Assessments were performed, primarily within a hospital setting but on occasions within the participants' home, by a research assistant blinded to randomisation allocation.

Intervention and comparator:

All participants received a weight loss booklet (British Heart Foundation, 2006). Participants randomised to receive the 12 week intervention were allocated a trained lifestyle counsellor who delivered the intervention by 3 face to face consultations at monthly intervals (at a location most convenient for the participant).

Between consultation contact was maintained with the intervention group by the lifestyle counsellor via a minimum of 3 structured telephone calls to identify progress towards goals, achievements and challenges and to provide positive feedback and support.

Motivational interviewing techniques [START_REF] Rollnick | Motivational interviewing[END_REF] were employed and a personalised dietary prescription of estimated energy requirements minus 500 kcals was calculated with verbal and written guidance on food groups, frequency of consumption and portion size. Personalised physical activity goals were also set towards achieving 150 minutes of moderate to vigorous activity per week. Participants were provided with 4 week walking plans, a pedometer and a weight logbook for self monitoring.

The comparison group received no further contact beyond the weight loss booklet until follow-up assessment at 12 weeks. The group received a one-off consultation with a lifestyle counsellor after follow-up assessment.

Post-study feedback was sought via semi-structured telephone interviews on a sub-sample of 13 participants from each group. These were undertaken by a research assistant not involved in the study.

Quantitative data analysis was undertaken using SPSS (Version 17.0) utilising ANOVA to assess changes between baseline and follow-up. There was no imputation for missing values; i.e. for the feasibility study's indicative estimate of effect, we did not do an intention to treat analysis but looked simply at differences between baseline and 12-weeks for those participants for whom weight-loss data were available at both points. Chi-square analysis was undertaken for categorical variables.

Ethical approval was provided by the Fife and Forth Valley NHS Research Ethics Committee 09/S0501/44.

Results

Subjects

Between August 2009 and February 2010, 142 women responded to the study publicity.

Most were ineligible for participation (n=75), largely due to area of residence (SIMD decile).

Sixty five women (46%) met the inclusion criteria and were appointed for a baseline visit but 11 women subsequently declined to participate. At baseline assessment two women were excluded due to low BMI. Of the 52 participating women, 29 were randomised to the intervention group and 23 to the control group (Figure 1).

Loss to follow-up was 31% (24% and 39% for intervention and control group respectively)

including three participants who became pregnant during the study and were excluded. Thirty six participants completed follow up assessments by May 2010.

No significant group differences were identified at baseline for age, BMI, ethnicity, education level, household income, SIMD category, employment status or smoking status (Tables 1 and2).

Feasibility of assessment measures

Height, weight and waist circumference were obtained from all participants who took part in baseline and follow up assessments. Skinfold measurements were attempted in all participants and obtained from 37 (71%) at baseline and 26 (72%) at follow up. The remainder were not collected due to measurement difficulties. Fasting blood samples were obtained from 35 (67%) participants at baseline and 20 (56%) at follow up. The activity monitors were worn for a minimum of 4 days by 49 (94%) at baseline with a similar proportion at follow up (97%).

Feasibility of intervention delivery

The intervention face to face consultations (3) and telephone contact calls (3) were successfully delivered to 100% of the Intervention Group who completed the study. Most (76%) of the participants were seen at home.

Potential efficacy

Body weight loss was achieved by 73% of the intervention group compared to 36% of the comparison group (Table 2). Weight loss of clinical significance (reduction of 5% body weight SIGN, 2010) was achieved by 9% of the intervention group, compared to 0% in the comparison group. Whilst the study was not powered to show change between intervention and comparator there was a significantly greater change in the intervention compared to the comparison group for body weight, BMI and % body fat. No differences were detected between groups for change in waist circumference, nor objectively measured physical activity.

Post-study interviews

Post-study interviews revealed that all participants reported their experience positively overall, regardless of group. However, many comparison group participants noted a feeling of disappointment about their allocation despite acknowledging their awareness of the randomisation procedure prior to their enrolment on the study.

Baseline and follow-up assessments were largely acceptable, with most difficulties relating to either the discomfort experienced whilst wearing the SenseWear TM physical activity arm band and/or a small number of questionnaire items. However, a number of positive comments were received overall about the usefulness of the feedback received from the physical activity monitors.

Whilst the comparison group received only a weight loss booklet, many did report having made some improvements to their lifestyle, either as a result of having an increased awareness of aspects of their lifestyle requiring improvement after having carried out the assessment procedures and/or after reading the British Heart Foundation booklet provided.

The intervention was particularly well received with respect to the format (one-to-one rather than group sessions, duration and frequency), the supportive approach of the counsellors, and the literature provided, with all recipients describing the intervention as useful.

Intervention group participants all reported having made sustained improvements to aspects of their diet (e.g. increases in fruit and vegetable intake and cooking of fresh food; and reductions to portion sizes, frequency of eating out, and intakes of snacks and sugary foods and drinks). In most cases these were reported to have extended to the wider family.

Although not as consistent as the reported dietary changes, most also reported having improved their levels of physical activity.

Discussion

The findings of this feasibility study suggest the potential efficacy of the programme for initiating postpartum weight loss. Though not designed or powered to provide evidence of effect, the study showed a promising weight loss over the 12 week period by the intervention group was modest and in contrast to the weight gain found in the comparison group. The comparison group had all received written information on weight loss, a condition of ethical approval, so cannot be regarded as a true control group receiving usual care only. However, the results suggest that without health professional support the norm may well be to gain weight, despite a perception of having made positive lifestyle changes. These results are similar to a recent intervention trial on prevention of weight gain in young mothers (with primary school aged children) which reported a significant weight loss of -0.20kg after a 12 month intervention compared to a gain of 0.83kg in their control group [START_REF] Lombard | A low intensity, community based lifestyle programme to prevent weight gain in women with young children: cluster ransomised trail[END_REF]. Such findings highlight the challenges of avoiding weight gain in societies where social contacts focus on encouraging eating, drinking and sedentary activities.

The current work raises several considerations for the design of a future RCT. The response of women to recruitment strategies suggest that current approaches might be enhanced by identifying eligible women at postnatal discharge and sending personal contact letters through GPs. Loss to follow up was similar to that reported by [START_REF] Leermakers | Reducing postpartum weight retention through a correspondence intervention[END_REF] Those who completed the study expressed dissatisfaction at their allocation even though women were offered a consultation with a counsellor after completion of follow up measures. One potential solution to this in a future trial would be the use of an active comparison group, which improves loyalty by providing a similar level of support to that provided in the intervention group but in an area that is not expected to affect weight loss, such as a focus on positive aspects of baby development or other aspects of maternal wellbeing such as stress reduction.

The measurements utilised were intended to provide subjective and objective measures of factors influencing weight loss. A future trial would have weight loss as its primary outcome and measuring this was not a problem in this feasibility study. However, difficulties in obtaining skinfold thickness measurements (as also reported by [START_REF] Gray | Skinfold thickness measurements in obese subjects[END_REF] and fasting blood analysis suggests these measures may be of limited use in a future trial. In addition, these may have added to subject burden as they necessitated a visit to the research centre and may partially account for interested participants withdrawing. There was a clear preference expressed for intervention visits to be at home and future work should reconsider essential measurements in this light. Given the importance of body fat as an outcome measure, this should include reconsideration as to the methods of body fat measurement. Bioelectrical impedance analysis may offer a quick and portable alternative less prone to observer bias than skinfold thickness measurements, which would be important in a larger RCT [START_REF] Deurenberg | Body Composition[END_REF].

Whilst it is recognised that home visits may be costly, women recruited to studies of postpartum weight loss have been reported as having little time available, competing responsibilities above their own health, and find rigid interventions (such as group based classes) difficult to attend [START_REF] Carter-Edwards | Barriers to adopting a healthy lifestyle: insight from postpartum women[END_REF]. A recent trial utilising diet and activity classes and telephone counselling found no difference in weight change between intervention and control groups noting that engaging women during this busy period is challenging and concluding that home based interventions may be more successful [START_REF] O'toole | Structured diet and physical activity prevent postpartum weight retention[END_REF].

This feasibility study was aimed at delivering a 3-month intervention to explore intervention delivery, recruitment and retention with post-partum women and, additionally, to give an indication of the intervention's ability to support weight loss. The results are encouraging although a future RCT should embrace wider, personalised recruitment strategies and the development of specific approaches to improve study retention over a clinically relevant intervention period.

  of social disadvantage served by NHS Tayside by conducting a pilot intervention to examine recruitment and retention, feasibility of assessment measures, intervention delivery, and potential efficacy. The study was not designed or analysed to demonstrate a definitive change in body weight. The study used a 1:1 parallel-group randomised controlled trial design.

Table 1 : Baseline characteristics 346 Mean ± St. Deviation (range), or n (%) 1 Intervention n=29 Comparison n=23

 1

	Age (years)

Acknowledgements

The authors acknowledge the financial support of the Medical Research Council (Ref GO701771), and NHS Research Scotland (NRS) through NHS Tayside, to carry out this work. The authors would like to thank Amy Gregor who assisted with recruitment and screening of participants and in the development of study materials and Margaret Robertson, the project lifestyle counsellor. They would also like to thank Professor Peter Howat, Director of the Centre for Behavioural Research in Cancer Control at Curtin University, Australia for guidance in project design and assessment.

Conflict of interest

The authors declare no conflict of interest.


Giacomo Baldi
email: giacomo.baldi@esrf.fr

Aldo Fontana

Flavio Rossi

Giulio Monaco

Raman scattering investigation of the boson peak in a sodium silicate glass

Keywords: boson peak, glass, elasticity boson peak, glass, elasticity pm-pml

Raman scattering is used to investigate the vibrational spectrum of a sodium silicate glass around the boson peak frequency range at temperatures between 10 and 450 K. The comparison with the density of states measured with coherent neutron scattering allows one to determine the Raman coupling function. This quantity presents a linear frequency dependence in the boson peak region and a negligible temperature dependence, confirming similar observations in other glasses. The Raman spectra at different temperatures scale according to the Debye frequency determined from the sound velocity measured at terahertz frequency with inelastic x-ray scattering. This result confirms previous neutron scattering data and the importance of measuring the elastic properties of the glass in the proper frequency range.

Introduction

Topologically disordered solids are characterized by the lack of long range structural order. In spite of the absence of periodicity, these systems can sustain the propagation of sound up to terahertz frequencies [1]. However their vibrational dynamics is strongly affected by the presence of disorder. Particularly evident is the appearance of The boson peak variation as a function of an external control parameter has been deeply investigated in the last two decades. In particular the BP evolution has been studied as a function of temperature [1,2,3], pressure [4,5] or density [6,7,8],

varying the sample preparation [9] and during chemical vitrification [10]. An increase in sample density is usually accompanied by a shift of the BP towards higher frequencies associated to a reduction of its intensity. In the case of vitreous silica the same behavior is observed as the temperature is increased [2,3].

A major question is whether the BP shift can be explained by corresponding variations in the macroscopic elastic medium properties, such as density and sound speeds. Using nuclear inelastic scattering Monaco et al. [6] have shown that in permanently densified samples the BP shift follows the variation of the Debye frequency D ν , in the range of densities where local structure modifications can be neglected. A similar result is obtained in recent numerical simulations of systems with a varying degree of fragility [11]. On the contrary a pressure dependence of the BP frequency stronger than the D ν variation has been reported by Niss et al. [4] in studies of polymeric glasses.

In a recent work [12] we have shown that the comparison of the BP variations to those of the macroscopic continuum medium requires a careful determination of the elastic properties of the glass. Specifically the sound velocity, which is used to estimate the Debye frequency, needs to be measured in a frequency range where contributions from anharmonicity or relaxation processes can be neglected. This can be accomplished by measuring the sound velocity at high frequency, in the terahertz range, by means of inelastic x-rays scattering.

Experimental

The silicate glass sample, 60%SiO 2 -40%Na 2 O, has been prepared using the standard melt-quenching technique. Pure SiO 2 and Na 2 CO 3 powders have been melted at 1600 o C in air in a Pt crucible. The obtained sample has been annealed for 6 h at the glass transition temperature (T g ~ 700 K [13]). A cubic shaped sample of dimensions 5x4x4 mm 3 has been cut and optically polished. The inclusion of Na in the SiO 2 network has the effect of inducing a strong reduction of the glass transition temperature and an increase of the fragility of the system (m ~ 50 [14]).

The elastic properties of the glass have been studied by means of Brillouin light (BLS) and x-ray (IXS) scattering as a function of temperature, as previously reported in ref. [12]. The BLS signal in right angle geometry has been measured using a Sopra DPDM monochromator. The spectrometer employs an incident wavelength of 5145 Å and is operated in single pass configuration at the 11th order, providing a resolution of 1.2 GHz. The right angle geometry allows one to measure both the longitudinal and the transverse sound velocities. The value of the longitudinal sound velocity around room temperature has been checked in backscattering geometry. For this test we employed a Sandercock type (3+3)-pass tandem Fabry-Perot on the experimental setup and data analysis can be found in ref. [12].

Discussion

The Raman coupling function

The Raman intensity, I R , is conveniently written in terms of the reduced Raman intensity I red :

[ ] ( , ) ( , ) 1 red R I I T n T ν ν ν = + (1)

Elastic properties and the scaling of the boson peak

The comparison between the BLS and IXS data allows one to investigate the temperature evolution of the elastic properties of the system in different frequency ranges, some tens of GHz for the BLS experiment and a few THz for the IXS one.

The temperature dependence of the sound velocity, both longitudinal and transverse, normalized to its low temperature value, is plotted in figure 3 B ~ 3 and A a system dependent quantity [15]. The parameter A can be estimated from the BLS data, which correctly obey the Cauchy relation [12].

Figure 3 shows that the sound velocity in the GHz frequency range is strongly temperature dependent and thus affected by anharmonicity or relaxation processes that tend to reduce the elastic modulus at high temperature. On the contrary, in the THz regime the sound velocity appears to be temperature independent within the experimental accuracy. This observation is of great relevance when the temperature or pressure dependence of the boson peak is compared to the corresponding evolution of the elastic properties of the medium. This comparison can be done estimating the Debye frequency:

3 q v 3 ( ) v ( ) 2 4 D D D D T T m ρ ν π π = = (3)
where q D and v D are the Debye wavevector and sound velocity respectively and m is the average atomic mass. In the temperature range here investigated, below the glass transition temperature, the density of the sodium silicate glass doesn't change appreciably. For this reason the temperature dependence of the Debye frequency is entirely due to the variation of the sound velocity.

On general grounds the sound velocity can depend on temperature because of the presence of relaxation processes or anharmonicity. Concerning the contribution of anharmonic terms we can distinguish between a quasi-harmonic part and a "purely" anharmonic contribution. The quasi-harmonic term may induce a variation of the sound velocity because the elastic constants of the glass rearrange to different values when the temperature is changed. This contribution is expected to be frequency independent. With "purely" anharmonic contribution we indicate the effect of terms in the expansion of the inter-atomic potential which are of third and higher order in the atomic displacement around the equilibrium configuration. This contribution is frequency dependent and gives rise to a temperature dependence of the sound velocity and to damping of the sound waves [17].

Because of the frequency dependence of the sound velocity we may conclude that also the Debye frequency is frequency dependent. However here the Debye frequency is used to estimate the temperature evolution of the elastic properties of the continuum medium. We should thus measure it in a frequency range where it is not affected by "purely" anharmonic terms or by relaxation processes. This is accomplished by measuring it in the terahertz frequency range. It is worth noting that the sound velocity may still be temperature dependent in the terahertz range, because of the presence of a quasi-harmonic mechanism, due, for instance, to a structural rearrangement of the system with temperature or to a temperature dependence of the density. This is not the case in the silicate glass here studied, as shown by the temperature independence of the sound velocity determined with IXS.

Once the Debye frequency is known, one can rescale the measured density of vibrational states, ( ) g ν , plotting it as a function of the quantity / D ν ν . In order to maintain the correct normalization, the density of states in the new variable is: ( / ) ( )

D D g g ν ν ν ν = ⋅ %
. The reduced density of vibrational states,

  vibrational modes over the Debye level at terahertz frequencies, usually called the boson peak (BP).

  In this paper we present new data on the vibrational spectrum of a sodium silicate glass in the BP range, measured with Raman scattering at temperatures between 10 and 450 K, in the glassy state. The comparison of these new data with neutron scattering measurements allows us to determine the Raman coupling function, which shows an almost linear frequency dependence and a negligible temperature dependence. The Raman data give further support to the importance of measuring the elastic properties of the medium in the proper frequency range.

  spectrometer works with an incident wavelength of 532 nm and has an energy resolution ~ 0.6 GHz. The sound velocity in the THz regime has been measured by means of IXS. The experiment has been performed at the beamline ID16 of the European Synchrotron Radiation Facility. An incident beam of 23.7 keV energy is monochromatized by the(12,12,12) reflection of a Si crystal, providing an energy resolution of 1.4 meV. The sound velocity has been measured at a small exchanged wavevector, q = 0.12 Å -1 .Information on the density of vibrational states is obtained by means of Raman and inelastic neutron scattering experiments. The Raman measurements in HV geometry were performed using a standard experimental set-up Jobin Yvon U1000.The spectra were measured at temperatures in the range from 10 K to 450 K. The intensity of the measured spectra is plotted as a function of frequency in figure1. The curves are normalized to the high frequency peaks, outside the frequency range shown in the figure. The spectra show a prominent boson peak at a frequency ν ~ 1.6 THz, best visible at high temperatures. The neutron scattering experiment has been performed at the IN4 spectrometer of the Institut Laue Langevin in Grenoble. Details

  population factor for phonons. In a disordered system, as a glass, the reduced intensity is related to the density of vibrational states, ( ) accounting for the light-vibration coupling.The neutron inelastic scattering technique allows to obtain a reliable determination of the density of vibrational states ( ) g ν , as explained in ref.[12]. The comparison between the Raman and the neutrons spectra thus allows to determine theRaman coupling function ( , )C T ν , which is plotted in figure2. The coupling function is a smooth function of frequency and it increases approximately linearly with frequency in the boson peak range. Moreover its shape is not affected by temperature, whose effect is only a slight shift of ( , ) C T ν to higher values as T is increased.

  . The transverse sound velocity at terahertz frequency cannot be directly measured because the IXS technique probes the longitudinal current correlation function. The plotted values are estimated exploiting the Cauchy relation: M A BG = + and the shear modulus respectively and ρ is the mass density. This shown to hold for a variety of materials at every frequency, with

2 ( ) / g ν ν , is plotted in figure 4

 24 as a function of the variable / D ν ν . The figure shows a comparison between the Raman (top) and inelastic neutron scattering (bottom) data. In the left column the Debye frequency calculated from the IXS sound velocity, IXS D ν , is used to scale the figure axis. The Raman intensity is scaled assuming that the coupling function, ( , ) C T ν, is linear in frequency, as confirmed by the comparison with the neutron data (see figure2). The left column of figure4shows that the boson peak in is temperature independent in the temperature range here explored. This is confirmed by both the Raman and the neutron data. Also the elastic properties of the continuum medium are not affected by temperature, and they are properly described by IXS D ν . A temperature dependence of the reduced density of states can be seen below the boson peak frequency, in both the Raman and neutron data. This quasi-elastic contribution is probably associated to the same anharmonic or relaxation processes that affect the sound velocity at GHz frequencies.On the right column of figure4the scaling is performed using the Debye frequency determined from the BLS data, BLS D ν . The temperature dependence of this quantity induces a spurious variation of the scaled reduced density of states, appreciable in both the Raman and the neutrons data. The figure allows to better appreciate the importance of using sound velocity values which are not affected by relaxation or anharmonic processes, when these are employed to estimate the elastic properties of the continuum medium.ConclusionsThe investigation of the vibrational dynamics of a sodium silicate glass by means of Raman scattering further supports the conclusions obtained with inelastic neutron scattering. The comparison of the spectra obtained with the two techniques allows us to determine the Raman coupling function, which is marked by a linear frequency dependence in the boson peak region. This result is used to estimate the reduced vibrational density of states from the Raman intensity and to scale it with the Debye frequency. This quantity is independently determined from the sound velocity obtained with BLS and IXS.

A

  proper scaling of the boson peak is obtained using the IXS values of the sound velocity, which are not affected by anharmonicity or relaxation processes. This conclusion is confirmed by both neutrons and Raman scattering. The present contribution indicates the importance of measuring the elastic properties of the glass in the proper frequency range if a characterization of the elastic continuum medium is desired.

Figure captions:Figure 1 (

 1 Figure captions:

Figure 2 (

 2 Figure 2 (color online). Raman coupling function as a function of frequency at the indicated temperatures. The line is a guide for the eye showing a linear dependence.

Figure 3 ( 1 .

 31 Figure 3 (color online). Temperature dependence of the longitudinal (panel A)) and transverse (panel B)) sound velocities, normalized to their low temperature values. Squares: IXS data, circles: BLS data in right angle geometry. Triangle: BLS point measured in back scattering. The low temperature sound velocity values for the BLS and IXS data differ because of the negative dispersion effect [12,16]. They have been determined from a linear fit of the temperature dependence to be: ,0 v (5784 27) BLS L = ± m s -1 , ,0 v (3280 35) BLS T = ± m s -1 , ,0 v (5454 26) IXS L = ± m s -1 ,

Figure 4 ((((

 4 Figure 4 (color online). Left column: upper panel: reduced Raman intensity as a function of / IXS D ν ν ; lower panel: reduced density of states measured with inelastic neutron scattering as a function of / IXS D ν ν . Right column: the same quantities of the left column rescaled according to the Debye frequency determined from the BLS sound velocity values, BLS D ν .

http://mc.manuscriptcentral.com/pm-pml Philosophical Magazine & Philosophical Magazine Letters


PhD, ELS HOUBEN, MSc Vicky De Preter

MSc Karen Windey

MSc, AND Anja Luypaerts

Ph.D Kristin Verbeke
email: kristin.verbeke@uz.kuleuven.ac.be

ANALYSIS OF THE URINARY GLUCOSE-[ 15 N, 15 N]-UREIDE CONTENT IN THE STUDY OF THE LACTOSE-[ 15 N, 15 N]-UREIDE METABOLISM IN HEALTHY HUMANS GC-MS ANALYSIS OF GLUCOSE-[ 15 N, 15 N]-UREIDE

Keywords: gas chromatography -mass spectrometry, OCTT: orocaecal transit time, TLC lactose-[ 15 N, 15 N]-ureide, ammonia metabolism, stable isotopes, GC-MS

Background/Objectives: Lactose-[ 15 N, 15 N]-ureide is used to study the fate of the colonic ureanitrogen metabolism. During the passage through the gastrointestinal tract, lactose ureide is hydrolysed to glucose ureide, which is absorbed to a limited extent from the small intestine and is excreted urinarily. In the present study, a procedure has been developed to quantify the urinary excretion of glucose-[ 15 N, 15 N]-ureide. In addition, urine and faecal samples obtained during a dietary intervention study with the prebiotic lactulose were retrospectively analysed.

Subjects/Methods: The glucose ureide and lactose ureide content was measured by GC-MS in nineteen healthy volunteers. After consumption of a standard test meal containing 75 mg lactose-[ 15 N, 15 N]-ureide, 6 healthy volunteers performed a fractionated 24h urine collection to investigate the urinary excretion of glucose-[ 15 N, 15 N]-ureide. In 13 volunteers, the effect of lactulose administration on the urinary excretion of glucose-[ 15 N, 15 N]-ureide was analysed.

Results:

The urinary excretion of glucose-[ 15 N, 15 N]-ureide reached its maximum level in the 3-6h urine collection and decreased in the 6-9h urine. The label was still detectable in the 9-24h urine collection. The cumulative excretion of 15 N-labelled glucose ureide after 24h amounted 12.91 %. No significant differences in glucose-[ 15 N, 15 N]-ureide excretion were found in either of the urine fractions after administration of lactulose compared to baseline. In none of the urine samples lactose-[ 15 N, 15 N]-ureide was detected.

Conclusions:

In conclusion, the results obtained in the present study indicated that the percentage dose glucose-[ 15 N, 15 N]-ureide recovered in urine is rather constant and not influenced by the presence of lactulose.

INTRODUCTION

Lactose ureide labelled with 13 C on the urea moiety has been proposed as a substrate for the determination of orocaecal transit time (OCTT) by Heine et al. [START_REF] Heine | A novel stable isotope breath test: 13C-labeled glycosyl ureides used as noninvasive markers of intestinal transit time[END_REF]. Its application is based on the observation that the bond between the urea and sugar moiety in lactose ureide is completely resistant to human digestive processes, yet it is hydrolysed by the intestinal microbiota upon arrival in the colon. The labelled urea generated in this way is rapidly hydrolysed to 13 CO 2 and NH 3 .

On the basis of the same principle, its 15 N-labelled analogue has been applied as a vehicle to introduce a known amount of urea-nitrogen into the colon. The labelled NH 3 can either be used by the colonic microbiota for their own metabolism which is followed by faecal 15 N-excretion or it can be absorbed through the colonic wall and after conversion in the liver to labelled urea, be excreted in the urine [START_REF] Jackson | Metabolism of lactose-[13C]ureide and lactose-[15N,15N]ureide in normal adults consuming a diet marginally adequate in protein[END_REF] (Figure 1). In this way, lactose-[ 15 N, 15 N]-ureide can be used to evaluate the fate of the colonic urea-nitrogen metabolism. Using the same molecule, Jackson et al. demonstrated that bacterially derived amino acids from [ 15 N, 15 N]-urea are available for colonic absorption and thus for the host [START_REF] Jackson | Transfer of (15)N from oral lactose-ureide to lysine in normal adults[END_REF]. We have proposed this molecule as a biomarker to evaluate the influence of pre-and/or probiotic administration on the colonic ammonia metabolism. It has been shown that bacterial activity and/or growth is stimulated upon administration of pre-and/or probiotics which is reflected in a shift from urinary to faecal 15 Several methods have previously been applied to measure the 15 N-enrichement and total nitrogen content in urine and faeces, however, they do not all allow discrimination between the different chemical forms of the marker. Ruemmele et al. showed that during the passage through the gastrointestinal tract, lactose ureide is converted by β-galactosidase, located in the brush border of the small bowel, to galactose and glucose ureide, and that glucose ureide is absorbed to a limited extent from the small intestine and is excreted urinarily without being further metabolised [START_REF] Ruemmele | Metabolism of glycosyl ureides by human intestinal brush border enzymes[END_REF]. The analytical methodology used by [START_REF] Jackson | Metabolism of lactose-[13C]ureide and lactose-[15N,15N]ureide in normal adults consuming a diet marginally adequate in protein[END_REF] did not allow to differentiate between 15 N originating from urea or glucose-[ 15 N, 15 N]-ureide, leading to their conclusion that a limited amount of labelled [ 15 N, 15 N]-urea (5 %) can be absorbed unchanged from the colon. Morrison et al. have qualitatively identified glucose-[ 13 C]-ureide in urine after administration of 13 C-labelled lactose ureide using thin layer chromatography (TLC). They estimated the 13 C-recovery in urine at approximately 15% of administered dose [START_REF] Morrison | Gastrointestinal handling of glycosyl [13C]ureides[END_REF]. As a consequence, it is likely that 15 N-labelled glucose ureide will be excreted in urine after administration of 15 N-labelled lactose ureide and it might be necessary to correct urinary 15 N-data for the presence of glucose-[ 15 N, 15 N]-ureide.

Therefore, an analytical procedure using gas chromatography -mass spectrometry (GC-MS) technology has been developed to quantify in a prospective study the urinary excretion of glucose-[ 15 N, 15 N]-ureide after oral administration of lactose-[ 15 N, 15 N]-ureide. In addition, urine and faecal samples obtained during a dietary intervention study with the prebiotic lactulose were retrospectively analysed.

MATERIALS AND METHODS

GC-MS analysis

Substrates

Lactose-[ 15 N, 15 N]-ureide, glucose-[ 15 N, 15 N]-ureide and the corresponding unlabelled substrates were synthesized according to the method of Schoorl [START_REF] Schoorl | Les ureides (carbamides) des sucres[END_REF] as modified by Hofmann [START_REF] Hofmann | Ueber den Abbau von glucoseureid durch Bakterien[END_REF] with [ 15 N, 15 N] urea obtained from Euriso-top (Saint-Aubain Cédex, France). Sugar ureides are the condensation products of a reducing sugar and urea in mild aqueous acid. Their synthesis is simple and avoids the use of toxic chemicals, making them safe for use in clinical practice.

Absence of [ 15 N, 15 N]-urea, lactose or glucose-[ 15 N, 15 N]-ureide in the synthesis of lactose-[ 15 N, 15 N]ureide, and absence of [ 15 N, 15 N]-urea or glucose in the synthesis of glucose-[ 15 N, 15 N]-ureide was confirmed using TLC [START_REF] Morrison | Rapid quality control analysis of (13)C-enriched substrate synthesis by isotope ratio mass spectrometry[END_REF].

Chemicals

Meso-inositol and n-heptane were supplied by Vel (Leuven, Belgium), whereas acetone was obtained from Chem-Lab NV (Zedelgem, Belgium). NH 2 OH.HCl was purchased from Sigma-Aldrich (St. Louis, USA), pyridine and BSTFA-TMCS (99:1) were obtained from Pierce (Rockford, USA).

Sample preparation

The glucose ureide and lactose ureide content was measured by gas chromatography-mass spectrometry (type time-of-flight (TOF)) technology. Therefore, 40 µl internal standard (meso-inositol (100mg/100ml)) was added to 960 µl of a standard solution (= final concentration range of glucose ureide and lactose ureide between 0 and 30 mg/l). This solution was diluted with 3 ml aceton, mixed for 1 min and centrifuged at 3000 rpm for 20 min to deproteinized the samples. One ml aliquots were evaporated to dryness and 100 µl oxime reagent (NH 2 OH.HCl in pyridine, 25 mg/l) was added to the sample, mixed for 1 min and heated for 30 min at 80°C. The reaction was stopped at -20°C (10 min) and the samples were evaporated under a stream of nitrogen. Derivatisation was accomplished by adding 50 µl of BSTFA+TMCS (99:1) to the dried samples, thoroughly mixed and heated at 80°C. After 35 min, samples were cooled down to room temperature. After adding 250 µl pyrogeen-free H 2 O, samples were extracted with 300 µl n-heptane and 0.5 µl of this solution was analysed on a GC-MS (Interscience, Louvain-la-Neuve, Belgium). The analytical column was a 30 m x 0.25 mm i.d., 0.25 µm AT5-MS (Alltech Associates, Deerfield, USA). Helium GC grade was used as a carrier gas with a constant flow of 1.3 ml/min. The oven temperature was programmed to increase from 200°C (1 min), with 5°C/min to 270°C (isothermal for 15 min). Mass spectrometric detection was performed in full scan mode from m/z 35 to m/z 600 at 10 scans/sec. Xcalibur-software was used for the automatisation of the GC-TOF-MS and for data acquisition. The results for glucose-ureide and lactose ureide were expressed as percentage of the administered dose recovered in the different urine fractions.

Study design

Subjects

Nineteen healthy volunteers (10 men and 9 women; mean age 22) were included in the study. None of the subjects had a history of gastrointestinal or metabolic disease or previous surgery (apart from appendectomy). The subjects were free of antibiotics or any other medical treatment influencing gut transit or intestinal flora for at least 3 months before the start of the study. The Ethics Committee of the University of Leuven approved the study and all subjects gave informed consent.

Prospective study to quantify the glucose-[ 15 N, 15 N]-ureide excretion

Six healthy volunteers (3f / 3m) were included and performed one test. On the day of the test, they provided a basal urine sample after which they received a standard pancake test meal (8.4 g proteins, 11.2 g fat and 26.7 g carbohydrates (243.5 kcal)) containing 75 mg lactose-[ 15 N, 15 N]-ureide.

After intake of the test meal, a fractionated 24h urine collection was performed (0-3h, 3-6h 6-9h and 9-24h) to investigate the urinary excretion of glucose-[ 15 N, 15 N]-ureide in the different urine fractions.

Influence of lactulose on the glucose-[ 15 N, 15 N]-ureide excretion

In a retrospective study, urine and faecal samples obtained from 13 healthy volunteers (6f / 7m) who participated in a study to investigate the effects of the prebiotic lactulose, were analysed. These volunteers had consumed three times a standard pancake test meal labelled with 75 mg lactose-[ 15 N, 15 N]-ureide; the first time in baseline conditions, the second time together with 10g lactulose and the third time after a 4-week dietary intervention period with lactulose (2x 10g/d). Each time, the volunteers provided a basal urine sample before consumption of the test meal and collected all urine for 48h (0-24h and 24-48h fractions) and stools for 72h.

Samples

All urine was collected in recipients to which neomycin was added for prevention of bacterial growth.

After measurement of the volume, samples were taken and stored at -20 °C until analysis. Upon delivery of the faecal samples, all stools collected on the same day were combined, diluted fivefold with sterile pyrogen-free water and homogenized. The homogenate was ultracentrifuged at 25000g during 120 min (MR22i, Jouan, St-Herblain, France) and the supernatans was subsequently filtered through a 0.2-µm syringe filter (Supor Acrodisc 32, Gelman Sciences, Ann Arbor, USA) in order to discard the ultimate faecal rests and the bacteria. The final filtrate was used for determination.

Aliquots were frozen at -20°C.

For analysis, 960 µl of urine or faecal extract were prepared according to the standard solution to determine the excretion of glucose-[ 15 N, 15 N]-ureide and lactose-[ 15 N, 15 N]-ureide.

Statistical analysis

Results were expressed as median and interquartile range (IQR). The statistical analysis was performed with SPSS software (SPSS 16.0 for Windows; SPSS Inc., Chicago, IL, USA). Given the low number of subjects in the treatment groups, non-parametric statistical analysis was used. Statistical evaluation of the data was performed by applying the Wilcoxon and Mann-Whitney test. The level for statistical significance was set at p<0.05.

RESULTS

GC-MS analysis

GC-MS analysis of a derivatisation reaction of glucose ureide showed a peak eluting at 11.02 min which was identified as the internal standard and a peak at 15.37 min, identified as glucose ureide.

Similarly, lactose ureide was found to elute from the column at 24.85 min. A calibration curve was constructed using dilutions ranging from 0 -30 mg/l (r²=0.9923). The limit of detection was established at 1.25 mg/l. A good interday and intraday reproducibility was found in the analysis of the urine samples (<10% RSD)

Prospective study to quantify the glucose-[ 15 N, 15

N]-ureide excretion

Figure 2 shows the glucose-[ 15 N, 15 N]-ureide excretion in the different urine fractions. Within the first 3h of ingestion of the marker, a small fraction of the labelled glucose-ureide (i.e. 0.64 % dose glucose-[ 15 N, 15 N]-ureide (IQR 0.21 -0.86)) was already excreted in the urine indicating an early absorption from the upper small intestine. Urinary excretion reached its maximum level in the 3-6h urine collection (5.45 % dose glucose-[ 15 N, 15 N]-ureide (IQR 4.89 -6.25) and decreased in the 6-9h urine collection to 4.03 % dose glucose-[ 15 N, 15 N]-ureide (IQR 3.74 -5.46). The label was still detectable in the 9-24h urine collection (3.27 % dose glucose-[ 15 N, 15 N]-ureide (IQR 1.53 -3.90). The cumulative excretion of 15 N-labelled glucose ureide after 24h amounted 12.91 % dose glucose-[ 15 N, 15 N]-ureide (IQR 11.40 -15.30) and is shown in Figure 3. In none of the samples lactose-[ 15 N, 15 N]ureide was detected.

Influence of lactulose on the glucose-[ 15 N, 15 N]-ureide excretion

The urinary and faecal excretion of glucose-[ 15 N, 15 N]-ureide in the three different test situations is represented in Table 1. The individual recovery of glucose-[ 15 N, 15 N]-ureide over 24h is shown in Figure 4. No statistically significant differences were found in either of the urine fractions. No glucose-[ 15 N, 15 N]-ureide was found in the 0-24h and 24-48h urine collections in 1 of the volunteers after short-term administration of lactulose and was probably due to the fact that these urine fractions were significantly diluted. In none of the urine samples lactose-[ 15 N, 15 N]-ureide was detected. Neither glucose-[ 15 N, 15 N]-ureide nor lactose-[ 15 N, 15 N]-ureide was found in the analysis of the faecal samples.

DISCUSSION

The aim of the present study was to develop an analytical procedure using GC-MS analysis to quantify in a prospective study the urinary excretion of glucose-[ 15 N, 15 N]-ureide after oral administration of lactose-[ 15 N, 15 N]-ureide. The appearance of glucose-[ 15 N, 15 N]-ureide in urine is the result of hydrolysis, absorption and urinary filtration of the disaccharide bond in lactose-[ 15 N, 15 N]ureide by the brush border enzyme β-galactosidase to release galactose and glucose-[ 15 N, 15 N]ureide.

Quantitative evaluation of the urinary glucose-[ 15 N, 15 N]-ureide excretion in the prospective study has indicated that the urinary excretion of 15 N-labelled substrate reaches its maximum excretion level in the 3-6h urine collection, which is assumed to represent the in vivo absorption from the small intestine. We determined previously the orocaecal transit time, i.e. the time to reach the colon, of the standard test meal used in the present study and found it to approximate 360 min (Verbeke et al., 2005). Thus, the time for appearance of the label in urine within the first 6 hours, after administration is due to hydrolysis of lactose-[ 15 N, 15 N]-ureide to glucose-[ 15 N, 15 N]-ureide and galactose by the enzyme β-galactosidase which is located in the brush border of the small intestine, subsequent absorption and distribution in the body, followed by renal excretion. However, also in the 6-9h and 9-24h urine collection, a small amount of 15 N-labelled glucose ureide was recovered, suggesting that a certain percentage of glucose-[ 15 N, 15 N]-ureide might remain in circulation in the body before being excreted. As a consequence, the urinary 15 N content recovered in those urine collections does not all originates from the 15 N-labelled urea formed after bacterial degradation of the test substrate, but a minor fraction of the 15 N can be attributed to 15 N-labelled glucose ureide excretion.

Since lactose-[ 15 N, 15 N]-ureide has been proposed as a biomarker to evaluate the influence of preand/or probiotics on the colonic fate of urea-nitrogen, it was investigated whether the metabolism of lactose-[ 15 N, 15 N]-ureide was influenced by administration of the pre-and/or probiotics. For this purpose, urine and faecal samples which were already available from a dietary intervention study with lactulose have been re-analysed in the second part of the study [START_REF] De Preter | Effect of lactulose and Saccharomyces boulardii administration on the colonic urea-nitrogen metabolism and the bifidobacteria concentration in healthy human subjects[END_REF].

It is unlikely that probiotics would influence the lactose-[ 15 N, 15 N]-ureide metabolism, but it is well known that certain non-digestible carbohydrates may influence transit and digestion in the gastrointestinal tract. Lactulose has previously been shown to significantly delay gastric emptying by increasing viscosity of the gut contents and to accelerate small intestinal transit [START_REF] Diggory | The effect of dose and osmolality of lactulose on the oralcaecal transit time determined by the hydrogen breath test and the reproducibility of the test in normal subjects[END_REF][START_REF] Holgate | Relationship Between Small Bowel Transit-Time and Absorption of A Solid Meal -Influence of Metoclopramide, Magnesium-Sulfate, and Lactulose[END_REF][START_REF] Wutzke | Evaluation of oro-coecal transit time: a comparison of the lactose-[13C, 15N]ureide 1[END_REF]. As a consequence, the absorption of glucose-[ 15 N, 15 N]ureide could be decreased due to either the shorter time available for absorption or to a decreased hydrolysis of lactose-[ 15 N, 15 N]-ureide to glucose-[ 15 N, 15 N]-ureide. However, in the present study the mean glucose-[ 15 N, 15 N]-ureide absorption and urinary excretion was not influenced by the presence of lactulose in the test meal, although the individual results of the urinary glucose-[ 15 N, 15 N]-ureide excretion are more variable compared to baseline and long-term lactulose administration. In five individuals, inclusion of lactulose in the test meal resulted in less glucose-[ 15 N, 15 N]-ureide excretion suggesting that the absorption of glucose-[ 15 N, 15 N]-ureide was decreased due to the shorter time available for absorption or to a decreased hydrolysis of lactose-[ 15 N, 15 N]-ureide to glucose-[ 15 N, 15 N]ureide, whereas in four individuals more glucose-[ 15 N, 15 N]-ureide was recovered.

Long-term dietary intake of lactulose on the other hand, is known to cause changes in the metabolic activity and the relative composition of the colonic microbiota. Acidification of colonic luminal environment has probably no effect on the absorption of glucose-[ 15 N, 15 N]-ureide in the small intestine, but could hypothetically influence the bacterial hydrolytic processes in the colon, resulting in an incomplete hydrolysis of 15 N-labelled glucose ureide. As a consequence, unhydrolysed glucose-[ 15 N, 15 N]-ureide might be detected in the faecal samples. However, analysis of faecal samples has indicated that nor glucose-[ 15 N, 15 N]-ureide neither lactose-[ 15 N, 15 N]-ureide appeared in the faeces.

The results of both studies have indicated that meanly 13.16 ± 2.19 % of glucose-[ 15 N, 15 N]-ureide is recovered in urine after administration of 15 N-labelled lactose ureide and remains quite constant within the different individuals and even between the different test circumstances. This percentage dose recovered in urine was in line with the estimated 13 C-recovery after oral administration of lactose-[ 13 C]-ureide, as determined by Morrison et al. [START_REF] Morrison | Gastrointestinal handling of glycosyl [13C]ureides[END_REF].

In Table 2, the original (total) 15 N data and corrected 15 N data are shown. For each volunteer, the original 15 N data was corrected with the actual individual percentage glucose-[ 15 N, 15 N]-ureide recovered. As was expected, the correction for the presence of glucose-[ 15 N, 15 N]-ureide did not have a significant influence on the previously observed effects. Since it would be very time-consuming and labour intensive to measure in each urine sample the amount of glucose-[ 15 N, 15 N]-ureide besides the 15 N-enrichment and because of the small variability in amounts of retrieved glucose-[ 15 N, 15 N]-ureide, we suggest not to correct the data for total 15 N excretion for the presence of glucose-[ 15 N, 15 N]ureide.

In conclusion, the results obtained in the present study have indicated that the percentage dose glucose-[ 15 N, 15 N]-ureide recovered in urine is rather constant and not influenced by the presence of lactulose.

  Nexcretion (De Preter et al., 2004; Geboes et al., 2005).

Figure 1 :Figure 2 :Figure 3 :Figure 4 :

 1234 Figure 1: Schematic representation of the metabolism of lactose-[ 15 N, 15 N]-ureide

Table 2 :

 2 Correction of the urinary15 N-data (% dose/48h) for the presence of glucose-[ 15 N,15 N]-ureide before and after short-term (ST) and long-term (LT) lactulose intervention

			Baseline	ST Lactulose	p-value	LT Lactulose	p-value
	Cum 15 N rec (%dose/48h)	correction Before correction After	(IQR 25.25-44.29) 52.62 (IQR 39.48-56.06) 37.95	(IQR 5.39-21.42) 29.27 (IQR 20.96-34.60) 18.40	p=0.002 p<0.001	(IQR 19.77-34.60) 43.18 (IQR 32.83-49.23) 29.26	p=0.013 p=0.013

Acknowledgements

VDP is a postdoctoral fellow of the Fund for Scientific Research -Flanders (F.W.O. Vlaanderen, Belgium).

None of the authors had any financial or personal conflict of interest.

* In 1 volunteer, GUR was still present in the 24-48h urine fraction.