Specification and Refinement using a Heterogeneous Notation for Concurrency and Communication

Research output: Contribution to conferencePaper



Publication details

DatePublished - 1999
Original languageUndefined/Unknown


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.

Discover related content

Find related publications, people, projects, datasets and more using interactive charts.

View graph of relations