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.
This work was partially funded by British Telecom Research Labs., and the EPSRC under grant number GR/K13035.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
References
E. Boiten, J. Derrick, H. Bowman, and M. Steen. Consistency and refinement for partial specification in Z. In M.-C. Gaudel and J. Woodcock, editors, FME'96: Industrial Benefit of Formal Methods, Third International Symposium of Formal Methods Europe, volume 1051 of Lecture Notes in Computer Science, pages 287–306. Springer-Verlag, March 1996.
T. Bolognesi and E. Brinksma. Introduction to the ISO Specification Language LOTOS. Computer Networks and ISDN Systems, 14(1):25–59, 1988.
E. Brinksma. A theory for the derivation of tests. In S. Aggarwal and K. Sabnani, editors, Protocol Specification, Testing and Verification, VIII, pages 63–74, Atlantic City, USA, June 1988. North-Holland.
E. Brinksma, G. Scollo, and C. Steenbergen. Process specification, their implementation and their tests. In B. Sarikaya and G. v. Bochmann, editors, Protocol Specification, Testing and Verification, VI, pages 349–360, Montreal, Canada, June 1986. North-Holland.
E. Cusack. Object oriented modelling in Z for Open Distributed Systems. In J. de Meer, V. Heymer, and R. Roth, editors, IFIP TC6 International Workshop on Open Distributed Processing, pages 167–178, Berlin, Germany, September 1991. North-Holland.
E. Cusack and G. H. B. Rafsanjani. ZEST. In S. Stepney, R. Barden, and D. Cooper, editors, Object Orientation in Z, Workshops in Computing, pages 113–126. Springer-Verlag, 1992.
E. Cusack and C. Wezeman. Deriving tests for objects specified in Z. In J. P. Bowen and J. E. Nicholls, editors, Seventh Annual Z User Workshop, pages 180–195, London, December 1992. Springer-Verlag.
J. Derrick, H. Bowman, E. Boiten, and M. Steen. Comparing LOTOS and Z refinement relations. In FORTE/PSTV'96, pages 501–516, Kaiserslautern, Germany, October 1996. Chapman & Hall.
J. Derrick, E.A.Boiten, H. Bowman, and M. Steen. Supporting ODP — translating LOTOS to Z. In First IFIP International workshop on Formal Methods for Open Object-based Distributed Systems, Paris, March 1996. Chapman & Hall.
M. Hennessy. Algebraic Theory of Processes. MIT Press, 1988.
C. A. R. Hoare. Communicating Sequential Processes. Prentice Hall, 1985.
ITU Recommendation X.901-904 — ISO/IEC 10746 1-4. Open Distributed Processing — Reference Model — Parts 1–4, July 1995.
L. Lamport. TLZ. In J.P. Bowen and J.A. Hall, editors, ZUM'94, Z User Workshop, pages 267–268, Cambridge, United Kingdom, June 1994.
P. Mataga and P. Zave. Formal specification of telephone features. In J. P. Bowen and J. A. Hall, editors, Eighth Annual Z User Workshop, pages 29–50, Cambridge, July 1994. Springer-Verlag.
R. Milner. Communication and Concurrency. Prentice-Hall, 1989.
G. H. B. Rafsanjani. ZEST — Z Extended with Structuring: A users's guide. Technical report, BT, June 1994.
S. Rudkin. Modelling information objects in Z. In J. de Meer, V. Heymer, and R. Roth, editors, IFIP TC6 International Workshop on Open Distributed Processing, pages 267–280, Berlin, Germany, September 1991. North-Holland.
J. M. Spivey. The Z notation: A reference manual. Prentice Hall, 1989.
B. Strulo. How firing conditions help inheritance. In J. P. Bowen and M. G. Hinchey, editors, Ninth Annual Z User Workshop, LNCS 967, pages 264–275, Limerick, September 1995. Springer-Verlag.
C. Wezeman and A. J. Judge. Z for managed objects. In J. P. Bowen and J. A. Hall, editors, Eighth Annual Z User Workshop, pages 108–119, Cambridge, July 1994. Springer-Verlag.
J. Woodcock and J. Davies. Using Z: Specification, Refinement, and Proof. Prentice Hall, 1996.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1997 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Derrick, J., Boiten, E., Bowman, H., Steen, M. (1997). Weak refinement in Z. In: Bowen, J.P., Hinchey, M.G., Till, D. (eds) ZUM '97: The Z Formal Specification Notation. ZUM 1997. Lecture Notes in Computer Science, vol 1212. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0027298
Download citation
DOI: https://doi.org/10.1007/BFb0027298
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-62717-3
Online ISBN: 978-3-540-68490-9
eBook Packages: Springer Book Archive