Re: Internal processes and/or external choreographies (was RE: Ev ents and States ...

I want to re-iterate my point of view on this subject.

Q: Can you define a language that can express all types of processes 
with different levels of detail and abstraction, ranging from the most 
abstract high-level choreography to the most fine-grained detail of 
implementation (in fact down to the IP packet flow)?

A: This has been proven mathematically as part of a large body of 
research. I accept any evidence that the mathematical proof is flawed, 
but until then I'm inclined to believe it is correct, and this in fact 
can be done.

Q: Do you want to define a language that does that?

A: Definitely not. Such a language already exists (e.g. pi-calculus, 
join calculus) but is too generic and so not very useful. I would prefer 
to see a language that is expressed in terms of Web services. If that 
means we can't describe how IP packets flow, or the gory details you 
will find in a piece of Java code, so be it. There's more than enough 
utility in a language that is defined at the level of Web services.

Q: Can one language define both choreographies and recusrive composition 
of services, and constrain one definition to the other?

A: A language defined at the level of Web services still has the ability 
inherit from mobile process calculus to define choreographies, recursive 
composition of services, and constrain/validate one definition against 
the other.

Q: Do you want to define a language that covers both use cases?

A: That's an open question. Maybe that language provides so much utility 
it that it's the best way to leverage our time & eneregy. With just 
minor extensions we can cover more ground and provide so much more 
capability. Maybe time is of the essence and doing less but on a shorter 
time frame is better (see 80/20 rule). We'll move such capabilities to a 
future time and just focus on choreography in this iteration. Maybe 
there is a political issue - providing such a language may stand in 
competition to other languages that specifically address implementation, 
and we want to promote variety and it's best to stay clear of this space.

Q: Assuming a choreography language that is not turing complete and any 
number of implementation languages that are turing complete, can a 
definition given in one be used to constrain/verify a definition given 
in the other?

A: You can prove at design-time or check at run-time that a more 
complete specification (the turning complete implementation) in fact 
conforms to the less complete specification (the non-complete 
choreography). Bi-simulation is one way to prove it. The whole space of 
mobile process calculus is intended to provide mathematical models for 
making such proofs at design-time and checks at run-time, and also helps 
us determine when such proofs are P problems and when they are NP problems.

Q: Can you show that by example?

A: Yes I can. But there is an infinite number of examples out there: 
order-to-pay, hire-to-fire, package-to-deliver, etc. If we try to cover 
all possible use cases by example we'll never get anything accomplished. 
If we pick some specific and interesting examples, we need to keep 
focusing on them and not constantly switch examples, as we're currently 
doing. Pick two/three examples, specify them in precise term that 
everyone agrees on, and then explore them.

But it's far more interesting to look at all possible use cases at once 
by picking up a model that describes all of them. Instead of working one 
example at a time, we work on all possible use cases at once. That's the 
benefit of using models, it gives you so much leverage in exploring a 
wider problem space and accounting for both current and future use cases.

Q: Has anyone ever done this before?

A: There are a variety of research projects and running systems based on 
mobile process calculus that anyone can download and experiment with. 
And there are several products in the market that are already taking 
advantage of these models and technologies.

Received on Friday, 11 April 2003 15:35:34 UTC