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. 1 Introduction The Z notation [15] has proven to be useful and appropriate for specifying and reasoning about sequential software and hardware systems. The strengths of Z include its ability to construct specifications by parts, its growing tool support, and its proof system. Recent work on Z has studied its application to concurrent systems. In this growing body of work, there are two general classes of approaches: 1. Extension approaches, which apply Z, perhaps with som..