Abstract
This paper discusses theoretical background for the use of Z as a language for partial specification, in particular techniques for checking consistency between viewpoint specifications. The main technique used is unification, i.e. finding a (candidate) least common refinement. The corresponding notion of consistency between specifications turns out to be different from the known notions of consistency for single Z specifications. A key role is played by correspondence relations between the data types used in the various viewpoints.
This work was partially funded by the U.K. Engineering and Physical Sciences Research Council under grant number GR/K13035 and by British Telecom Labs., Martlesham, Ipswich, U.K.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
M. Ainsworth, A. H. Cruickshank, L. J. Groves, and P. J. L. Wallis. Viewpoint specification and Z. Information and Software Technology, 36(1):43–51, February 1994.
R. D. Arthan. On free type definitions in Z. In Nicholls [12], pages 40–58.
E. Boiten, J. Derrick, H. Bowman, and M.Steen. Unification and multiple views of data in Z. In J.C. van Vliet, editor, Computing Science in the Netherlands, pages 73–85, November 1995.
T. Bolognesi and E. Brinksma. Introduction to the ISO Specification Language LOTOS. Computer Networks and ISDN Systems, 14(1):25–29, 1988.
H. Bowman, J. Derrick, and M. Steen. Some results on cross viewpoint consistency checking. In Raymond and Armstrong [13], pages 399–412.
J. Derrick, H. Bowman, and M. Steen. Maintaining cross viewpoint consistency using Z. In Raymond and Armstrong [13], pages 413–424.
J. Derrick, H. Bowman, and M. Steen. Viewpoints and Objects. In J. P. Bowen and M. G. Hinchey, editors, Ninth Annual Z User Workshop, LNCS 967, pages 449–468, Limerick, September 1995. Springer-Verlag.
A.C.W. Finkelstein, D. Gabbay, A. Hunter, J. Kramer, and B. Nuseibeh. Inconsistency handling in multiperspective specifications. IEEE Transactions on Software Engineering, 20(8):569–578, August 1994.
ITU Recommendation X.901-904 — ISO/IEC 10746 1–4. Open Distributed Processing — Reference Model — Parts 1–4, July 1995.
D. Jackson. Structuring Z specifications with views. Technical Report CMU-CS-94-126, School of Computer Science, Carnegie Mellon University, Pittsburgh, PA 15213, 1994.
D. Jackson and M. Jackson. Problem decomposition for reuse. Software Engineering Journal, 1995. To appear.
J. E. Nicholls, editor. Z User Workshop, York 1991, Workshops in Computing. Springer-Verlag, 1992.
K. Raymond and L. Armstrong, editors. IFIP TC6 International Conference on Open Distributed Processing. Chapman and Hall, Brisbane, Australia, February 1995.
A. Smith. On recursive free types in Z. In Nicholls [12], pages 3–39.
J. M. Spivey. The Z notation: A reference manual. Prentice Hall, 1989.
P. Zave and M. Jackson. Conjunction as composition. ACM Transactions on Software Engineering and Methodology, 2(4):379–411, October 1993.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1996 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Boiten, E., Derrick, J., Bowman, H., Steen, M. (1996). Consistency and refinement for partial specification in Z. In: Gaudel, MC., Woodcock, J. (eds) FME'96: Industrial Benefit and Advances in Formal Methods. FME 1996. Lecture Notes in Computer Science, vol 1051. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-60973-3_93
Download citation
DOI: https://doi.org/10.1007/3-540-60973-3_93
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-60973-5
Online ISBN: 978-3-540-49749-3
eBook Packages: Springer Book Archive