🚀 go-pugleaf

In article <JIM.DAVIES.92Aug11180159@pierrot.prg.ox.ac.uk>,
Jim.Davies@prg.ox.ac.uk (A Wooden Fish on Wheels) writes:

|>In article <...> hufnagel@cse.uta.edu (Stephen Hufnagel) writes:
|>
|>   A simple extention is to use CSP to specify the concurrency and Z to 
|>   specify the processes. Another extention is to use path expressions
|>   to specify the concurrency and Z ...
|>     Good luck!
|>
|>On a serious note, 
|>
|>  * CSP can be used for the specification and analysis of patterns of
|>    communication (that's what a CSP process is).  These patterns can
|>    evolve concurrently, and timing information is easily included.
|>
|>  * Z can be used for the specification and analysis of state-based 
|>    or transformational systems.  Extending Z to deal with real-time
|>    systems, which are
|>
|>        ---  reactive (maintain a continuous interaction with their
|>             environment)
|>    
|>        ---  distributed (may be required to perform several tasks
|>             concurrently) 
|>
|>        ---  timed (may be subject to complex timing constraints)
|>
|>    is not an easy task.  In particular cases, a satisfactory
|>    treatment of timed or concurrent behaviour can be achieved
|>    with a suitable choice of abstraction, but this can't really
|>    be generalised. 
|>    
|>So it seems sensible to use CSP (or something very like it) and Z
|>together, using CSP to specify the patterns of communication between
|>system components, and then Z to specify the computational (or
|>transformational) aspects of the components themselves.
|>
|>This is all a bit ad-lib, I'm afraid, but I hope that it helps...

I have worked on a large real time system using Z and CSP as
specification tools. I think that it is a bit too soon to generalise
upon how to achieve such an integration, different applications require
different approaches.  If you want to build a real system you are almost
certainly going to have to accept a certain amount of vagueness in the
relationship between the two methods (especialy in the initial stages),
the precise rlationship will probably only become apparent when you have
got the ting working. If you are going to think ivory tower type
thoughts about hypothetical problems you have just cooked up youself
then it probably dosen't matter what technique you use.

After sorting out the theoretical problems, your next step will be to
try to get the TCSP LaTeX style to work with Zed...

One major caveat, don't try to specify the whole system before you start
to implement it. This is only a solution when you intend to change jobs
before the implementation phase begins.


Phill Hallam-Baker