🚀 go-pugleaf

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