Thread View: comp.specification.z
2 messages
2 total messages
Started by song
Fri, 14 Aug 1992 09:15
Z and Concurrency
Author: song
Date: Fri, 14 Aug 1992 09:15
Date: Fri, 14 Aug 1992 09:15
25 lines
1351 bytes
1351 bytes
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 ======================================
Re: Z and Concurrency
Author: Lucy Chubb
Date: Wed, 19 Aug 1992 03:10
Date: Wed, 19 Aug 1992 03:10
49 lines
2142 bytes
2142 bytes
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
Thread Navigation
This is a paginated view of messages in the thread with full content displayed inline.
Messages are displayed in chronological order, with the original post highlighted in green.
Use pagination controls to navigate through all messages in large threads.
Back to All Threads