Davide Sangiorgi

Asynchronous π-calculus at work: the call-by-need strategy

 Palamidessi has shown that the expressive power of the Asynchronous π-calculus is strictly less than that of the full (synchronous) π-calculus. This gap in expressiveness has a correspondence, however, in sharper semantic properties for the former calculus, notably concerning algebraic laws. This paper substantiates this, taking, as a case study, the encoding of call-by-need λ-calculus into the π-calculus. We actually adopt the Local Asynchronous π-calculus, that has even sharper semantic properties. We exploit such properties to prove some instances of validity of β-reduction (meaning that the source and target terms of a β-reduction are mapped onto behaviourally equivalent processes). Nearly all results would fail in the ordinary synchronous π-calculus. We show that however the full β-reduction is not valid. We also consider a refined encoding in which some further instances of β-validity hold. We conclude with a few questions for future work.

Introduction

A lot of effort has been devoted to the comparison of the π-calculus with the λ-calculus, beginning with Milner's seminar work on functions as processes [START_REF] Milner | Functions as processes[END_REF]. The attention has gone mostly to call-by-name and call-by-value λ-calculi [START_REF] Plotkin | Call by name, call by value and the λ-calculus[END_REF], and the main results concern operational correspondence, validity of β-reduction, characterisation of the equivalence induced on λ-terms by the π-calculus encoding [START_REF] Milner | Functions as processes[END_REF][START_REF] Sangiorgi | An investigation into functions as processes[END_REF][START_REF] Sangiorgi | From λ to π, or: Rediscovering continuations[END_REF][START_REF] Vasconcelos | Lambda and pi calculi, CAM and SECD machines[END_REF][START_REF] Durier | Eager functions as processes[END_REF]. In particular, the call-by-name encoding, for its simplicity, is often presented as the π-calculus representation of functions.

In a call-by-name reduction, the redex contracted is the leftmost one; the reduction occurs regardless of whether the argument of the function is a value (as in call-by-value). As a consequence, if the argument is not a value and will be used several times, its evaluation will be repeated the same number of times. In implementation of programming languages following call-by-name, this repetition of evaluation is avoided: evaluation occurs only once, the first time the term is used, and the value so obtained is recorded for future uses. This implementation technique is referred to as call-by-need evaluation (or strategy) [START_REF] Wadsworth | Semantics and pragmatics of the lambda calculus[END_REF]. Thus call-by-need uses explicit environments and β-reduction does not require substituting a term for a variable, as in call-by-name (or call-by-value) -just substituting a reference to a term for a variable. In this sense call-by-need is closer to the π-calculus than call-by-name, as substitutions in the π-calculus only involve names. Again, the modifications that take us from call-by-name to call-by-need can be easily represented in a π-calculus encoding [START_REF] Sangiorgi | The π-calculus: a Theory of Mobile Processes[END_REF].

The π-calculus, having a rich and well-developed theory, as well as a remarkable expressiveness, has been advocated as a foundational model for reasoning about higher-order languages, including equivalence between programs and correctness of compilers and compiler optimisations [START_REF] Sangiorgi | Typed pi-calculus at work: A correctness proof of Jones's parallelisation transformation on concurrent objects[END_REF][START_REF] Turner | The polymorphic pi-calculus: Theory and Implementation[END_REF]. Indeed, the π-calculus and related languages have been used, via appropriate encodings, as a target language of compilers, for a number of experimental programming languages, beginning with Pict [START_REF] Pierce | Pict: A programming language based on the pi-calculus[END_REF] and Join [START_REF] Fournet | The join calculus: A language for distributed mobile programming[END_REF].

The above raises the question about how, and at which extent, the π-calculus and its current theory can be used to prove the correctness of call-by-need as an optimised implementation strategy for call-by-name. The only work on the correctness of the π-calculus representation of call-by-need is by Brock and Ostheimer [START_REF] Brock | Process semantics of graph reduction[END_REF]. The paper considers operational correspondence, between reduction in a call-by-need system and in the encoding π-calculus terms. However there are foundametal semantic issues that remain unexplored. A major one is the validity of β-reduction, namely the property that the processes encoding β-convertible λterms are behaviourally iundistinguishable. The property holds in call-by-name (and it is at the heart of its theory), as well as in the π-calculus encoding of callby-name. One would therefore hope to find analoguos results for call-by-need. The correctness of the process representation of call-by-need is the topic of the present paper, focusing on the validity of β-reduction.

In a well-known and influential paper [START_REF] Palamidessi | Comparing the expressive power of the synchronous and asynchronous pi-calculi[END_REF] Palamidessi has shown that the expressive power of the asynchronous π-calculus is strictly less than that of the full (synchronous) π-calculus. This gap in expressiveness has a correspondence, however, in sharper semantic properties for the former calculus, notably concerning algebraic laws. This paper may be seen as a demonstration of this, since most the proofs are carried out using algebraic laws that are only valid in the asynchronous π-calculus -precisely in the Asynchronous Local π-calculus, ALπ, [START_REF] Merro | On asynchrony in name-passing calculi[END_REF], where only the output capability of names may be exported.

In Section 2 we present ALπ and some of its laws. In Section 3 we briefly recall the call-by-name and call-by-need λ-calculus. In Section 4 we consider two encodings of call-by-need. We show that limited forms of validity β-reduction hold, and that the general property fails. The questions that follow from this, discussed in Section 5, may contribute to open some interesting directions for future work, which may also shed further light on the theory of the π-calculus and similar name-passing calculi.

The Asynchronous Local π-calculus

Syntax

Small letters a, b, . . . , x, y, . . . range over the infinite set of names, and P, Q, R, . . . over the set of all processes. A tilde represents a tuple. The i-th elements of a tuple E is referred to as E i . Our notations are extended to tuples componentwise.

The Asynchronous Local π-calculus (ALπ) [START_REF] Merro | On asynchrony in name-passing calculi[END_REF] is built from the operators of inaction, input prefix, output, parallel composition, restriction, and replication:

P := 0 | a( b). P | a b | P 1 | P 2 | νa P | !a( b). P .
with the syntactic constraint that in processes a( b). P and !a( b). P names b may not occur free in P in input position.

When the tilde is empty, the surrounding brackets () and will be omitted. 0 is the inactive process. An input-prefixed process a( b). P , where b has pairwise distinct components, waits for a tuple of names c to be sent along a and then behaves like P { c / b}, where { c / b} is the simultaneous substitution of names b with names c. An output particle a b emits names b at a. Parallel composition is to run two processes in parallel. The restriction νa P makes name a local, or private, to P . A replication !P stands for a countable infinite number of copies of P in parallel. We assign parallel composition the lowest precedence among the operators.

Terminologies and notations

We write a(b). b( c). Q as an abbreviation for νb (ab | b( c). Q), and similarly for a(b). !b( c). Q. The prefix 'a(b)' is called a bound output. In prefixes a( b) and a b , we call a the subject and b the object. We use α to range over prefixes. We often abbreviate α. 0 as α, and νa νb P as (νa, b) P . An input prefix a( b). P and a restriction νb P are binders for names b and b, respectively, and give rise in the expected way to the definition of free names (fn), bound names (bn) and names (n) of a term or a prefix, and alpha conversion. We identify processes or actions that only differ on the choice of the bound names. The symbol = will mean "syntactic identity modulo alpha conversion". Sometimes, we use def = as abbreviation mechanism, to assign a name to an expression to which we want to refer later. In a statement, a name declared fresh is supposed to be different from any other name appearing in the objects of the statement, like processes or substitutions. Substitutions are of the form { b / c}, and are finite assignments of names to names. A context is a process expression with a hole [•] in it. We use C to range over contexts; then C[P ] is the process obtained from C by filling its hole with P .

