Weak refinement in Z

Derrick, John and Boiten, Eerke Albert and Bowman, Howard and Steen, Maarten (1997) Weak refinement in Z. In: Bowen, Jonathan P. and Hinchey, Michael G. and Till, David, eds. ZUM '97: The Z Formal Specification Notation. Lecture Notes in Computer Science, 1212. Springer-Verlag, Reading pp. 369-388. ISBN 3-540-62717-0. (doi:https://doi.org/10.1007/BFb0027298) (Full text available)

Other (zip)
Download (80kB)
Download (250kB)
Download (215kB)
Official URL


An important aspect in the specification of distributed systems is the role of the internal (or unobservable) operation. Such operations are not part of the user interface (i.e. the user cannot invoke them), however, they are essential to our understanding and correct modelling of the system. Various conventions have been employed to model internal operations when specifying distributed systems in Z. If internal operations are distinguished in the specification notation, then refinement needs to deal with internal operations in appropriate ways. However, in the presence of internal operations, standard Z refinement leads to undesirable implementations. In this paper we present a generalization of Z refinement, called weak refinement, which treats internal operations differently from observable operations when refining a system. We illustrate some of the properties of weak refinement through a specification of a telecommunications protocol. Keywords Refinement; Distributed Systems; Internal Operations; Process Algebras; Concurrency.

Item Type: Conference or workshop item (Paper)
Uncontrolled keywords: Refinement; Distributed Systems; Internal Operations; Process Algebras; Concurrency; Z Refinement - Distributed Systems - Internal Operations - Process Algebras - Concurrency
Subjects: Q Science > QA Mathematics (inc Computing science) > QA 76 Software, computer programming,
Divisions: Faculties > Sciences > School of Computing > Theoretical Computing Group
Depositing User: Eerke Boiten
Date Deposited: 25 Jul 2009 22:14 UTC
Last Modified: 20 Oct 2015 14:27 UTC
Resource URI: https://kar.kent.ac.uk/id/eprint/21516 (The current URI for this page, for reference purposes)
ORCiD (Boiten, Eerke Albert): http://orcid.org/0000-0002-9184-8968
  • Depositors only (login required):


Downloads per month over past year