Specification and Refinement using a Heterogeneous Notation for Concurrency and Communication

Research output: Contribution to conferencePaperpeer-review


It is shown how to combine the Z formal specification notation with a predicative
notation so as to be able to specify and reason about concurrency and communication.
The integration is carried out so as to alleviate some of the limitations
noted with previous integration approaches, such as the inability to use Z proof
rules and tools with the integrated notation. In the process, it is demonstrated that
it is not necessary to combine Z with a very different behavioural formalism in
order to reason about concurrency.
Original languageUndefined/Unknown
Publication statusPublished - 1999

Cite this