Z and other design methodologies

Thread View: comp.specification.z

2 messages

[T] Back to Threads [V] Tree View [G] Group Articles

2 total messages Started by Mike Kirby Tue, 26 Jan 1993 15:46

#130

Author: Mike Kirby
Date: Tue, 26 Jan 1993 15:46

20 lines
1347 bytes

I am a new user to Z.  I've picked up most of the syntax.  But I have some questions
about how to go about applying it.  One of the most useful features of your 
traditional design and analysis methodologies (like rumbaugh, shlaer/mellor, etc..) is
the state-transition diagram.  Is there a way in Z to model not only the
states, but the transitions into and outof different states?  It would be
nice if I could specify states, and then when  I specify my member functions
I can describe the state that this function is valid for. 

I am using the Object-Z Specification descripted in TR91-1 from Duke et al.
Is there a newer specification that is available?  

Thanks,
Mike Kirby
Xerox Corp
E-mail: kirby.roch803@xerox.com

Refs:

Roger King, et al., "The Object-Z Specification Language, Version 1,"  Technical
Report 91-1, University of Queensland, Queensland Australia, May 1991

Re: Z and other design methodologies

#128

Author: Jon Jacky
Date: Wed, 27 Jan 1993 17:40

22 lines
1528 bytes

In article <1993Jan26.154610.27454@spectrum.xerox.com> kirby@xerox.com writes:

> One of the most useful features of your 
> traditional design and analysis methodologies (like rumbaugh, shlaer/mellor,
> etc..) is the state-transition diagram.  Is there a way in Z to model not 
> only  the states, but the transitions into and out of different states? 

Yes.  If S is the state schema that contains the state variables 
for the subsystem modelled by the diagram,
then each bubble in the diagram represents a set of states distinguished
by some predicate on those variables.   So, bubbles labelled A and B can be 
represented by Z state schemas also:

	SA =^=  [ S  | ... predicate for state SA ... ]

	SB =^=  [ S  | ... predicate for state SB ... ]

Then the transition from A to B is simply:

	TrAB =^=  SA /\ SB'

- Jon Jacky, jon@radonc.washington.edu, University of Washington, Seattle USA

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