School of Computing

Weak refinement in Z

J. Derrick, E.A. Boiten, H. Bowman, and M. Steen

In J.P. Bowen, M.G. Hinchey, and D.Till, editors, ZUM '97: The Z Formal Specification Notation, volume 1212 of Lecture Notes in Computer Science, pages 369-388, Reading, April 1997. Springer-Verlag.

Abstract

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.

Download publication 78 kbytes

Bibtex Record

@conference{190,
author = {J. Derrick and E.A. Boiten and H. Bowman and M. Steen},
title = {Weak refinement in {Z}},
month = {April},
year = {1997},
pages = {369-388},
keywords = {Refinement; Distributed Systems; Internal Operations; Process Algebras; Concurrency; Z},
note = {},
doi = {},
url = {http://www.cs.kent.ac.uk/pubs/1997/190},
    ISBN = {3-540-62717-0},
    address = {Reading},
    booktitle = {ZUM '97: The Z Formal Specification Notation},
    editor = {J.P. Bowen and M.G. Hinchey and D.Till},
    publisher = {Springer-Verlag},
    refereed = {yes},
    series = {Lecture Notes in Computer Science},
    volume = {1212},
}

School of Computing, University of Kent, Canterbury, Kent, CT2 7NF

Enquiries: +44 (0)1227 824180 or contact us.

Last Updated: 12/03/2012 17:02