Non-atomic Refinement in Z and CSP

  • John Derrick
  • Heike Wehrheim
Part of the Lecture Notes in Computer Science book series (LNCS, volume 3455)


In this paper we discuss the relationship between notions of non-atomic (or action) refinement in a state-based setting with that in a behavioural setting. In particular, we show that the definition of non-atomic coupled downward simulation as defined for Z and Object-Z is sound with respect to an action refinement definition of CSP failures refinement.


Transition System Operational Semantic Parallel Composition Process Algebra Couple Simulation 
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.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Aceto, L.: Action Refinement in Process Algebras. CUP, London (1992)Google Scholar
  2. 2.
    Boiten, E.A., Derrick, J.: IO-refinement in Z. In: Evans, A., Duke, D.J., Clark, T. (eds.) 3rd BCS-FACS Northern Formal Methods Workshop, September 1998. Springer, Heidelberg (1998), Google Scholar
  3. 3.
    Bolton, C., Davies, J.: A Singleton Failures Semantics for Communicating Sequential Processes. In: Formal Aspects of Computing. Under consideration (2002)Google Scholar
  4. 4.
    Bolton, C., Davies, J.: Refinement in Object-Z and CSP. In: Butler, M., Petre, L., Sere, K. (eds.) IFM 2002. LNCS, vol. 2335, pp. 225–244. Springer, Heidelberg (2002)CrossRefGoogle Scholar
  5. 5.
    Derrick, J., Boiten, E.: Non-atomic refinement in Z. In: Woodcock, J.C.P., Davies, J., Wing, J.M. (eds.) FM 1999. LNCS, vol. 1709, pp. 1477–1496. Springer, Heidelberg (1999)CrossRefGoogle Scholar
  6. 6.
    Derrick, J., Boiten, E.A.: Refinement in Z and Object-Z. Springer, Heidelberg (2001)zbMATHGoogle Scholar
  7. 7.
    Derrick, J., Boiten, E.A.: Relational concurrent refinement. Formal Aspects of Computing 15(2-3), 182–214 (2003)zbMATHCrossRefGoogle Scholar
  8. 8.
    Derrick, J., Wehrheim, H.: Using coupled simulations in non-atomic refinement. In: Bert, D., P. Bowen, J., King, S. (eds.) ZB 2003. LNCS, vol. 2651, pp. 127–147. Springer, Heidelberg (2003)CrossRefGoogle Scholar
  9. 9.
    Fischer, C.: CSP-OZ - a combination of CSP and Object-Z. In: Bowman, H., Derrick, J. (eds.) Second IFIP International conference on Formal Methods for Open Object-based Distributed Systems, July 1997, pp. 423–438. Chapman & Hall, Boca Raton (1997)Google Scholar
  10. 10.
    Fischer, C.: How to combine Z with a process algebra. In: P. Bowen, J., Fett, A., Hinchey, M.G. (eds.) ZUM 1998. LNCS, vol. 1493, pp. 5–23. Springer, Heidelberg (1998)CrossRefGoogle Scholar
  11. 11.
    Galloway, A., Stoddart, W.: An operational semantics for ZCCS. In: Hinchey, M.G., Liu, S. (eds.) First International Conference on Formal Engineering Methods (ICFEM 1997), Hiroshima, Japan, November 1997, pp. 272–282. IEEE Computer Society Press, Los Alamitos (1997)CrossRefGoogle Scholar
  12. 12.
    He, J.: Process simulation and refinement. Formal Aspects of Computing 1, 229–241 (1989)CrossRefGoogle Scholar
  13. 13.
    Janssen, W., Poel, M., Zwiers, J.: Actions systems and action refinement in the development of parallel systems. In: Groote, J.F., Baeten, J.C.M. (eds.) CONCUR 1991. LNCS, vol. 527, pp. 298–316. Springer, Heidelberg (1991)Google Scholar
  14. 14.
    Jifeng, H.: Process refinement. In: McDermid, J. (ed.) The Theory and Practice of Refinement, Butterworths (1989)Google Scholar
  15. 15.
    Josephs, M.B.: A state-based approach to communicating processes. Distributed Computing 33, 9–18 (1988)CrossRefGoogle Scholar
  16. 16.
    Mahony, B.P., Dong, J.S.: Blending Object-Z and timed CSP: An introduction to TCOZ. In: Futatsugi, K., Kemmerer, R., Torii, K. (eds.) 20th International Conference on Software Engineering (ICSE 1998). IEEE Press, Los Alamitos (1998)Google Scholar
  17. 17.
    Parrow, J., Sjödin, P.: Multiway Synchronisation Verified with Coupled Simulation. In: Cleaveland, W.R. (ed.) CONCUR 1992. LNCS, vol. 630, pp. 518–533. Springer, Heidelberg (1992)CrossRefGoogle Scholar
  18. 18.
    Rensink, A.: Action Contraction. In: Palamidessi, C. (ed.) CONCUR 2000. LNCS, vol. 1877, pp. 290–304. Springer, Heidelberg (2000)CrossRefGoogle Scholar
  19. 19.
    Rensink, A., Wehrheim, H.: Dependency-based action refinement. In: Privara, I., Ružička, P. (eds.) MFCS 1997. LNCS, vol. 1295. Springer, Heidelberg (1997)CrossRefGoogle Scholar
  20. 20.
    Roscoe, A.W.: The Theory and Practice of Concurrency (1998)Google Scholar
  21. 21.
    Smith, G., Derrick, J.: Specification, refinement and verification of concurrent systems - an integration of Object-Z and CSP. Formal Methods in Systems Design 18, 249–284 (2001)zbMATHCrossRefGoogle Scholar
  22. 22.
    Stepney, S., Cooper, D., Woodcock, J.C.P.: More powerful data refinement in Z. In: Bowen, J. P., Fett, A., Hinchey, M.G. (eds.) ZUM 1998. LNCS, vol. 1493, pp. 284–307. Springer, Heidelberg (1998)CrossRefGoogle Scholar
  23. 23.
    Treharne, H., Schneider, S.: Using a process algebra to control B operations. In: Araki, K., Galloway, A., Taguchi, K. (eds.) International Conference on Integrated Formal Methods 1999 (IFM 1999), York, July 1999, pp. 437–456. Springer, Heidelberg (1999)Google Scholar
  24. 24.
    van Glabbeek, R., Goltz, U.: Equivalence notions for concurrent systems and refinement of actions. In: Kreczmar, A., Mirkowska, G. (eds.) MFCS 1989. LNCS, vol. 379, pp. 237–248. Springer, Heidelberg (1989)Google Scholar
  25. 25.
    Woodcock, J.C.P., Davies, J.: Using Z: Specification, Refinement, and Proof. Prentice Hall, Englewood Cliffs (1996)zbMATHGoogle Scholar
  26. 26.
    Woodcock, J.C.P., Morgan, C.C.: Refinement of state-based concurrent systems. In: Langmaack, H., Hoare, C.A.R., Bjorner, D. (eds.) VDM 1990. LNCS, vol. 428. Springer, Heidelberg (1990)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2005

Authors and Affiliations

  • John Derrick
    • 1
  • Heike Wehrheim
    • 2
  1. 1.Department of ComputingUniversity of SheffieldSheffieldUK
  2. 2.Institut für InformatikUniversität PaderbornPaderbornGermany

Personalised recommendations