HDTenEightyP/NetNews huggingface dataset:
From: s897461@numbat.cs.rmit.OZ.AU (Alfred Yau)
Newsgroups: comp.specification
Subject: Verification Methodology For LOTOS Specification
Keywords: LOTOS Verification
Date: 17 Aug 92 09:44:21 GMT

I would like to know from anyone regarding methodology for verification
of protocols in LOTOS. Is it similar to the CCS verification methodogy ?  
Thank....

Alfred Yau
Newsgroups: comp.specification.z
From: hallam@zws009.desy.de (Phillip M. Hallam-Baker)
Subject: Re: Z and concurrent systems
Reply-To: hallam@zeus02.desy.de
Organization: wot me?
Date: Wed, 12 Aug 1992 13:50:47 GMT

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
From: Jim.Davies@prg.ox.ac.uk (A Wooden Fish on Wheels)
Newsgroups: comp.specification.z
Subject: Re: Z and concurrent systems
Date: 12 Aug 92 16:20:45 GMT
	<JIM.DAVIES.92Aug11180159@pierrot.prg.ox.ac.uk>
	<1992Aug12.135047.11085@dscomsf.desy.de>
Organization: Foundations for the Laboratory of Computer Science, Oxford
In-reply-to: hallam@zws009.desy.de's message of 12 Aug 92 13:50:47 GMT


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

--
From: brendan@cs.uq.oz.au (Brendan Mahony)
Newsgroups: comp.specification.z
Subject: Re: Z and concurrent systems
Date: 19 Aug 92 23:46:34 GMT
Reply-To: brendan@cs.uq.oz.au

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."
From: Jim.Davies@prg.ox.ac.uk (A Wooden Fish on Wheels)
Newsgroups: comp.specification.z
Subject: Re: Z and concurrent systems
Date: 13 Aug 92 16:23:41 GMT
	<JIM.DAVIES.92Aug11180159@pierrot.prg.ox.ac.uk>
	<9792@uqcspe.cs.uq.oz.au>
Organization: Foundations for the Laboratory of Computer Science, Oxford
In-reply-to: brendan@cs.uq.oz.au's message of 13 Aug 92 01:21:02 GMT


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

--
From: agoodloe@gmuvax2.gmu.edu (Alwyn Goodloe)
Subject: CSP and Z
Organization: George Mason University, Fairfax, Va.
Distribution: comp.specification.Z
Date: Fri, 14 Aug 1992 22:04:50 GMT

