Skip Navigation
York U: Redefine the PossibleHOME | Current Students | Faculty & Staff | Research | International
Search »FacultiesLibrariesCampus MapsYork U OrganizationDirectorySite Index
Future Students, Alumni & Visitors
1998 Technical Reports

Specification and Refinement using a Heterogeneous Notation for Real-Time, Concurrency, and Communication

Richard Paige

Technical Report CS-1998-07

York University

October 29, 1998

Abstract

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.

A shortened version will appear in Proc. Integrated Formal Methods 1999, Springer-Verlag, June 1999 (York, UK).

Download paper in PDF format.



The documents distributed by this server have been provided by the contributing authors as a means to ensure timely dissemination of scholarly and technical work on a noncommercial basis. Copyright and all rights therein are maintained by the authors or by other copyright holders, notwithstanding that they have offered their works here electronically. It is understood that all persons copying this information will adhere to the terms and constraints invoked by each author's copyright. These works may not be reposted without the explicit permission of the copyright holder.