Specification and Refinement using a Heterogeneous Notation for Concurrency and Communication

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.