[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
RE: rewriting CSP processes
> > The words around the mathematics
> > talk about "events" being instantaneous transactions...
> The "instantaneity" supposed in CSP does not necessarily imply that the
> model zero-time transactions. It is much more a simplifying assumption
> is sufficiently often valid to make it worthwhile) that if two events can
> happen in either order, with the possibility of no other event
> then there is nothing useful that can be added by considering the
> that they in fact happen simultaneously.
In terms of mathematically verifying the behavior of a system
with CSP, I agree. At that level you are concerned with the
the *specification*. (BTW I think its meaningless to speak of
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
into lower level constructs. In this context, a single event in the
abstract specification must become multiple events in the hand
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
> you need to establish is that the more abstract events are made atomic
> 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