🚀 go-pugleaf

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