🚀 go-pugleaf

In article <...> hufnagel@cse.uta.edu (Stephen Hufnagel) writes:

   A simple extension 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!

Good man!  More of these postings please!  Couldn't agree more! 

etc. etc.

Jim Davies (Oxford CSP Group)

--

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...

Jim









--

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

In article <...> hallam@zws009.desy.de (Phillip M. Hallam-Baker) writes:

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

As the author of said style, I ought to state that the latest version
seems fairly compatible with Mike Spivey's ZED and FUZZ style files.

The CSP/LaTeX style files and the CSP/TeX symbol font WILL be available
by anonymous ftp from "ftp.comlab.ox.ac.uk" in the near future.  I'd put
them out now, but I want to produce better documentation first.  By the
way, the CSP stuff works with both old and new font selection schemes,
and both oldlfont and newlfont options to the NFSS.

Jim

--

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



>  * 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.

I feel that in claiming that timing information is easily included in
CSP that Jim is modestly undervaluing the years of endeavour that he and
others have invested in achieving this goal. Those wishing to follow in
these illustrious footsteps might find a firm grounding in metric space
topology an asset. Indeed any attempt to rigorously treat real-time
issues would benefit from study of this most relevent area of
mathematical endeavour. Afterall it was started by Newton and Liebniz.

>  * Z can be used for the specification and analysis of state-based 
>    or transformational systems.

Z is essentially a machine parsable (formal) version of classical set theory
which has a large body of literature and convention explaining how it may be
used to specify state transition systems. However it is readily
adapted to other fields of endeavour.

>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.

Using CSP within Z required little more than the definition of a new
data type and some useful operations. Eg CSP trace theory:

\begin{zed}
[EVENTS]
\end{zed}

\begin{axdef}
TRCSP : power (\power (\seq EVENTS))
\where
\forall P : \power (\seq EVENTS) \spot \\
\t1	P \in TRCSP \iff \\
\t1	\lang \rang \in P \\
\t1	\forall s : \seq EVENTS,; a : EVENTS \spot \\
\t2		s \cat \lang a \rang \in P \implies s \in P

	etc
\end{axdef}

\begin{zed}
STOP \defs \lang \rangl \\
CHAOS \defs  \power (\seq EVENTS)
\end{zed}

\begin{axdef}
\_ \detchoice \_, \_ \nondetchoice \_ : (TRCSP \cross TRCSP) \fun TRCSP
\where
...
\end{axdef}

etc

--
When soldiers form lines or hollow squares, you call it reason.
When wild geese in flight take the form of a letter V, you say instinct.
When the homogeneous atoms of a mineral arrange themselves into shapes
mathematically perfect you have nothing to say. You have not even invented a name to conceal your heroic unreason."

In article <...> brendan@cs.uq.oz.au (Brendan Mahony) writes:

   I feel that in claiming that timing information is easily included in
   CSP that Jim is modestly undervaluing the years of endeavour that he and
   others have invested in achieving this goal. Those wishing to follow in
   these illustrious footsteps might find a firm grounding in metric space
   topology an asset. 

Thanks for the appreciation.  However, the weirdo mathematics is only needed
to set up the models... in APPLICATIONS of CSP, all you need is a little set
theory... as you've pointed out

   Using CSP within Z required little more than the definition of a new
   data type and some useful operations. Eg CSP trace theory:

   \begin{zed}
   [EVENTS]
   \end{zed}

   \begin{axdef}
   TRCSP : power (\power (\seq EVENTS))
   \where
   \forall P : \power (\seq EVENTS) \spot \\
   \t1	P \in TRCSP \iff \\
   \t1	\lang \rang \in P \\
   \t1	\forall s : \seq EVENTS,; a : EVENTS \spot \\
   \t2		s \cat \lang a \rang \in P \implies s \in P

	   etc
   \end{axdef}

   \begin{zed}
   STOP \defs \lang \rangl \\
   CHAOS \defs  \power (\seq EVENTS)
   \end{zed}

   \begin{axdef}
   \_ \detchoice \_, \_ \nondetchoice \_ : (TRCSP \cross TRCSP) \fun TRCSP
   \where
   ...
   \end{axdef}

Tho' I should add that this is an example of how Z may be used to support the
mathematical reasoning required in applications of CSP.  It's not an example
of how Z and CSP can be used together in the description of a real-time
system.  

And then we hear from Julian.Rose@bristol.ac.uk ("Julian Rose")

  For my own penny's worth, no-one seems to have highlighted
  the different levels of abstraction between Z and CSP(-like
  languages). Z is about 'whats' and CSP is (mostly?) about
  'hows' and there is a difference. I think Jim Davies hinted
  this when he said "...using CSP to specify the patterns of
  communication between system components, and then Z to specify
  the computational aspects of the components themselves",

which helps to make the point---although I should say that trace and refusal
specifications are 'whats' not 'hows'---that Z and CSP can be used together to
tackle different aspects or concerns in the specification and development of a
real-time system.  The business about 'whats' and 'hows' might be easier to
fathom if you see the process algebra part of CSP as an abstract
implementation language, and the language of traces and refusals as
specifications... SAT is a refinement relation.  

