Abstract
State-based refinement relations have been developed for use on the Object-Z components in an integrated Object-Z / CSP specification. However this refinement methodology does not allow the structure of a specification to be changed in a refinement, whereas a full methodology would allow concurrency to be introduced during the development life-cycle. In this paper we tackle these concerns and discuss refinements of specifications written using Object-Z and CSP where we change the structure of the specification when performing the refinement. In particular, we develop a set of structural simulation rules which allow a single Object-Z component to be refined to a number of communicating or interleaved classes. We prove soundness of these rules and illustrate them with a small example.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
J. Derrick, E. Boiten, H. Bowman, and M. Steen. Specifying and Refining Internal Operations in Z. Formal Aspects of Computing, 10:125–159, December 1998.
C. Fischer. CSP-OZ-a combination of CSP and Object-Z. In H. Bowman and J. Derrick, editors, Formal Methods for Open Object-Based Distributed Systems, pages 423–438. Chapman & Hall, 19
C. Fischer and H. Wehrheim. Model-checking CSP-OZ specifications with FDR. In K. Araki, A. Galloway, and K. Taguchi, editors, 1st International Conference on Integrated Formal Methods, pages 315–334. Springer-Verlag, 19
C.A.R. Hoare. Communicating Sequential Processes. International Series in Computer Science. Prentice Hall, 1985.
B.P. Mahony and J.S. Dong. Blending Object-Z and Timed CSP: An introduction to TCOZ. In 20th International Conference on Software Engineering (ICSE’98), pages 95–104. IEEE Computer Society Press, 1998.
R. Milner. Commnication and Concurrency. International Series in Computer Science. Prentice Hall, 1989.
G. Smith. A semantic integration of Object-Z and CSP for the specification of concurrent systems. In J. Fitzgerald, C.B. Jones, and P. Lucas, editors, Formal Methods Europe (FME’97), volume 1313 of LNCS, pages 62–81. Springer-Verlag, 1997.
G. Smith. The Object-Z Specification Language. Advances in Formal Methods. Kluwer Academic Publishers, 2000.
G. Smith and J. Derrick. Refinement and verification of concurrent systems specified in Object-Z and CSP. In M.G. Hinchey and Shaoying Lui, editors, First International Conference on Formal Engineering Methods (ICFEM’ 97), pages 293–302. IEEE Computer Society Press, 1997.
G. Smith and J. Derrick. Specification, refinement and verification of concurrent systems-an integration of Object-Z and CSP. Formal Methods in System Design, 2000. (To appear.).
J.M. Spivey. The Z Notation: A Reference Manual. Prentice Hall, 2nd edition, 1992.
J.C.P. Woodcock and J. Davies. Using Z: Specification, Refinement, and Proof. International Series in Computer Science. Prentice Hall, 1996.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2000 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Derrick, J., Smith, G. (2000). Structural Refinement in Object-Z / CSP. In: Grieskamp, W., Santen, T., Stoddart, B. (eds) Integrated Formal Methods. IFM 2000. Lecture Notes in Computer Science, vol 1945. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-40911-4_12
Download citation
DOI: https://doi.org/10.1007/3-540-40911-4_12
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-41196-3
Online ISBN: 978-3-540-40911-3
eBook Packages: Springer Book Archive