Abstract. Do process calculi have anything helpful to say about web service choreography? Maybe. These slides are from a talk for the w3c web-service choreography group. I've tried to make the slides a 'primer', one that will help web-service-people get an idea about what process calculi offer.
The remainder of this web page contains additional material and citations, more technical than was appropriate for the talk.
The easiest process calculus language is the pi calculus. Here is a minimal example:
proxy<y,"hello"> | !proxy(chan z,string s);z<s> }
The vertical bar separates to 'processes' (threads) which run in parallel. The first sends a channel-name and a string over the channel called 'proxy'. Meanwhile, in parallel, the second can receive such messages over the channel 'proxy', and sends them on. The exclamation mark means that it can keep handling further requests.
There's also a 'choice' command x(a);C2 + y(b);C2 which can respond either to x or to y. And a command new x; to create a new channel. And that's it!
I think the pi calculus is a concise alternative to writing automatas. And also, when channel-names start getting passed around (like 'y' in the above example) then this is awkward to write in automata diagrams. But this is still speculation. People haven't written enough real programs in the pi calculus itself, yet, to know how good it is as a language.
Bisimulation is a way to judge whether two programs (or specifications) are equivalent. It involves paying attention to the states of each, and to the possibilities still open at each state. Let P, P' be the states in the left hand program, and Q, Q' be the states in the right hand.
A bisimulation S is a relation between states such that
whenever P S Q then:
if state P can do an action to get to state P', then
state Q must also be able to do the same action to end in some state Q',
where P' and Q' are themselves related by S.
Basically, you draw the state diagrams of left and right programs. Then draw a set of lines to connect each state on the left to one on the right, and vice versa. (You can have many lines going from, or coming to, the same state). For every action that a left-hand-state can make, then all the equivalent right-hand-ones must also make, and the results must still be equivalent.
This definition is a very basic old one, back from the days of CCS. (CCS is an old process calculus from the 80s which doesn't allow you to pass channel-names as arguments. For more on it, read the book "Communicating and concurrent systems" by Milner.)
Bisimulation is symmetric. This makes you wonder: is it appropriate to use bisimulation to compare an implementation and a specification? Shouldn't we instead allow the implementation to do extra stuff?
You can partly fix this problem within bisimulation: by only comparing on those actions that are mentioned in the specification. That way, even if the implementation accepts a "extra-functionality" message and goes on to do something special, it still passes the bisimulation test.
You can fix the remainder of this problem with an asymmetric version called coupled bisimulation: a slightly more complicated definition that allows the implementation more leeway. (In particular, it is allowed to make a commitment step-by-step rather than all at once.)
Consider the program u(x);x<"hello">;. This receives a channel-name, and then sends a message over it. The question is, how do you account for this in bisimulation? Here's one attempt:
If P can perform the action u(x) and end in state P' -- i.e. it receives the formal argument x over channel u -- then the corresponding state Q must also be able to receive an argument and end in Q'. And also, P' and Q' must be equivalent no matter what actual value was bound to x in them.
This happens to be called "late bisimulation". It's a bit arbitrary, because we picked the 'bind any value to x' clause out of the air. And indeed, this bisimulation doesn't quite work. That is, it's possible for a client to distinguish between an implementation and a specification, even when the implementation and specification are late-bisimilar.
The problem boils down to the fact that we're passing channels as arguments in messages. And it's hard to define bisimulation to account for this. So instead, researchers use a clear unambiguous definition, called congruence...
We say that a specification and implementation are congruent, if no client can distinguish them. This is a clear and unambiguous definition, and it's clearly what we're aiming for. Problem is, it's too hard to decide whether two programs are congruent. So, instead, researchers try to find conservative approximations -- ones that are overly-cautious, but at least they're practical!
Actually, even "congruence" isn't entirely unambiguous. It depends on what capabilities we allow for the clients, known as "contexts" in the literature. How much can the clients change during runtime? (reduction-closed vs shallow congruence). Can a client observe the system receiving a message, or only emitting a message? (synchronous vs asynchronous calculus). Can the client incorporate the program as an internal subroutine, or only access an existing already-running program? (full congruence vs equivalence). The first of these points turns out not to matter, but the rest of them lead to practically different definitions.
How does the complexity of the language relate to the complexity of bisimulation?
(1) The simplest calculus, CCS, has no reconfigurability at all. This has the easiest bisimulation.
(2) Then you add "internal mobility", which means you're only ever allowed to send the names of channels at the same time as creating them. The maths of this bisimulation is a bit harder, but not too much. The calculus here is called pi-I.
(3) Then you add "external mobility" aka "output capability", which means you can send the names of existing channels. This makes the maths of bisimulation more complicated. Biztalk does this, and the Join Calculus and Localised Pi Calculus. (which also have the ability to create fresh channels.)
(4) Then you add "input cabapility", which means that when someone tells you the name of an existing channel, you can receive messages over that channel. Bisimulation is the same complexity as above. The pi calculus has input capability, and also MS Highwire. People have avoided input capability in the past, on the grounds that it seemed too hard to implement. But recently, "fusions" seem to make its implementation possible.