In using Z and CSP together, we would be refining Z --> computational code
within modules or components, and refining CSP specifications --> CSP language
--> communication code or interface designs.  If you see what I mean... 

Jim

--

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


>Tho' I should add that this is an example of how Z may be used to support the
>mathematical reasoning required in applications of CSP.  It's not an example
>of how Z and CSP can be used together in the description of a real-time
>system.  

My PhD contains and example of one approach to this issue.

A "hybrid" model of CSP is used in which the trace contains not only an
event name but also the system state trace. That is

	TRACE \defs \seq (EVENT \cross STATE)

	or alternatively

	TRACE \defs (\seq EVENT) \cross (\seq STATE)

where EVENT is a set of event names and STATE is the system state
schema. A function

	\del : EVENT \fun \power (STATE \cross STATE)

determines the effect of each event on the system state. $\del$ is
specified as a series of Z state transition schemas.

	+-\del a-----------------------
	| \Delta STATE
	+--------------
	| ....
	+------------------------------

Each trace satisfies the invariant

	tr(1) = (a,S') \implies \exists S : InitSTATE \spot \del a

	tr(n+1) = (a,S') \land tr(n) = (b,S) \implies \del a

The technique is then to write a specification in terms of what the
allowed STATE traces are, introduce the EVENT trace through data
refinement and write a CSP program to ensure the required properties of
the STATE trace. 

Anyway that's the basic idea, modular some notational liberties in the
above.

>The business about 'whats' and 'hows' might be easier to
>fathom if you see the process algebra part of CSP as an abstract
>implementation language, and the language of traces and refusals as
>specifications... SAT is a refinement relation.  

I find it quite natural (as perhaps do other state based people) to
think of event related notations as being fundamentally algorithmic in
nature. An event is afterall something that is done, either by a system
or to a system. Of course at the most abstract level there is nothing to
distinguish event from state, except the language we throw at them, and
it is hard to argue that CSP is not about describing how something is to
be done. The specification language of traces and refusals has very
little to tell us about what we are discussing, without some mechanism
for interpretting the "meaning" of the event names, such as described
above.

>In using Z and CSP together, we would be refining Z --> computational code
>within modules or components, and refining CSP specifications --> CSP language
>--> communication code or interface designs.  If you see what I mean... 

Which is more or less the method described above, modulo the top level
of Z state-based "what" specification.

--
When soldiers form lines or hollow squares, you call it reason.
When wild geese in flight take the form of a letter V, you say instinct.
When the homogeneous atoms of a mineral arrange themselves into shapes
mathematically perfect you have nothing to say. You have not even invented a name to conceal your heroic unreason."

(for those of you who feel that there's a little too much CSP in your
 very own Z newsgroup... relax, it'll be over by Christmas)

In article <...> brendan@cs.uq.oz.au (Brendan Mahony) writes:

   I find it quite natural (as perhaps do other state based people) to
   think of event related notations as being fundamentally algorithmic in
   nature. 

Depends upon what you mean by "event".  

In standard CSP, events are instantaneous happenings in the history of a
system. This is why we don't have any problem with "true" vs. "interleaving"
concurrency, by the way... events don't describe states or actions with
duration, although a limited amount of state information may be inferred from
a record of external events.

   An event is after all something that is done, either by a system
   or to a system. Of course at the most abstract level there is nothing to
   distinguish event from state, except the language we throw at them,

I disagree, politely. Events are best seen as marker points in time, they may
delimit actions or mark state changes, but they should not be identified with
states (or actions with duration).

   it is hard to argue that CSP is not about describing how something is to
   be done. 

The theory of CSP consists of the language of processes (abstract programs)
and a series of semantic models, which are used for specification and
refinement.  These specifications need not be algorithmic; in fact, in five
years of producing CSP specifications I have yet to come up with an
useful algorithmic one.  But that may just be me :-)

             The specification language of traces and refusals has very
   little to tell us about what we are discussing, without some mechanism
   for interpretting the "meaning" of the event names, such as described
   above.

Surely this is true for any formal notation: if you don't give an intuitive
interpretation for your formal symbols, then you can't infer very much about
the "real" world.  

Returning to the point, however... what do I have to say about the hybrid
models of CSP, the models which include system state in their semantics?  The
answer is: not very much.  Some of these models are custom jobs, tailored to a
specific task---such as compiler verification---and some of them are excellent
pieces of work, but they shouldn't be confused with standard CSP.

That's not an "Oxford knows best" sort of comment.  Most of the hybrid models
have originated around here, for a start.  But a large number of complementary
design decisions have been incorporated into CSP.  These were pretty much
undocumented by the people who made them (Brookes, Hoare, Roscoe)... at least
never in the form where they were isolated or made obvious.

If you change the notion of "event", then you've got a different theory.  The
assumptions of your model of computation may not be so complementary, and you
may have to address such issues as "true" vs. "false" concurrency.  Just
because it still looks like good old CSP notation, it's not necessarily the
same animal.  For similar reasons, CSP is very different from CCS or ACP.

Jim

p.s.  to avoid any global misunderstandings, I should emphasise that 
      there's no conflict between Brendan's research and mine... we're 
      working in different areas, and any disagreement in our postings 
      is probably about terminology. 
--

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


|>Returning to the point, however... what do I have to say about the hybrid
|>models of CSP, the models which include system state in their semantics?  The
|>answer is: not very much.  Some of these models are custom jobs,
|>tailored to a
|>specific task---such as compiler verification---and some of them are
|>excellent
|>pieces of work, but they shouldn't be confused with standard CSP.

If you are looking for a useful calculus then it might be a good idea to
start by observing that both CSP and Z are already pretty complex
systems. Combining them is asking to produce something so mind boggling
huge and vast that most people will move to something rather smaller of
their own devising. If you have a problem that is entirely concerned
with the problem of Oggla nut distribution in a limited topological
space then one should only look for calculii capable of tacling
structures more complex than tree based solutions if this is of some
benefit, ie simplifies the problem.


Phill Hallam-Baker

In article <...> hallam@zeus02.desy.de (Phillip M. Hallam-Baker) writes:

   If you are looking for a useful calculus then it might be a good idea to
   start by observing that both CSP and Z are already pretty complex
   systems. 

I disagree.  

The Z notation is simpler than any other formal method I can think of.

The theory of CSP isn't that difficult to understand. 

Didn't someone like Einstein say that a theory should be "as simple as
possible, but no simpler"?  What's the use of switching to an easier 
calculus or method if it's no longer adequate?

   Combining them is asking to produce something so mind boggling
   huge and vast that most people will move to something rather smaller of
   their own devising.

It's the "divising" part that's the complicated bit.  I'm (reasonably) happy
to rely upon the skills of aircraft engineers when I fly; I don't expect to
build my own plane.  And that's more complicated than booking a ticket and
flying.  It's a bit of a useless analogy, but I'm sure you get the point. 

Just because we had to think in metric spaces in order to check that the
language and models of CSP were all hunky dory, it doesn't mean that you need
to know anything more than basic set theory in order to use them.  I'm sure
that a similar argument applies to Z...

Jim




--

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

|>In article <...> hallam@zeus02.desy.de (Phillip M. Hallam-Baker) writes:
|>
|>   If you are looking for a useful calculus then it might be a good idea to
|>   start by observing that both CSP and Z are already pretty complex
|>   systems. 
|>
|>I disagree.  
|>
|>The Z notation is simpler than any other formal method I can think of.
|>
|>The theory of CSP isn't that difficult to understand. 

That is precisely why they are useful.

|>Didn't someone like Einstein say that a theory should be "as simple as
|>possible, but no simpler"?  What's the use of switching to an easier 
|>calculus or method if it's no longer adequate?

I did not mean to imply go off and invent your own version of CSP and Z! However
in combining them you do not want to end up with something vastly more complex.


|>   Combining them is asking to produce something so mind boggling
|>   huge and vast that most people will move to something rather smaller of
|>   their own devising.
|>
|>It's the "divising" part that's the complicated bit.  I'm (reasonably) happy
|>to rely upon the skills of aircraft engineers when I fly; I don't expect to
|>build my own plane.  And that's more complicated than booking a ticket and
|>flying.  It's a bit of a useless analogy, but I'm sure you get the point. 

Yep, about as usless as my own analogy...!

What I was trying to get across was that if the cost of getting a workable
system together is having to live in a subset of CSP/Z then this is quite a
reasonable price to pay.


|>Just because we had to think in metric spaces in order to check that the
|>language and models of CSP were all hunky dory, it doesn't mean that you need
|>to know anything more than basic set theory in order to use them.  I'm sure
|>that a similar argument applies to Z...

But whence Z+CSP? It's one think to glue the two theories together with sticky
tape, quite another to do something usefull with the result. 

Occam accepts a set of simplifying assumtions which reduce the power of CSP but
create a useable system.

I would prefe to use an approach where I use the power of CSP to define an
implementation paradigm (eg a transaction processor) and then use Z to specify
at a different level of abstraction (eg the transactions themselves).

In other words I regard Jim not as a purveyor of motor cars but as a supplyer of
parts... yep you are right it is a useless analogy...

A better analogy might be to the use of design rules for silicon. I may take my
design rules and use them to demonstrate that a standard cell library is
correct, thereafter I use the standard cell library without looking under the
covers too often...

--

Phill Hallam-Baker

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


|Just because we had to think in metric spaces in order to check that the
|language and models of CSP were all hunky dory, it doesn't mean that you need
|to know anything more than basic set theory in order to use them.  I'm sure
|that a similar argument applies to Z...

As I always try to point out to people, Z IS (a formalized) set theory.

--
When soldiers form lines or hollow squares, you call it reason.
When wild geese in flight take the form of a letter V, you say instinct.
When the homogeneous atoms of a mineral arrange themselves into shapes
mathematically perfect you have nothing to say. You have not even invented a name to conceal your heroic unreason."