Sorting

Following Milner [START_REF] Milner | The polyadic π-calculus: a tutorial[END_REF], we only admit well-sorted agents, that is agents obeying a predefined sorting discipline in their manipulation of names. The sorting prevents arity mismatching in communications, like in a b, c | a(x). Q. A sorting is an assignment of sorts to names, which specifies the arity of each name and, recursively, of the names carried by that name. We do not present the formal system of sorting because it is not essential in the exposition of the topics in the present paper.

We will however allow sorting to identify linear names, that is, names that are supposed to be used only once. Linearity will be used a few times to replace input-replicated prefixes with ordinary input prefixes. Again, we omit the details of linearity in type systems (sorting is a form of type system), as they are by now standard [START_REF] Kobayashi | Linearity and the pi-calculus[END_REF][START_REF] Sangiorgi | The π-calculus: a Theory of Mobile Processes[END_REF]. ------→ P . In both cases, the action occurs at a -the subject of the action. In the output action, b is the tuple of names which are emitted, and d ⊆ b are private names which are carried out from their current scope. We use µ to represent the label of a generic action (not to be confused with α, which represents prefixes). In an input action a( d) and in an output action (ν d) a b , names d are bound, the remaining ones free. Bound and free names of an action µ, respectively written bn(µ) and fn(µ), are defined accordingly. The names of µ, briefly n(µ), are bn(µ) ∪ fn(µ). The transition system of the calculus is presented in Figure 1. We have omitted the symmetric versions of rules par and com. Alpha convertible processes have deemed to have the same transitions. We often abbreviate P τ -→ Q with P -→ Q. The 'weak' arrow =⇒ is the reflexive and transitive closure of -→.

inp: a( b). P a( b) ---→ P out: a b a b ---→ 0 rep: P | !P µ -→ P !P µ -→ P par: P µ -→ P P | Q µ -→ P | Q if bn(µ) ∩ fn(Q) = ∅ com: P a( c) ---→ P Q (ν d) a b ------→ Q P | Q τ -→ ν d (P { b / c} | Q ) if d ∩ fn(P ) = ∅ res: P µ -→ P νa P µ -→ νa P a ∈ n(µ) open: P (ν d) a b ------→ P νc P (ν c, d) a b -------→ P c ∈ b -d, a = c.
We use the symbol ≡ to denote structural congruence, a relation used to rearrange the structure of processes [START_REF] Milner | The polyadic π-calculus: a tutorial[END_REF]. We shall also use it to represent garbagecollection of restrictions and of inert terms.

Definition 1 (Structural congruence). Structural congruence, ≡, is the smallest congruence relation satisfying the axioms below:

-P | 0 ≡ P , P | Q ≡ Q | P , P | (Q | R) ≡ (P | Q) | R -!a(x). P ≡ a(x). P | !a(x). P ; -νa 0 ≡ 0, νa νb P ≡ νb νa P , νa (P | Q) ≡ P | νa Q if a ∈ fn(P ); -νa (P | !a( b). Q) ≡ P and νa (P | a( b). Q) ≡ P , if a ∈ fn(P ).
(A derivable law is νa P ≡ P , for a not free in P .) A standard behavioural equivalence for the π-calculus is barbed congruence. Barbed congruence can be defined in any calculus possessing: (i) an interaction relation (the τ -steps in the π-calculus), modelling the evolution of the system; and (ii) an observability predicate ↓ a for each name a, which detects the possibility of a process of accepting a communication with the environment at a. More precisely, we write P ↓ a if P can make an output action whose subject is a, that is, if there are P and an output action µ with subject a such that P µ -→P . We write P ⇓ a if P =⇒ P and P ↓ a . Unlike synchronous π-calculus, in asynchronous calculi it is natural to restrict the observation to output actions [START_REF] Amadio | On bisimulations for the asynchronous π-calculus[END_REF]. The reason is that in asynchronous calculi the observer has no direct way of knowing when a message emitted is received.

Definition 2 (Barbed congruence). A symmetric relation S on π-calculus processes is a barbed bisimulation if P S Q implies:

1. If P τ -→P then there exists Q such that Q =⇒ Q and P S Q . 2. If P ↓ a then Q ⇓ a .
Two π-calculus processes P and Q are barbed bisimilar if P S Q for some barbed bisimulation S. We say that P and Q are barbed congruent, written P ≈ Q, if for each π-calculus context C, processes C[P ] and C[Q] are barbed bisimilar.

Strong barbed congruence, written ∼, is defined analogously but replacing the weak arrows =⇒ and ⇓ a with the strong arrows -→ and ↓ a . As expected, we have ≡ ⊆ ∼ ⊆ ≈; each containment is strict.

Further algebraic laws

Most of the proofs in the paper are carried out using algebraic reasoning. We report here some important laws. First some simple laws that are valid in the full (synchronous) π-calculus (Lemma 1). Then laws that are specific to ALπ.

Lemma 1. 1. νa (a(b). P | a(y). Q) ≈ (νa, b) (P | Q{ b /y}) and νa (a(b). P | !a(y). Q) ≈ (νa, b) (P | Q{ b /y} | !a(y). Q); 2. νa (α. Q | !a( x). P ) ∼ α. νa (Q | !a( x). P ), if bn(α) ∩ fn(a( x). P ) = ∅ and
a ∈ n(α) (a similar law holds without the replication); 3. a( x). (P | !a( x). P ) ∼ !a( x). P .

Important laws of ALπ are the following ones. Their validity hinges on the asynchronous and output-capability properties of ALπ. For simplicity we present them on monadic prefixes.

Lemma 2. We have ab ≈ νc (ac | !c(x). bx). Moreover, if b is linear, then the replication can be removed thus: ab ≈ νc (ac | c(x). bx).

Next, we report some distributivity laws for private replications, i.e., for systems of the form νy (P | !y( q). Q) in which y may occur free in P and Q only in output position. One should think of Q as a private resource of P , for P is the only process who can access Q; indeed P can activate as many copies of Q as needed. One such law has already been given as Lemma 1 [START_REF] Ariola | A call-by-need λcalculus[END_REF]. (The laws can be generalised to the full π-calculus, but need stronger assumptions.) Lemma 3. Suppose a occurs free in P, R, Q only in output position. Then:

1. νa (P | R | !a( b). Q) ∼ νa (P | !a( b). Q) | νa (R | !a( b). Q); 2. νa ((!P ) | !a( b). Q) ∼ !νa (P | !a( b). Q); 3. νa (α. P | !a( b). Q) ∼ α. νa (P | !a( b). Q), if bn(α) ∩ fn(a( b). Q) = ∅ and a ∈ n(α); 4. νa ((νc P ) | !a( b). Q) ∼ νc νa (P | !a( b). Q) if c ∈ fn(a( b). Q).
ALπ has also sharper properties concerning labelled characterisation of bisimilarity and associated congruence properties [START_REF] Merro | On asynchrony in name-passing calculi[END_REF][START_REF] Boreale | Some congruence properties for π-calculus bisimilarities[END_REF].

