Fwd: W3C Usecase Description encoding in pi-calculus

Begin forwarded message:

> From: Nobuko Yoshida <yoshida@doc.ic.ac.uk>
> Date: 7 April 2004 12:27:15 BST
> To: Steve Ross-Talbot <steve@enigmatec.net>, Nickolas Kavantzas 
> <nickolas.kavantzas@oracle.com>, Robin Milner 
> <Robin.Milner@cl.cam.ac.uk>, Kohei Honda <kohei@dcs.qmul.ac.uk>
> Cc: Nobuko Yoshida <yoshida@doc.ic.ac.uk>
> Subject: W3C Usecase Discription
>
> Dear all,
>
> The attachment are a model description for W3C Choreography
> and my proposal of a deadlock-free typing system.
>
> [1] Explanation of the basic idea of [2].
> [2] 7 pages pdf scanned by a scanner
>
> It would be difficult to understand materials of this document
> fully without discussion using a blackboard. I am happy to
> answer any questions from you.  It would be easier to meet
> sometime and discuss together (at least by phone).
>
> Best regards,
> Nobuko Yoshida
> A Model Description for WS Choreography and its Types
>
> Abstract
>
> This document proposes a model description for
> the usecases in Web Services Choreography Requirements 1.01
> dated 3 December 2003, and its deadlock free typing system.
> It also presents an idea to model timeout simply
> in WS Choreography. There are three key ideas:
>
> [1] Session Types
> [2] Causality-based Types
> [3] Local Time Out
>
> A couple of key references are attached at the end.
>
> This document focuses on Usecase 4.2 D-UC-001 Travel Agent,
> in which most of key features are found. I believe the idea
> extends to other (present and future) usecases, but this
> should be examined individually.
>
> Page 1:
>
> This page describes the basic idea.
>
> In the standard programming languages such as ML, the usecase in 4.2
> can be naturally represented using "case" or "switch" constructors. If
> the client request is matched by "request1" in the server, then M1 is
> executed; if it is matched by "request2", then M2 is executed.  Note 
> that
> request1 and request2 are labels, not names.  This gives us a hint to
> a type system for the usecases. Concretely we may extend the 
> well-studied
> sum type in the functional languages [Pierce 02].
>
> A proposed typing system (branching/selection [HVK,BHY])
> is based on the idea of this sum type. The type of page 1
> is a channel type which is assigned by a channel.
> T + T is called branching type (in [HVK,BHY], this is written
> as [T & T]). ; denotes  sequencing.
>
> The code is read:
>
>   if a server gets request1 with an argument of a vector INT,
>   then it selects a client's ack1 branch with an argument
>   of char and int.
>
>   if a server gets request1 with an argument of a vector INT,
>   then it selects a client's ack2 branch with an argument of char.
>
> Page 2:
>
> This page shows how we can describe the Usecase by
> a pi-calculus with branching/selection.
>
> The first process is a server.
> -- !a(x).P denotes an replicated input. 
> -- \overline{x}(c)P denotes an bound output (i.e. c is a new linear
> name). (I omit overline in this text from now on).
> -- c[label1(x).P1 & label2(y).P2] denotes branching. 
> -- c<ack<v>;P denotes selection output with value v.  
> -- P;Q denotes sequencing. 
>
> The behaviour of branching can be given by the following
> reduction rule.
>
> c[request1(x).P1 & request2(y).P2] | c<request1<k>;P
>
>       --> P1[v/x] | P
>
> In this page, the server accepts the request repeatedly (by !).
> First the client sends its private name x, then the server
> sends back its private name c. Then via c, the client
> selects the service "request2" with value its id, card-id and date
> etc. then server sends ack(v) to the client.
> Once the server and the client starts interactions,
> a new session (linear) channel 'c' ensures non-interference.
>
> Page 3.
> This page describes the Usecase 2. in 4.2.1.1.
>
> Prices and availability matching the client requests are returned
> to the client. The client can then perform one of the following
> actions:
>
>    1. The client can refine their request for information,
>       possibly selecting more services from the provider (Repeat step 
> 2). OR
>
>    2. The client may reserve services based on the response. OR
>    3. The client may quit the interaction with the travel agent.
>
> For 3, we use the standard recursive agent [Milner 90].
> A(a) = .... A(a).
>
> Page 4:
>
> This page describes the Usecase 3. in 4.2.1.1.
>
> Usecase 3 says:
>
> When a customer makes a reservation, the travel agent
> then check the availability of the requested services
> with each service provider.
>
> Q (which is found in the second branch in the
> server P1 in Page 3) starts interaction with the other
> service provider with channel t. Then check availability.
> If it is available, then it returns "ok". etc.
>
> Page 5:
>
> This page describes Usecase 7, which says:
>
>   Between the reservation time and the final date for confirmation, the
>   client may modify the reservation. Modifications may include
>   cancellation of some services or the addition of extra services.
>
> This situation is very simply represented by local time out,
> which is studied by [Berger 02].
>
> The final line says that after 100 days, if there is no confirmation
> from the server, then it sends the abort.
>
> Page 6:
>
> The syntax of the typing system. There are three elements.
> [1] Tv: Sorting [Milner 92]
> [2] T : Session Types [HVK]
> [3] Gamma: Causality type [YBH]
>
> The examples show how we can avoid deadlock by checking the causality
> between channels.
>
> The last example cutted off by scanning is
>
> a:T --> b:T and  b:T --> a:T means deadlock (so it should not be 
> typable).
>
> Page 7:
>
> The first example is a type of channel a of the server.
> The last example is a type of the whole server, which
> includes the causality at a then t.
>
> This is also cutted off!
>
> a:(type1;type2 + type3) --> t:type4;type5
>
> Extensions.
>
> -- With this simple typing system, we believe it is possible 
>    to handle the Global View via subtyping and guarantees deadlock-
>    freedom. We believe this typing system can be used for typing
>    code written in recent Choreography  Language Description 1.0
>    (April 3 2004).
>
> -- We believe implementing the typing system is much easier than 
>    general CCS-like types because we do not have to use
>    indirect model-checking. Sorting, branching/selection
>    types and session types are well-studied and some of them are
>    already implemented by researchers.
>
> -- Session-based communication is representable by purely by 
> asynchronous
>    message passing. So it can be mixed with asynchronous communication
>    consistently as needed.
>
> Concluding Remarks.
>
> It would be difficult to understand materials of this document
> fully without discussion using a blackboard. We are happy to
> answer any questions from you.  It would be easier to meet
> sometime and discuss together (at least by phone).
>
> Reference:
>
> [Milner 92] Robin Milner,
> The Polyadic Pi-Calculus: A Tutorial,
> Proceedings of the International Summer School on
> Logic Algebra of Specification, Marktoberdorf, 1992.
>
> [Berger 02] Martin Berger,
> Towards Abstractions for Distributed Systems,
> Ph.D. Thesis, Imperial College London, 2002.
> Available from: www.dcs.qmul.ac.uk/~martinb
>
> [HVK] Honda, K., Vasconcelos, V. and Kubo, M.,
> Language Primitives and Type Discipline
> for Structured Communication-Based Programming.
> ESOP'98, LNCS 1381, 122--138. Springer-Verlag, 1998.
> Available from: www.dcs.qmul.ac.uk/~kohei
>
> [Pierce 02]
> Pierce, B.C.,
> Types and Programming Languages, MIT, 2002.
>
> [YBH]
> Nobuko Yoshida, Martin Berger and Kohei Honda,
> Strong Normalisation in the Pi-Calculus,
> To appear in Journal of Information and Computation.
> Available from: www.doc.ic.ac.uk/~yoshida.
>
>
>
>
>
>
>
>
>
>