RE: rewriting CSP processes

["Campbell, John" <John.Campbell@xxxxxxxxxxxxxx>]

Michael


> > The words around the mathematics
> > talk about "events" being instantaneous transactions...
> 
> The "instantaneity" supposed in CSP does not necessarily imply that the
> events
> model zero-time transactions.  It is much more a simplifying assumption
> (which
> is sufficiently often valid to make it worthwhile) that if two events can
> happen in either order, with the possibility of no other event
> intervening,
> then there is nothing useful that can be added by considering the
> possibility
> that they in fact happen simultaneously. 
> 
	In terms of mathematically verifying the behavior of a system
specified
	with CSP, I agree.  At that level you are concerned with the
behaviors of
	the *specification*.  (BTW I think its meaningless to speak of
zero-time
	occurences in untimed CSP.)  

	However, in terms of *implementing* a specification, it makes 
	a great deal of sense to re-write (i.e. compile) an abstract
specification 
	into lower level constructs.  In this context, a single event in the

	abstract specification must become multiple events in the hand
shaking 
	protocol.  The question is, what are the minimal requirements 
	needed to assure that properties proven with respect to the abstract
	spec actually hold?

> The general topic to look up is probably "event refinement".  Essentially
> what
> you need to establish is that the more abstract events are made atomic
> with
> regard to one another.  That is something that you lose by looking inside
> them, unless you use appropriate protocols.
> 
	Thank you.  I'll check that. -jc
>