The λ-calculus

We use M, N to range over the set Λ of λ-terms, and x, y, z to range over variables. The set Λ of λ-terms is given by the grammar:

M ::= x | λx. M | M N
A redex is a term of the form (λx. M )N , and then its contractum is M { N /x}. In call-by-name evaluation [START_REF] Plotkin | Call by name, call by value and the λ-calculus[END_REF], the redex is always at the extreme left of a term. We omit the standard evaluation rules.

Call-by-need [START_REF] Wadsworth | Semantics and pragmatics of the lambda calculus[END_REF][START_REF] Ariola | A call-by-need λcalculus[END_REF] optimises call-by-name as follows, so to guarantee that in the contractum M { N /x} the evaluation of N is not performed more than once. Roughly, N is placed in an environment, and the evaluation continues on M . When x is needed (i.e., x reaches the leftmost position), then N is evaluated and, if a value (i.e., an abstraction) is obtained, say V , then V replaces x (value V can replace all occurrences of x or, more commonly, only the leftmost occurrence, and then other occurrences of x when they reach the outermost position). Callby-need is best presented in a graph; or in a system with a let construct to represent sharing. We refer to Ariola et al. [START_REF] Ariola | A call-by-need λcalculus[END_REF] for details, as they are not essential for understanding the remainder of the paper; see also the references in Section 5.

We sometimes omit λ in nested abstractions, thus for example, λx 1 x 2 . M stands for λx 1 . λx 2 . M . We assume the standard concepts of free and bound variables and substitutions, and identify α-convertible terms. Thus, throughout the paper '=' is syntactic equality modulo α-conversion.

Following the call-by-value terminology, the set of abstractions and variables are the values. (Indeed, call-by-need may also be thought of as a modified form of call-by-value, in which the evaluation of the argument of a function λx. M is made only when x is used for the first time, rather than before performing the reduction.) [START_REF] Boudol | Some chemical abstract machines[END_REF] The encoding and its properties

Background material

Figure 2 presents the call-by-name and call-by-need encodings [START_REF] Ostheimer | π-calculus characterisations of some practical λ-calculus reductions strategies[END_REF][START_REF] Sangiorgi | The π-calculus: a Theory of Mobile Processes[END_REF]. The callby-name one is a variant of the original encoding by Milner [START_REF] Milner | Functions as processes[END_REF], with the advantage that it can be written in ALπ and can be easily modified to follow call-by-need.

We explain the encodings. The important part is the treatment of application. Both in call-by-name and in call-by-need, a function located at q (its 'location') is a process that signals to be a function on q, and then receives a pointer x to the argument N together with the location p for the next interaction. Now the evaluation of M continues. The difference between call-by-name and call-by-need arises when the argument N is needed. This is signaled by an output at x that also provides the location for the evaluation of a copy of N . In call-by-name, every output at x triggers the evaluation of a new copy of N . In call-by-need, in contrast, the evaluation is made only the first time. Precisely, in call-by-need N is evaluated at the first request and, when it becomes a value, a pointer to this value is returned (instantiating w, in the table). This pointer is returned to the process that requested N . When further requests for N are made, the pointer is returned immediately. Thus, for instance, in the call-by-name encoding of (λ. xx)(II) term II is evaluated twice, whereas in the call-by-need encoding only once. In all encodings, the location names (in the table, the names ranged over by p, q, r) are linear.

Correcteness of call-by-name has been studied in depth. In particular, it has been shown that β-reduction is validated by the encoding, that the encoding gives rise to a term model for the λ-calculus, and that the equivalence on λ-terms induced by the encoding corresponds to the best tree-structures of the λ-calculus -which are also at the heart of its denotational semantics -namely Böhm Trees and Lévy-Longo Trees [START_REF] Milner | Functions as processes[END_REF]23] Correctness of the call-by-need encoding has been studied only by Brock and Ostheimer [START_REF] Brock | Process semantics of graph reduction[END_REF], and only for operational correspondence with respect to Ariola et al.'s system [START_REF] Ariola | A call-by-need λcalculus[END_REF]. (The encoding in Figure 2 is actually a minor improvement over that in [START_REF] Brock | Process semantics of graph reduction[END_REF] -avoiding one reduction step during a β-reducition -and maintains the results of operational correspondence in [START_REF] Brock | Process semantics of graph reduction[END_REF] recalled below.) Following Ariola et al.'s system [START_REF] Ariola | A call-by-need λcalculus[END_REF] we write M ⇓ if the call-by-need computation of M terminates, and M ⇑ it the computation does not terminate.

call-by-name encoding

M[[λx. M ]]p def = p(v). !v(x, q). M[[M ]]q M[[x]]p def = xp M[[M N ]]p def = (νq ) M[[M ]]q | q(v). νx v x, p . !x(r). M[[N ]]r call-by-need encoding N [[λx. M ]]p def = p(v). !v(x, q). N [[M ]]q N [[x]]p def = xp N [[M N ]]p def = (νq ) N [[M ]]q | q(v). νx v x, p . x(r). νq ( N [[N ]]q | q (w). (rw | !x(r ). r w))

Fig. 2. The encoding of call-by-name and call-by-need

Theorem 1 (Brock and Ostheimer, [START_REF] Brock | Process semantics of graph reduction[END_REF]). We have, for M closed:

1. M ⇓ iff N [[M ]]p ⇓ p ; 2. M ⇑ iff N [[M ]]p ⇑.
The proof in [START_REF] Brock | Process semantics of graph reduction[END_REF] considers an extended version of the call-by-need system in [START_REF] Ariola | A call-by-need λcalculus[END_REF], one that yields a closer (nearly one-to-one) correspondence between reductions in the call-by-need system and reductions on the encoding π-calculus processes.

Note that, since M is closed, the only free name of N [[M ]]p is p; and since p is used in N [[M ]]p in output, the first visible action of N [[M ]]p (if there is one) is an output at p. However, operational correspondence alone is not fully satisfactory as a criterium for correctness. It does not ensure foundamental semantic properties of the source language terms. In the following sections we focus on the validity of β-reduction.

β-validity

We consider in this section a few cases of validity of β-reduction; that is, the property that a β-redex (λx. M )N and its contractum M { N /x} are barbed congruent when represented as ALπ processes.

A form of β-reduction that is straightforward to handle is one in which the argument is never used.

Theorem 2. If x ∈ fv(M ) then N [[(λx. M )N ]]p ≈ N [[M { N /x}]]p.
A more interesting form deals with β-reduction between closed values.

Theorem 3. N [[(λx. M )(λy. N )]]p ≈ N [[M { λy. N /x}]]p.
Proof. Using algebraic reasoning, we first derive:

