[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]


Hi Gordon,

> Is anyone else bored of all this process algebra vs OO debate. I am sure
> we are all well versed in both and their pros and cons.

The pros are well advertised but the cons are largely unacknowledged.
I guess many of us in University teaching are getting more uncomfortable
in pushing the pros on our students ... and this embarassment prompts
us to moan about it ... now and again ... just a little ... :)

But doing so just by anecdote doesn't progress things very much ... and
the CACM seems to be a big offender in this regard.  Whatever happened
to the CACM - it used to be *the* journal?

> 1) Dynamic object interactions: the need for dynamic alphabets and channel
> passing: pi&pict vav csp&occam

Absolutely!  The new (KRoC/Linux) occam will (soon) have dynamic channel
(and other event) creation, processes whose alphabets change over time
(as they enroll/resign from events), communicating channels and processes
over channels ... well some of this stuff will be a bit sooner than the
rest!  Of course, JCSP already has all of the above :) ... its security,
though, relies on the JCSP programmer playing the design patterns correctly.
For occam, the compiler will enforce correct play ... and the management
overheads will be around 500 times lighter.

occam has never been an absolute refelection of CSP.  It is both less than
it (e.g. no output guards, recursion etc.) and more than it (e.g. a block
structured name space, channel/event parametrisation of processes, PRI
choices and FAIR ones).  The "less than it" is very important for pragmatic
reasons - full blown CSP is too expensive to implement (probably).  The
"more than it" owes some dues to Milner's CCS (and pi-calculus) - especially
regarding name spaces!

> 4) MAXCHICKENS=3: Why do humans need to set the limits in CSP models, are
> there cases where FDR could work it out for a given subset of proofs?
> (Can you see that it is the tension between mathematical cleaness and ease
> of commercial applicability that is most interesting to me).

Yes - interesting problems here.  We built a CSP model of Java's monitor
primitives (synchronized/wait/notify/notifyAll) and then were able to use
the FDR model checker to verify the correctness of JCSP (and CTJ) channels
and the JCSP ALT.  At least, on the last item, we were able to verify the
correctness of a 2-way ALT over channel input guards - which was a great
relief given the difficulties in constructing and understanding the logic
of monitor implementations.

Now, we could have extended our model to verify (hopefully) the correctness
of a 3-way ALT.  But we haven't.  What we really want to do is verify the
correctness of the n-way ALT, for all n >= 0.  Humm ...

Another wish: I'd like a CSP-like algebra that is a consistent complete
subset of CSP that reflects only the occam-implemented (i.e. unit time
complexity) primitives.  I'd like a model checker specific for that subset
and semantics preserving transformer tools.  Then I'd like that extended
to deal with PRI ALTs, FAIR ALTs, timeout and SKIP guards (and the model
checkers/transformers upgraded to match).  Plus the dynamic alphabet stuff
we have in JCSP and (soon) occam.  Plus SHARED channels.

Plus channels of channel-ends and channels of processes.  And an event
interface algebra to allow me to abstract the essential information as
to what a process does and how it engages with its environment to do it
(need to combine this with Z specifications) ...  and will allow me decent
flexibility to derive processes from already existing processes (in a way
that works *much* better than OO inheritance).

And, then, we can have breakfast!