Abstract
For systems described using a combination of Object-Z and CSP, several possibilities for refinement exist. This chapter discusses some of these. In particular, it turns out that such systems can be refined component by component, due to a correlation between refinement in Object-Z and refinement in CSP.
Excerpts from pp. 66, 73 of [4] are reprinted within this chapter with kind permission of Springer Science and Business Media.
Excerpts from pp. 200–201 of [7] are reprinted within Sect. 19.2.1 with kind permission of Springer Science and Business Media.
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
References
Araki, K., Galloway, A., & Taguchi, K. (Eds.) (1999). International Conference on Integrated Formal Methods 1999 (IFM’99). York: Springer.
Bjørner, D., Hoare, C. A. R., & Langmaack, H. (Eds.) (1990). VDM’90: VDM and Z!—Formal Methods in Software Development. Lecture Notes in Computer Science: Vol. 428. Berlin: Springer.
Boiten, E. A., & Derrick, J. (2002). Unifying concurrent and relational refinement. Electronic Notes in Theoretical Computer Science, 70(3), 94–131.
Boiten, E. A., Derrick, J., & Schellhorn, G. (2009). Relational concurrent refinement II: internal operations and outputs. Formal Aspects of Computing, 21(1–2), 65–102.
Bolton, C., & Davies, J. (2002). Refinement in Object-Z and CSP. In M. Butler, L. Petre, & K. Sere (Eds.), Integrated Formal Methods (IFM 2002). Lecture Notes in Computer Science: Vol. 2335 (pp. 225–244). Berlin: Springer.
Bolton, C., & Davies, J. (2006). A singleton failures semantics for communicating sequential processes. Formal Aspects of Computing, 18, 181–210.
Derrick, J., & Boiten, E. A. (2003). Relational concurrent refinement. Formal Aspects of Computing, 15(2–3), 182–214.
Derrick, J., & Boiten, E. A. (2012). Relational concurrent refinement part III: traces, partial relations and automata. Formal Aspects of Computing. doi:10.1007/s00165-012-0262-3
Derrick, J., & Smith, G. (2000). Structural refinement in Object-Z/CSP. In W. Grieskamp, T. Santen, & B. Stoddart (Eds.), International Conference on Integrated Formal Methods 2000 (IFM’00). Lecture Notes in Computer Science: Vol. 1945 (pp. 194–213). Berlin: Springer.
Fischer, C. (2000). Combination and implementation of processes and data: from CSP-OZ to Java. PhD thesis, University of Oldenburg.
Fischer, C., & Wehrheim, H. (1999) Model checking CSP-OZ specifications with FDR. In Araki et al. [1] (pp. 315–334).
Formal Systems (Europe) Ltd. (1997). Failures-Divergences Refinement: FDR 2. FDR2 User Manual.
He, J. (1989). Process refinement. In J. McDermid (Ed.), The Theory and Practice of Refinement. Oxford: Butterworth-Heinemann.
Hinchey, M. G. & Liu, S. (Eds.) (1997). First International Conference on Formal Engineering Methods (ICFEM’97). Hiroshima, Japan, November 1997. Los Alamitos: IEEE Comput. Soc.
Josephs, M. B. (1988). A state-based approach to communicating processes. Distributed Computing, 3, 9–18.
Lynch, N., & Vaandrager, F. (1995). Forward and backward simulations—Part I: Untimed systems. Information and Computation, 121(2), 214–233.
Olderog, E.-R., & Hoare, C. A. R. (1986). Specification-oriented semantics for communicating processes. Acta Informatica, 23, 9–66.
Reeves, S., & Streader, D. (2008). Data refinement and singleton failures refinement are not equivalent. Formal Aspects of Computing, 20(3), 295–301.
Smith, G., & Derrick, J. (1997) Refinement and verification of concurrent systems specified in Object-Z and CSP. In Hinchey and Liu [14] (pp. 293–302).
Smith, G., & Derrick, J. (2001). Specification, refinement and verification of concurrent systems—an integration of Object-Z and CSP. Formal Methods in Systems Design, 18, 249–284.
Smith, G., & Derrick, J. (2002). Abstract specification in Object-Z and CSP. In C. George & H. Miao (Eds.), ICFEM. Lecture Notes in Computer Science: Vol. 2495 (pp. 108–119). Berlin: Springer.
Woodcock, J. C. P., & Morgan, C. C. (1990) Refinement of state-based concurrent systems. In Bjørner et al. [2] (pp. 340–351).
Author information
Authors and Affiliations
Rights and permissions
Copyright information
© 2014 Springer-Verlag London
About this chapter
Cite this chapter
Derrick, J., Boiten, E.A. (2014). Refining CSP and Object-Z Specifications. In: Refinement in Z and Object-Z. Springer, London. https://doi.org/10.1007/978-1-4471-5355-9_19
Download citation
DOI: https://doi.org/10.1007/978-1-4471-5355-9_19
Publisher Name: Springer, London
Print ISBN: 978-1-4471-5354-2
Online ISBN: 978-1-4471-5355-9
eBook Packages: Computer ScienceComputer Science (R0)