N [[(λx. M )(λy. N )]]p = (νq ) N [[λx. M ]]q | q(v). νx v x, p . x(r). νq ( N [[λy. N ]]q | q (w). (rw | !x(r ). r w)) = (νq ) q(v). !v(x, q ). N [[M ]]q | q(v). νx v x, p . x(r). νq ( N [[λy. N ]]q | q (w). (rw | !x(r ). r w)) ≈ (νx ) N [[M ]]p | x(r). νq ( N [[λy. N ]]q | q (w). (rw | !x(r ). r w)) = (νx ) N [[M ]]p | x(r). νq ( q (v). !v(y, q ). N [[N ]]q | q (w). (rw | !x(r ). r w)) ≈ (νx ) N [[M ]]p | x(r). νv ( !v(y, q ). N [[N ]]q | (rv | !x(r ). r v)) ∼ (νx, v ) N [[M ]]p | !v(y, q ). N [[N ]]q | x(r). (rv | !x(r ). r v) ∼ (νx, v ) N [[M ]]p | !v(y, q ). N [[N ]]q | !x(r ). r v
where the two occurrences of ≈ represent applications of law (1) of Lemma 1, and the two occurrences of ∼ are due to laws (2) and (3) of the same lemma, respectively. Now we proceed by induction on the structure of M . If M is variable different from x then the two replications at v and x can be garbage-collected and we are done.

If M = x, then (νx, v )(N [[M ]]p | !v(y, q ). N [[N ]]q | !x(r ). r v) = (νx, v )(xp | !v(y, q ). N [[N ]]q | !x(r ). r v) ≈ (νx, v )(pv | !v(y, q ). N [[N ]]q | !x(r ). r v) ≡ (νv )(pv | !v(y, q ). N [[N ]]q ) = N [[λy. N ]]p
where ≈ is obtained from law (1) of Lemma 1, and ≡ from the garbage-collection laws of Definition 1.

When M is an abstraction or an application, we proceed by induction and exploit the distributivity properties of private replications in Lemma 3

Finally we consider the case when the argument of the function is divergenta form of β-reduction that is not valid in call-by-value.

Theorem 4. Suppose (λx. M )N is closed. If N ⇑ then we have N [[(λx. M )N ]]p ≈ N [[M { N /x}]]p.
Proof. Using Theorem 1 we have N [[N ]]q ⇑, for any q, hence N [[N ]]q ≈ 0. As a consequence, using algebraic reasoning similar to that in the proof of Theorem 3, we obtain

N [[(λx. M )N ]]p ≈ νx (N [[M ]]p | x(r). 0) Now, since x occurs in N [[M ]]p

Failure of general β-validity

However, in call-by-name and call-by-need β-reduction is not confined to values. We show that, in the call-by-need encoding, the general β-reduction fails. Notably β-reduction fails when the argument of the function is a variable. For this we show that

N [[yy]]p ≈ N [[(λz. zz)y]]p (1)
While for simplicity this counterexample is shown for open terms, a similar one can be given for closed terms, by closing the two terms with an abstraction, i.e.,

N [[λy. (yy)]]p ≈ N [[λy. ((λz. zz)y)]]p

The remainder of the section is devoted to the proof of (1). We first unroll the initial traces of the two processes (the only traces that they can perform) We have:

N [[yy]]p = (νq ) yq | q (w). νx w x , p . x (r). νq ( yq | q (w ). (rw | !x(r ). r w )) y(q ) ---→ q (w) ----→ νx w x ,p -------→ x (r) ---→ νq ( yq | q (w ). (rw | !x (r ). r w )) y(q ) ----→ q (w ) ----→ rw | !x (r ). r w
Since the above is the only possible trace of the term, we have

N [[yy]

]p ∼ y(q). q(v). νx v x, p . x(r). y(q ). q (w). (rw | !x(r ). r w)

We now consider the analogous trace for N [[(λz. zz)y]]p. Below, the uses of ≡ are due to some garbage-collection of restrictions and private inputs (possibly replicated), and some rearrangements of the scopes of some restrictions; the use of ∼ is due to [START_REF] Ariola | A call-by-need λcalculus[END_REF].

N [[(λz. zz)y]]p = (νq ) N [[λz. zz]]q | q(v). νx v x, p . x(r). νq ( N [[y]]q | q (w). (rw | !x(r ). r w)) = (νq ) q(v). !v(z, q ). N [[zz]]q | q(v). νx v x, p . x(r). νq ( yq | q (w). (rw | !x(r ). r w)) τ -→ τ -→≡ νx N [[xx]]p | x(r). νq ( yq | q (w). (rw | !x(r ). r w))
∼ νx

x(q). q(v). νx v x , p . x (r). x(q ). q (w). (rw

| !x (r ). r w) | x(r). νq ( yq | q (w). (rw !x(r ). r w)) τ -→≡ (νx, q, q ) q(v). νx v x , p . x (r). x(q ). q (w). (rw | !x (r ). r w) | yq | q (w). (qw | !x(r ). r w) y(q ) ---→ q (w)
----→ (νx, q) q(v). νx v x , p . x (r). x(q ). q (w). (rw | !x (r ). r w) | (qw | !x(r ). r w) τ -→ (νx) νx w x , p . x (r). x(q ). q (w). (rw | !x (r ). r w) | !x(r ). r w νx w x ,p -------→

x (r)

---→ (νx) x(q ). q (w). (rw

| !x (r ). r w) | !x(r ). r w τ -→ τ -→≡ rw | !x (r ). r w
Again, the above is the only possible trace for the term. Up-to some renaming, the final derivative is the same as the final derivative of the trace emanating from N [[yy]]p examined earlier. However, the two traces are different -the first is longer. As a consequence, the two terms can be distinguished, for instance in the context

C def = νy ([•] | y(q). q(v). v(x, p). νr (xr | y(q ). h))
The observable output at h becomes visible only when the context is filled with the first term, N [[yy]]p (the one that produces the longer trace).

In contrast, in the call-by-name encoding the validity of the full β-reduction holds [23]. Therefore the above counterexample not only shows that the call-byneed encoding is observably different from the call-by-name one; it also tells us that the properties that the two encoding satisfy are quite different.

A refined encoding

In this section we experiment with a refinement R of the encoding so to on the problems described in Section 4.3.

Such encoding is shown in Figure 3. In the definition of application for callby-need, the argument of a function is interrogated only once, the first time the argument is used. Future uses of the argument will directly use the answer so received, without repeating the interrogation -this is indeed the essence of the call-by-need optimisation over call-by-name. To mirror this policy we modify the encoding of an abstraction λx. M , so that the body M will interrogate the parameter x only once. As a consequence, in this refined encoding when the head 'λx' of the function is consumed a local entry is left that takes care of the dialogue with x; in particular the local entry makes sure that x is consulted only once. The refined encoding, while it exhibits more interactions than the original one, in a distributed setting may be thought of as an optimisation of the latter, as the interactions with the new local entry replace interactions with the possibly remote actual parameter for x. We write LE(x, y) for a local entry in which the internal resource is x and the external one is y; it will be convenient to break its definition into two parts, using the auxiliary local entry LE (s, r, x); see Figure 3.

The local entry is unnecessary if the internal resource is used only once.

R

[[λx. M ]]p def = p(v). !v(x , q). νx ( R[[M ]]q | LE(x, x )) R[[x]]p def = xp R[[M N ]]p def = (νq ) R[[M ]]q | q(v). νx v x, p . x(r). νq ( R[[N ]]q | LE (q , r, x))
where