>(for those of you who feel that there's a little too much CSP in your
> very own Z newsgroup... 


   I like all the CSP stuff. I think alot of other people out there
probably do to. The reality is that both Z and CSP (or name your favorite
process algebra) provide different ways of looking at things.  The SA/SD
people have found that different various view points (data flow, entity 
relationship, information modeling) are complementry and possibly required
to get a realistic model of the  system. More work is clearly needed on the
kinds of hybrid models that have been discussed. 




>> relax, it'll be over by Christmas)

   
   Gee, I hope not. Maybe CSP should have its own newsgroup. Or maybe a 
hybrid models digest.

 
                                                        Alwyn E. Goodloe
                                                        PO Box 4206
                                                        Woodbridge Va. 22194
                                                   
                                               e-mail:agoodloe@gmuvax2.gmu.edu
                                
                                           Phone      (W) 703-640-3276
                                                      (H) 703-680-7808
From: brendan@cs.uq.oz.au (Brendan Mahony)
Newsgroups: comp.specification.z
Subject: Re: Z and concurrent systems
Date: 13 Aug 92 01:21:02 GMT
Reply-To: brendan@cs.uq.oz.au

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."
From: Julian.Rose@bristol.ac.uk ("Julian Rose")
Newsgroups: comp.specification.z
Subject: Z and concurrent systems bit 2
Date: 13 Aug 92 12:00:17 GMT
X-Mailer: ELM [version 2.3 PL8]
X-Mailer: mail-news 2.0.3


whoops, spotted a silly sentence in my previous email.
At the end I mean I'd do the Z bit first and then do the
CSP bit, not that I'd use Z to specify the patterns of
communication and CSP to specify the computational
aspects.

Julian
From: Julian.Rose@bristol.ac.uk ("Julian Rose")
Newsgroups: comp.specification.z
Subject: Z and concurrent systems
Date: 13 Aug 92 11:36:20 GMT
X-Mailer: ELM [version 2.3 PL8]
X-Mailer: mail-news 2.0.3


In her request, Maria Brielmann asks about a dialect of Z
to write concurrent specifications. I think she may be
referring to the Schumann-Pitt dialect of Z.

A number of following articles have mentioned the use of
CSP(-like) languages to complement a Z specification. Can
I suggest Matthew Hennessy's book, Algebraic theory of
processes, for the academic reader. It sets out the algebraic
theory of processes (surprisingly enough) where algebraic
structures, not entirely unlike Z, are described. This may
strengthen the idea that traces can be described in Z, as
Brendan Mahony suggested. 

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",
although personally I'd do it the other way around.

Julian
Newsgroups: comp.specification.z
From: lucyc@suite.sw.oz.au (Lucy Chubb)
Subject: Re: Z and Concurrency
Organization: Softway Pty Ltd
Date: 19 Aug 92 03:10:22 GMT

From article <713783720.16967@minster.york.ac.uk>, by song@minster.york.ac.uk:
> Z, VDM, state machines are state based languages
> 
> CSP, CCS, LOTOS are event based languages
> 
> Petri nets are state-event based languages
> 
> Combining Z and CSP means that you can have either states or events in the
> language, which are sometimes useful.
> 	But I wonder why we cannot define concurrency operators, trace,
> process by using Z and then use these highlevel constructs to define
> concurrent systems.  In fact B. Sufrin and Jifeng He have already made some
> efforts on this. See Specification, analysis and refinement of interactive
> processes in Formal Methods in Human-Computer Interaction, Ed. M. Harrison
> and H. Thimbleby.
> 	Same argument goes to CSP, why we cannot extend state into CSP. It
> is useful to view the state of systems so that you can know ,e.g. how many
> products in buffersm how many machines in use.

Another couple of papers to have a look at are:

@INBOOK{woodcock:90,
TITLE = "VDM '90: VDM and Z - Formal Methods in Software Development",
EDITOR = "G. Goos and J. Hartmanis",
CHAPTER = "Refinement of State-Based Concurrent Systems",
AUTHOR = "J C P Woodcock and Carroll Morgan",
PUBLISHER = "Springer-Verlag",
YEAR = "1990",
NOTE = "LNCS 428" }

and

@INBOOK{jifeng:xx,
TITLE = "Stepwise Refinement of Distributed Systems",
EDITOR = "J W de Bakker et. al.",
CHAPTER = "Various Simulations and Refinement",
AUTHOR = "He Jifeng",
PUBLISHER = "Springer-Verlag",
YEAR = "19??",
NOTE = "LNCS 430" }


		Lucy Chubb.

Softway Pty Ltd,		Phone: +61 2 698 2322;
P.O. Box 305,			Fax: +61 2 699 9174;
Strawberry Hills,		Email: lucyc@softway.oz.au
NSW 2012,
AUSTRALIA
From: hallam@zeus02.desy.de (Phillip M. Hallam-Baker)
Subject: Re: Z and concurrent systems
Reply-To: hallam@zeus02.desy.de
Organization: ZEUS Central Data Aquisition
Date: Mon, 17 Aug 1992 17:04:19 GMT

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
Newsgroups: comp.specification.z
From: hallam@zeus02.desy.de (Phill Hallam-Baker)
Subject: Re: Z and concurrent systems
Reply-To: Hallam@zeus02.desy.de
Organization: Deutsches Elektronen Synchrotron, Experiment ZEUS bei HERA
Date: Wed, 19 Aug 1992 16:09:00 GMT

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
From: Julian.Rose@bristol.ac.uk ("Julian Rose")
Newsgroups: comp.specification.z
Subject: Z and concurrency
Date: 17 Aug 92 08:49:42 GMT
X-Mailer: ELM [version 2.3 PL8]
X-Mailer: mail-news 2.0.3


In reply to J. Song (of York)

| Combining Z and CSP means that you can have either states or events in the
| language, which are sometimes useful.

It is not possible to combine Z and CSP in a simple way because they
have different underlying mathematical structures. People are talking
about using them as complementary notations.

| 	But I wonder why we cannot define concurrency operators, trace,
| process by using Z and then use these highlevel constructs to define
| concurrent systems.

Brendan Mahoney suggested his description of traces. For processes
you might be able to define a syntactic relation, ||, for example, but
you will need to embrace the semantic model of CSP to describe it.

| In fact B. Sufrin and Jifeng He have already made some
| efforts on this [the high level constructs].

I think the same authors had a publication in volume 1 of the BCS FAC
journal. There, they advanced a Z specification by a process of refinement,
if I remember correctly (correct me if I'm wrong).

In general, refinement is the kind of approach required to advance a Z
specification into a process-based one, like CSP. Someone pointed out to me
work on action systems (originally by R.J.R. Back), that attempt a
sort of refinement, some papers are published in the FAC journal.

Julian
From: song@minster.york.ac.uk
Newsgroups: comp.specification.z
Subject: Z and Concurrency
Date: 14 Aug 92 09:15:21 GMT
Organization: Department of Computer Science, University of York, England

Z, VDM, state machines are state based languages

CSP, CCS, LOTOS are event based languages

Petri nets are state-event based languages

Combining Z and CSP means that you can have either states or events in the
language, which are sometimes useful.
	But I wonder why we cannot define concurrency operators, trace,
process by using Z and then use these highlevel constructs to define
concurrent systems.  In fact B. Sufrin and Jifeng He have already made some
efforts on this. See Specification, analysis and refinement of interactive
processes in Formal Methods in Human-Computer Interaction, Ed. M. Harrison
and H. Thimbleby.
	Same argument goes to CSP, why we cannot extend state into CSP. It
is useful to view the state of systems so that you can know ,e.g. how many
products in buffersm how many machines in use.

=====================================
J. Song
Dept. of Computer Science
University of York			Concurrency is the best resources
Heslington
York, YO1 5DD
======================================