LE(x, y) def = x(r). y(s). LE (s, r, x) LE (s, r, x) def = s(v). (rv | !x(r ). r v)
νz (R[[M ]]p | LE(z , z)) ≈ R[[M { z /z }]]p
Proof. By induction on the structure of M . The most interesting case is when M = z , in which case we exploit the (linear) law of ALπ in Lemma 2. When M is an application we exploit the hypothesis (z occurring only once), and simple algebraic manipulation, so to be able to carry out the induction.

The next lemma shows that local entries compose. Proof. We use laws ( 2) and (1) of Lemma 1, and the garbage-collection laws of structural congruence.

We revisite the counterexample of Section 4.3, that involves terms yy and (λz. zz)y, under the refined encoding R. All free variables should be protected under a local entry, except for the variables that occur only once (by Lemma 4). We begin by examining νy ( R[[y y ]]q | LE(y , y)). We have:

νy ( R[[y y ]]q | LE(y , y)) ∼
νy ( y (q). q(v). νx v x, p . x(r). y (q ). q (w). (rw | !x(r ). r w) | y (r). y(r ). r (v). (rv | !y (r). rv)) ≈ (νy , q) ( q(v). νx v x, p . x(r). y (q ). q (w). (rw

| !x(r ). r w) | y(r ). r (v). (qv | !y (q). qv)) y(r ) ---→ r (v)
---→ (νy , q) ( q(v). νx v x, p . x(r). y (q ). q (w). (rw | !x(r ). r w) | qv | !y (q). qv) τ -→ (νy ) ( νx v x, p . x(r). y (q ). q (w). (rw | !x(r ). r w) | !y (q). qv)

νx v x,p ------→ x(r)
---→ (νy ) ( y (q ). q (w). (rw | !x(r ). r w) | !y (q). qv)

τ -→ τ -→ rv | !x(r ). r v
where the occurrence of ∼ is justified by (2) (the two encodings coincide on terms that do not contain abstractions) and definition of LE(y , y), and the occurrence of ≈ comes from law (1) of Lemma 1.

We now consider the second term, (λz. zz)y, under the refined encoding. First we note that, if the argument of a function L is a variable, then the refined encoding can be simplified thus:

R[[Ly

]]p = (νq ) R[[L]]q | q(v). νx v x, p . x(r). νq ( N [[y]]q | LE (q , r, x)) = (νq ) R[[L]]q | q(v). νx v x, p . LE(x, y)

Conclusions

Call-by-need was proposed by Wadsworth [START_REF] Wadsworth | Semantics and pragmatics of the lambda calculus[END_REF] as an implementation technique. Formalizations of call-by-need on a λ-calculus with a let construct or with environments include Ariola et al. [START_REF] Ariola | A call-by-need λcalculus[END_REF], Launchbury [START_REF] Launchbury | A natural semantics for lazy evaluation[END_REF], Purushothaman and Seaman [START_REF] Purushothaman | An adequate operational semantics for sharing in lazy evaluation[END_REF], and Yoshida [START_REF] Yoshida | Optimal reduction in weak lambda-calculus with shared environments[END_REF]. The uniform encoding in Section 4 is from [START_REF] Ostheimer | π-calculus characterisations of some practical λ-calculus reductions strategies[END_REF].

A study of the correctness of the call-by-need encoding in Figure 2 is in [START_REF] Brock | Process semantics of graph reduction[END_REF]. Encodings of graph reductions, related to call-by-need, into π-calculus were given in [START_REF] Boudol | Some chemical abstract machines[END_REF][START_REF] Jeffrey | A chemical abstract machine for graph reduction[END_REF] but their correctness was not studied. Niehren [START_REF] Niehren | Functional computation as concurrent computation[END_REF] used encodings of callby-name, call-by-value and call-by-need λ-calculi into π-calculus to compare the time complexity of the strategies.

In the paper we have used the theory of the Asynchronous Local π-calculus (ALπ) [START_REF] Merro | On asynchrony in name-passing calculi[END_REF] to reason about the encoding of the call-by-need λ-calculus strategy as processes. We have mainly focused on the validity of β-reduction. We have showed that various instances of the property on closed terms hold, though the general property fails. We have also considered a refined encoding in which βreduction on arbitrary values (though not on arbitrary terms) holds. All this leaves us with some challenging questions, that we leave for future work:

1. In the refined encoding, we use special processes called local entries to protect the formal parameter of the function, thus improving the results about βvalidity. Is it possible to further protect variables (or terms) so to recover the full β-validity? 2. Is there a different form of behavioural equivalence under which the full β-validity holds, in the initial or in the refined encoding? 3. What is an appropriate process preorder under which call-by-need can indeed be proved to be an optimisation of call-by-name? 4. What is the equivalence on λ-terms induced by the call-by-need encoding?

Following the results for call-by-name and call-by-value, one expects to recover some kind of tree structure (Böhm Trees and Lévy-Longo Tree for call-by-name, Lassen's trees [START_REF] Lassen | Eager normal form bisimulation[END_REF] for call-by-value). We are not aware of similar tree structures for call-by-need. Hence investigating this question may also shed light on what should the appropriate forms of trees for call-by-need be.

In questions ( 2) and (3), 'easy' answers may be obtained by confining the testing contexts to be encodings of λ-calculus contexts. The challenge is to find more general and useful answers, with applications outside the realm of pure λ-calculi. One may consider forms of behavioural types.

In questions (1) and (2), perhaps requiring the validity of the full β-reduction, in the same way as for call-by-name, is too demanding. Indeed in this way probably the tree structure referred to in question ( 4) is likely to be the same as that for call-by-name. One may find it acceptable to limit β-validity to reductions between closed terms.

Fig. 1 .

 1 Fig. 1. The transition system for ALπ

  only in output subject position, each output at x, say xr, can be removed, or replaced by N [[N ]]r (because in the relation ≈ with 0), up-to ≈. This yields N [[M { N /x}]]p.

Fig. 3 .Lemma 4 .

 34 Fig. 3. The refined call-by-need encoding

Lemma 5 .

 5 νx (LE(z, x) | LE(x, y)) ≈ LE(z, y).

Acknowledgments Thanks to the reviewers for their careful reading of the paper and their suggestions. Research partly supported by the H2020-MSCA-RISE project ID 778233 "Behavioural Application Program Interfaces (BEHAPI)".

Using this property, we have: R[[(λz. zz)y]]p = (νq ) R[[λz. zz]]q | q(v). νx v x, p . LE(x, y) = (νq )( q(v). !v(z , q). νz ( R[[zz]]q | LE(z, z ))

| q(v). νx v x, p . LE(x, y))

where ≈ is obtained by composition of local entries (Lemma 5).

The above reasoning shows that the behaviour of the initial and refined encodings are the same on the term (λz. zz)y:

And it is also the same as that of the refined encoding on the β-contractum yy, when the free variables y are protected under the appropriate local entry, i.e.,

R[[(λzz)y]]p ≈ νy (R[[y y ]]p | LE(y , y))

The result also holds by closing up the terms:

R[[λy. (yy)]]p ≈ R[[λy. ((λz. zz)y)]]p

In the refined encoding R, the local entry (necessary for confining the behaviour of yy) is produced by the encoding of the abstraction.

More generally, proceeding as above one can show that, on the encoding R, β-reduction is valid when the argument of a function is a variable. Moreover, β-reduction is also valid when the argument is itself a function, reasoning as in Theorem 3. We may therefore conclude that β-reduction is valid when the argument is a value (as it is the case for the encoding of the call-by-value strategy [START_REF] Sangiorgi | The π-calculus: a Theory of Mobile Processes[END_REF]).

We write LE( x, y) for LE(x 1 , y 1 ) | . . . | LE(x n , y n ) where n is the length of the tuples x and y. We use V to range over values. Theorem 5. Suppose fv((λz. M V )) ⊆ x. Then, for any y and fresh y, we have

Similarly to what done earlier, a local entry LE(x i , y i ) may be removed when the variable x i appears at most once.

However, even in the encoding R, the full β-reduction is unvalid. As a counterexample we can use the terms (xz)(xz) and (λy. yy)(xz). Indeed we have:

We omit the calculations, which are rather involved. Intuitively, the difference appears because the full trace of the process computing the application xz is visible twice in the first process, whereas, in the second process, the second time, part of the trace is concealed.


Vatsal Pant
email: vatsal.pant@isae.fr

Hamid Demmou

Using Systems Engineering to Model the Interaction of the Pilot, the Aircraft, and the Procedures

Keywords: MBSE, MBSA, SysML, Modeling, Procedures, Safety Analysis, Cockpit

This paper presents an ongoing work on how systems engineering relates pilot, procedures, and the aircraft. This is done by modelling these three using an example case of landing procedure (general aviation). The model also helps in performing safety analysis of the procedures laid out by the aircraft operators/ manufacturers, or the aviation regulating authorities (EASA, FAA, etc.).

I. INTRODUCTION

In aviation the three most important entities are, the human (be it the engineer who designs it or the pilot who flies it), the machine (the aircraft, more specifically the cockpit, where the pilot interacts with the aircraft), and perhaps the most important of all procedures. Procedures have played the role of making sure that everything is indeed done as it is meant to be. It is like the holy book of aviation; everyone believes in it and follows it with utmost faith. Almost always the outcome is perfect and smooth operation of the entire system (aircraft and personnel), for example, a pilot is trained to follow a procedure to land an aircraft at an airport. The pilot has a certain number of tasks to perform, that he/she verifies by going through a checklist. However, there have been cases when pilots had to actually deviate from the procedures to avoid a catastrophe (the best example can be the case of US Airways flight 1549 where captain Chesley Sullenberger skipped directly to the 18th step in order to safely ditch the A320 on the Hudson. [START_REF]Loss of Thrust in Both Engines After Encountering a Flock of Birds and Subsequent Ditching on the Hudson River US Airways Flight 1549 Airbus A320214, N106[END_REF] There have also been cases where the procedures were simply missing or not at place (for example, the recent crashes of Lion Air Flight 610 [START_REF]Lion Mentari Airlines Boeing 737-8 (MAX); PK-LQP Tanjung Karawang[END_REF] and Ethiopian Airlines Flight 302 [START_REF]Aircraft Accident Investigation Preliminary Report Ethiopian Airlines Group B[END_REF]) and the pilot had to rely on their experience or in some case inexperience (both examples of the 737 missing procedures for a certain Maneuvering Characteristics Augmentation System that compensated for higher and forward position of the engine on the wing). Given these situations, it becomes very interesting to carry out the safety assessment of how the pilots carry out these procedures. The first step in that direction is to model the pilot and the cockpit together with the procedures.

The next section shows why we use Systems Engineering to model this interaction. Subsequently moving on to the section that models the three parts separately and the fourth section shows how this integration is carried out. Finally discussing the Conclusion with some future works.

II. MBSE

Model-based systems engineering (MBSE) relies on the leverage of the graphical representation and the abstraction of modelling in the design and development phases. Thus, models bear powerful means for the systems analysis and the early validation, e.g., through model simulations or theorem proof techniques.

Why Use UML?

UML, or Unified Modelling Language, was developed to better visualize and model programs (especially for Object Oriented Programming). It has an interesting perspective to visualize relationship between classes and entities of a computer program. It has the advantage that it doesn't require a programmer to read the complete code, instead he can go through the model diagram and understand what the program is about. It is very readable for any level of computer programmer. Inspired by this, we wanted to develop a model that can be used by people from different domains. Our objective was that different users/experts can work on a common block diagram and understand the working from everyone's point of view. As will be seen later in the coming sections that it becomes very easy to understand what goes in the cockpit and how the pilot carries out tasks just by looking at these diagrams.

Also, we wanted to have a tool based on this modelling that enables, for instance, the pilot to try different operational scenarios and see how they affect the working of the whole system. The basic objective of this model is to have a common, "ready for all" starting model that everyone can play with and provide their inputs.

Before starting the modelling here is a brief introduction to the class diagram and what each representation (arrows, boxes, etc stand for). figure 1 shows a generic class diagram.

Class diagram represents a class as a block that has the following partitions: -Name: the name of the class -Attributes: the properties of the class that describe the object being modelled. The next section shows how each of the components is modelled separately and the explanation of each class diagram.

III. MODELLING

In this section we show how we used the above mentioned UML class diagram representation to model the pilot, procedures, and the cockpit. The overall idea of this interaction can be seen in figure 2.

Pilot takes visual inputs and information from the display screens and perform some actions on the aircraft by applying input to the control columns like yoke, thrust, flaps, rudder, and landing gear. These actions are given by Procedures that contain all the tasks needed to perform the landing and allows the pilot to execute the required task in a sequential order. To perform a task, the pilot provides a control action (landing gear lever down), this control action gives an input to the aircraft (electrical input). The aircraft processes it and gives corresponding control output (like, lowering of the landing gear by hydraulic actuation). The sensors check if the landing gear is down and locked, if yes, it is indicated to the pilot in the cockpit by three green lights and the approach is continued. If anything is in an incorrect position, the pilot receives a warning and he/she selects a non nominal procedure from the Quick Reference Handbook and switches to a different set of tasks (for example, they may perform a missed approach procedure by going around, in this case the task would be to increase throttle, pitch up, inform Air Traffic Controller, etc).

A. Landing Procedure

The landing procedures are published by regulatory authorities, airlines, and aircraft manufacturer based on their requirement like type of runway, special operating scenarios, etc. We use the generic landing procedure published by FAA in pilot handbook [START_REF]FAA Manual, Airplane Flying Handbook (FAA-H-8083-3B), Chapter8: Approaches and Landings[END_REF] mentioned in the following steps. This can also be seen in 3 4 The attributes are:

• speed: it corresponds to the speed of the aircraft with respect to the wind, it is of type integer. • position: it uses navigational aids and computes the distance from touch down point on the runway (it is in nautical miles, of type integer) • altitude: during the approach phase pilots usually switch from altitude with respect to the mean sea level to radio altitude, i.e., the altitude with respect to the ground just below the aircraft. (it is in feet, so type integer is used) • heading: It is defined as the direction of the flight with respect to the true north. It is measured in degrees (from 1 to 360, integer) • delay:delay in performing a task might lead to an abnormal scenario hence it is also used as an attribute to define the class. (it is measured in seconds, hence type integer) After the attributes we define the operations of this class:

• select task(): it selects the next task based on the position of the aircraft, for example when the aircraft is aligned to the runway, it will select lower landing gear. • execute task(): Once the input is received from the pilot it will perform the desired task • compare(): this operation will compare the task performed by the pilot and the task that must have been performed. Also the delay that was present while performing the task. There are two sub-classes that depend on the parent class "Procedures" they are "Checklists" and "Tasks"

The attributes of checklists are:

• tasklist: It is of type boolean and basically takes status of 1 (meaning task done) and 0 (missing task). The operations are:

• selectnormal(): based on the state of the aircraft, if everything is normal this will be selected. • selectnonnormal(): If there is a fault or failure, this will be selected. Here we notice that the relationship has "1 to many" cardinality this shows that there exists various checklists that Fig. 5. Pilot UML are performed when coming to land, and at the appropriate phase corresponding checklist is selected.

The attributes of class "Tasks" are:

• speed: same as "procedures"

• position: same as "procedures"

• altitude: same as "procedures"

• heading: same as "procedures"

• delay: same as "procedures"

• type: this is of type string that selects the type of tasks to be performed based on the condition of the flight (nominal, non nominal) After the attributes we define the operations of this class:

• select task(): it selects the next task to be performed.

B. Pilot Modeling

The pilot has in his/her memory the list of task to be done for a procedure, he starts with the first task, gives an input to the aircraft (yoke, thrust, etc) and then sees the output, if the output is correct, he moves to the next task, and subsequently finishes the entire procedure successfully. However, if the output is not the expected one, he selects a new procedure to compensate for the incorrect state of the aircraft. For example, lets say the pilot is approaching the runway and gives the command to extend the flaps. The flaps have a faulty actuator and they dont extend. In that case the pilot uses a different procedure by increasing the speed of the aircraft to compensate for loss of high lift device (flaps) so that the aircraft doesn't stall. The pilot then subsequently plans for a high speed approach and informs his intentions to the Air Traffic Controller. The thing that ensures that the procedures have been carried out is the checklist, it was purely verbal in the past but now we have electronic checklist that is partially verified/filled in by the aircraft systems. To better model this behavior of pilot in the cockpit we use UML model shown in 5

The attributes of class "pilot" are:

• visual: it is of type string. It describes everything that the pilot is looking outside of the cockpit, for example, the runway, approach lights, etc.

• screen: also of type string that shows the information available on the display screens inside the cockpit. The operations performed by class "pilot" are:

• lower LG(): the pilot lowers the landing gear • yoke input(): provides input on the control stick • rudder input(): provides input on the rudder The attributes of class Control Actions are

• decision: it is of type Boolean that shows if the decision of performing a control action was taken or not. Following are the operations performed by this class:

• advance task(): based on the decision move to the next task • assign checklist(): assign "done" to the checklist.

C. Aircraft

Aircraft class is the only physical component of our model. It represents two sub classes: cockpit and Control surfaces as seen in figure 6. The idea behind this block is to show how the pilot interacts with the aircraft. The attributes are

• callsign: it is the identifier of the aircraft, every flight has a unique identifier and is used by ATC to differentiate between various flights on ground and in sky. It is of the type string as it usually contains a string of letter or numbers, for example, British Airways flight 213 from London to Boston can have a callsign "BAW13G" note that it is different from actual flight number. This is done in order to avoid confusion with flights that have similar number/pronunciation but belong to different airlines. • phase: it tells us about the current phase of the flight, in our example case this is approach. It is also of type "string". • state: it tells about the state of the components, ie, if everything is working well or if there's any failure present. It is of type "string". After the attributes we define the operations of this class:

• PCAinout(): this provides signal to Primary Control Surfaces like the Aileron, Elevators, Rudder, etc. It does so by converting pilot's action on the control stick to an electric signal and then processing that electrical signal to the desired value and sends it to the actuator that controls the surface. • cockpitdisp(): it shows the status of all the flight parameters on the display in cockpit. As can be seen in the figure 6 we have the two sub classes, "Cockpit" and "Control Surfaces" that are linked to the class "Aircraft" by the relation of association.

Cockpit class describes the interior process in the cockpit and control surfaces class explains what is happening on the exterior of the aircraft.

The attributes of cockpit are:

• mode: it informs about the corresponding mode, for example G/S (glide scope is active), LOC (on localizer), FLARE (aircraft performing flare just before touchdown), etc. It is of type "string". • disp: it is of type "string" that shows the information on the display • inst ident: it is also of "string" type that shows what is to be displayed on the screen The operations are:

• update disp(): display the current status and keep updating • give warning(): it shows the status of all the flight parameters on the display in cockpit. The attributes of Control Surfaces are:

• ident: it informs about the corresponding mode, for example G/S (glide scope is active), LOC (on localizer), FLARE (aircraft performing flare just before touchdown), etc. It is of type string.

• sensor read: it reads the value from the sensor to check for the correct position and deflection of the control surface. (type integer) The operations are:

• devip(): provide deviation to the control surface.

D. Safety Analysis

To perform safety analysis of this process we add another class called "STPA" (System Theoretic Process Analysis) is based on STAMP (System Theoretic Accident Model -Process) developed at MIT [START_REF] Leveson | Engineering a Safer World: Systems Thinking Applied to Safety[END_REF]. It translates any process to a controller-process model that has a controller which provides control actions to control the process. We use this method to assess the hazards that might be caused by improper control actions. In our case the pilot becomes the controller and the aircraft becomes the process. Based on the procedures, the pilot gives control actions to the aircraft. We try to analyze all the possible control actions and obtain their corresponding unsafe control action. This class uses inputs that check when and if a control action was provided and correspondingly gives a list of unsafe control actions. That enables the pilot to know what are the hazards corresponding to each unsafe control action that he might provide. This is seen in figure 8 The attributes of STPA are:

• time: It is of type "string".

• quality: it is of type "string" and tells us if and when was a control action proveded (for example, landing gear lowered too late) The only operation associated with this class is "listUCA" that populates a table that contains all the possible unsafe control action.

Here the STPA block provides all the probable unsafe control action to the pilot. This becomes a very labor-intensive task if done manually by the pilot. In order to filter them and have only the relevant unsafe control actions provided to the pilot we add another block called tool.

The attributes of tool are:

• ADSB: It is of type "string" and represents the data packet received from the aircraft.(Automatic dependent surveillancebroadcast (ADSB) is a surveillance technology in which an aircraft determines its position via satellite navigation and broadcasts it which is received by ground stations and other aircraft. This provides situational awareness to other aircraft and allow ATC to maintain separation. It usually contains data packets that has information about the flight like speed, heading, position, etc) • ac state: shows the state of the aircraft (all ok, failure, atc) The operations are:

• predictUCA(): based on the safety analysis method it predicts some unsafe control actions • delay(): it shows the status of all the flight parameters on the display in cockpit. To allow pilots to simulate the prediction of Unsafe Control Actions, we have developed a tool in MATLAB that takes into account the physical position of the aircraft and other flight parameters like speed, heading, and altitude. It combines these with the delay that might have been caused because of previous tasks and predicts the unsafe control action by selecting from the previously generated unsafe control actions. [START_REF] Pant | Safety Analysis of Pilot-System Interaction[END_REF] IV. INTEGRATION Once we have specified the modelling for each of the components individually we move to integrating all of them in one model. Apart from the connectors already used, we use association type of link as it can be used to show any relationship or logical connection between two classes. Table I summarizes the link between all the classes.

The names on top of the columns are the classes that act on other classes given in the first column. To explain in detail let's start with the class pilot, as we can see Pilot performs some contron actions (CA) by applying the available procedures. The control action class provides a control output to the aircraft that enables correction in trajectory or any other desired action (like lowering the landing gear). Once the action has been performed in the aircraft's control surface the class "aircraft" provides feedback to the pilot about the state of the aircraft letting the pilot know if the action was done or not. The subclass "checklists" from the procedures model also provides a feedback to the pilot about the checklists that they perform. If something is missing they can correct/perform the action and move to the next step. Next we move to the class "tool". It performs safety analysis using the before mentioned STPA process and takes into account the control actions, state of the aircraft (position and other parameters), and finally the procedures. If everything is ok after the analysis then the normal procedures are selected and continued but if something is not normal the pilot switched to non nominal procedures and the tasks are updated.

V. CONCLUSION

The idea of this paper was to show that it would be interesting to model various aspects of aircraft operations using techniques from software development. The paper presents a different approach to model the interaction of the pilot in the cockpit. This approach enables different actors like engineers, researchers to understand the integration in a common framework. It has many advantages, for example, the one we explored during the research which was to perform the safety analyses of the pilot tasks in the cockpit. This will help not only assessing the performance of the pilot in the cockpit but will also help define the functionalities of the cockpit of the future. We can have real time safety analysis that can be built over this model that check for past pilot inputs and based on the way he/she pilots the aircraft propose future actions to optimize safety/economy or provide warnings in case of potential mistakes. This also enables design engineers to define better procedures that reduce the chances of error and improve the overall piloting experience and safety of the aircraft.

Fig. 1 .

 1 Fig. 1. UML class with type of connectors

Fig. 2 .

 2 Fig. 2. Process Diagram.

Fig. 3 .

 3 Fig. 3. Approach.

Fig. 4 .

 4 Fig. 4. Procedures UML

Fig. 6 .

 6 Fig. 6. Aircraft UML

Fig. 7 .

 7 Fig. 7. Safety Analysis UML

Fig. 8 .

 8 Fig. 8. Process Diagram.

TABLE I TABLE TYPE STYLES

 ITYPE

		Pilot	CA a	Aircraft	Tool	Checklist
	Pilot			feedback		feedback
	CA a	performs			analyse
	Aircraft		controls		analyse
	Procedures	applies			selects
	a CA = Control Actions.

ACKNOWLEDGMENT

The ongoing research is being funded by Dassault Aviation. The project is under the ISAE-SUPAERO and Dassault Aviation chaire titled CASAC.


* marie.gerardin@cea.fr

• Objectives

 Improve the modelling of fission gas thermal diffusion mechanisms to better predict UO 2 fuel behaviour under irradiation  Study the interaction between gas and defect induced by irradiation

Xenon diffusion coefficient dependance with the burn-up [1]

Rare gases diffusion in UO 2

Thermal desorption measurements

Gas release fraction

Diffusion coefficient

Xe 800keV or Kr 500 keV Implantation  Gases are trapped in UO 2 for a burn-up > 2.10 22 f.m -3

 In which defects ? [Gas] (at/cm 3 )(at/cm 2 ) Depth (nm)

𝐷 𝑖 𝜕 2 𝐶 𝑖 (𝑥, 𝑡) 𝜕 2 𝑥 = 𝜕𝐶 𝑖 (𝑥, 𝑡) 𝜕𝑡 𝐶 𝑖 0, 𝑡 = 0 𝐶 𝑖 ∞, 𝑡 = 0 𝐶 1 𝑥, 0 = 1 -𝑀 × 𝐶 𝑆𝑅𝐼𝑀 𝑃𝑟𝑜𝑓𝑖𝑙𝑒 𝐶 2 𝑥, 0 = 𝑀 × 𝐶 𝑆𝑅𝐼𝑀 𝑃𝑟𝑜𝑓𝑖𝑙𝑒
C SRIM (x,0) C 1 (x,0) C 1 (x,t) C 2 (x,0) C 2 (x,t) M = 0.95 D 1 = 3.10 -17 m 2 .s -1 D 2 = 1.10 -20 m 2 .s -1
T final = 500 min

• Trapping effect

Xenon 800 keV at 1.4.10 11 Xe.cm -2 Ea̴ = 3.10 ± 0.33 eV D0 = 1.62.10 -10 m 2 .s -1

Krypton 500 keV at 2.1.10 12 Kr.cm -2 Ea̴ = 2.81 ± 0.45 eV D0 = 2.13.10 -11 m 2 .s -1 D 0 ̴ 10 -12 to 5.10 -6 m 2 .s -1

Arrhenius laws of xenon and krypton implanted in UO 2

10 13 ions.cm -2

Diffusion coefficient (D 2 ) determined on isotherms obtained at 1300°C for each dose  D 1 remains constant  D 2 decreases from  10 13 ions.cm -2 in polycrystals  10 12 ions.cm -2 in monocrystals

Trapping effect in implanted UO 2 1. Thermal desorption

𝐶 1 𝑥, 0 = 1 -𝑀 × 𝐶 𝑆𝑅𝐼𝑀 𝑃𝑟𝑜𝑓𝑖𝑙𝑒 𝐶 2 𝑥, 0 = 𝑀 × (1 -𝑭𝒓 𝒊𝒏𝒊𝒕 ) × 𝐶 𝑆𝑅𝐼𝑀 𝑃𝑟𝑜𝑓𝑖𝑙𝑒 𝐶 𝑃 𝑥, 0 = 𝑀 × 𝑭𝒓 𝒊𝒏𝒊𝒕 × 𝐶 𝑆𝑅𝐼𝑀 𝑃𝑟𝑜𝑓𝑖𝑙𝑒

  Effect of cavities induced by ion implantation on rare gases diffusion in uranium dioxide M. Gerardin 1 *, E. Gilabert 2 , D. Horlait 2 , P. Desgardin 3 , G. Carlot 1 , M-F. Barthe 3 1 CEA/DEN/DEC (Saint Paul Lez Durance, France) 2 CENBG, CNRS/IN2P3 (Gradignan, France) 3 CEMHTI, CNRS/UPR3079 (Orléans, France)

•

  Stoichiometry of the sample • Burn up (fission.m -3 ) • Literature Arrhenius laws of xenon diffusion in UO 2.00 irradiated at a low burn-up (<2.10 22 fission.m -3 )



  Gas retained in cavities induced by irradiation[7] A. Michel, NIMB 272 (2012) [8] C. Onofri, non published

• Diffusion model : two populations

	• Experimental approach
	Second Fick law
	𝑪 𝟏 : Gaz concentration mobile with 𝑫 𝟏	Burst effect
	𝑴 : Fraction of 2 populations
	𝑪 𝟐 : Gaz concentration mobile with 𝑫 𝟐	Intrinsic diffusion

 Seperated effect studies

• Conclusions

 Same diffusion mechanism between xenon and krypton  Good agreement with literature  Rare gases trapped in cavities induced by irradiation