Understanding, Explaining, and Deriving Refinement

  • Eerke Boiten
  • John DerrickEmail author
Part of the Emergence, Complexity and Computation book series (ECC, volume 35)


Much of what drove us in over twenty years of research in refinement, starting with Z in particular, was the desire to understand where refinement rules came from. The relational model of refinement provided a solid starting point which allowed the derivation of Z refinement rules. Not only did this explain and verify the existing rules—more importantly, it also allowed alternative derivations for different and generalised notions of refinement. In this chapter, we briefly describe the context of our early efforts in this area and Susan Stepney’s role in this, before moving on to the motivation and exploration of a recently developed primitive model of refinement: concrete state machines with anonymous transitions.


  1. 1.
    Abadi, M., Lamport, L.: The existence of refinement mappings. Theor. Comput. Sci. 2(82), 253–284 (1991)MathSciNetCrossRefGoogle Scholar
  2. 2.
    Abrial, J.R.: Modelling in Event-B. CUP, Cambridge (2010)CrossRefGoogle Scholar
  3. 3.
    Ainsworth, M., Cruickshank, A.H., Wallis, P.J.L., Groves, L.J.: Viewpoint specification and Z. Inf. Softw. Technol. 36(1), 43–51 (1994)CrossRefGoogle Scholar
  4. 4.
    Back, R.J.R., Kurki-Suonio, R.: Distributed cooperation with action systems. ACM Trans. Program. Lang. Syst. 10(4), 513–554 (1988)CrossRefGoogle Scholar
  5. 5.
    Barden, R., Stepney, S., Cooper, D.: Z in Practice. BCS Practitioner Series. Prentice Hall, New York (1994)zbMATHGoogle Scholar
  6. 6.
    Boiten, E.: Z unification tools in generic formaliser. Technical report 10-97, Computing Laboratory, University of Kent at Canterbury (1997)Google Scholar
  7. 7.
    Boiten, E., Derrick, J.: IO-refinement in Z. In: Evans, A., Duke, D., Clark T. (eds.) 3rd BCS-FACS Northern Formal Methods Workshop. Springer (1998).
  8. 8.
    Boiten, E., Derrick, J., Bowman, H., Steen, M.: Consistency and refinement for partial specification in Z. In: Gaudel and Woodcock [20], pp. 287–306Google Scholar
  9. 9.
    Boiten, E.A.: Perspicuity and granularity in refinement. In: Proceedings 15th International Refinement Workshop, EPTCS, vol. 55, pp. 155–165 (2011)Google Scholar
  10. 10.
    Boiten, E.A.: Introducing extra operations in refinement. Form. Asp. Comput. 26(2), 305–317 (2014)MathSciNetCrossRefGoogle Scholar
  11. 11.
    Boiten, E.A., Derrick, J.: From ODP viewpoint consistency to integrated formal methods. Comput. Stand. Interfaces 35(3), 269–276 (2013). Scholar
  12. 12.
    Boiten, E.A., Derrick, J., Schellhorn, G.: Relational concurrent refinement II: internal operations and outputs. Form. Asp. Comput. 21(1–2), 65–102 (2009).
  13. 13.
    Derrick, J., Boiten, E.: Refinement – Semantics, Languages and Applications. Springer, Berlin (2018)CrossRefGoogle Scholar
  14. 14.
    Derrick, J., Boiten, E., Bowman, H., Steen, M.: Viewpoints and consistency: translating LOTOS to Object-Z. Comput. Stand. Interfaces 21, 251–272 (1999)CrossRefGoogle Scholar
  15. 15.
    Derrick, J., Boiten, E.A.: Relational concurrent refinement. Form. Asp. Comput. 15(1), 182–214 (2003)CrossRefGoogle Scholar
  16. 16.
    Derrick, J., Boiten, E.A.: Refinement in Z and Object-Z, 2nd edn. Springer, London (2014). Scholar
  17. 17.
    Derrick, J., Boiten, E.A., Bowman, H., Steen, M.W.A.: Specifying and refining internal operations in Z. Form. Asp. Comput. 10, 125–159 (1998)CrossRefGoogle Scholar
  18. 18.
    Derrick, J., Bowman, H., Boiten, E., Steen, M.: Comparing LOTOS and Z refinement relations. In: FORTE/PSTV’96, pp. 501–516. Chapman & Hall, Kaiserslautern (1996)Google Scholar
  19. 19.
    Flynn, M., Hoverd, T., Brazier, D.: Formaliser – an interactive support tool for Z. In: Nicholls J.E. (ed.) Z User Workshop, pp. 128–141. Springer, London (1990)Google Scholar
  20. 20.
    Gaudel, M.C., Woodcock, J.C.P. (eds.): FME’96: Industrial Benefit of Formal Methods, Third International Symposium of Formal Methods Europe. Lecture Notes in Computer Science, vol. 1051. Springer (1996)Google Scholar
  21. 21.
    van Glabbeek, R.J.: The linear time - branching time spectrum I. The semantics of concrete sequential processes. In: Bergstra, J., Ponse, A., Smolka S. (eds.) Handbook of Process Algebra, pp. 3–99. North-Holland (2001)Google Scholar
  22. 22.
    He, J., Hoare, C.A.R., Sanders, J.W.: Data refinement refined. In: Robinet, B., Wilhelm R. (eds.) Proceedings of ESOP 86, Lecture Notes in Computer Science, vol. 213, pp. 187–196. Springer, Berlin (1986)Google Scholar
  23. 23.
    Hoare, C.A.R., He, J.: Unifying Theories of Programming. Prentice Hall, Englewood Cliffs (1998)zbMATHGoogle Scholar
  24. 24.
    Leduc, G.: On the role of implementation relations in the design of distributed systems using LOTOS. Ph.D. thesis, University of Liège, Liège, Belgium (1991)Google Scholar
  25. 25.
    Schellhorn, G.: ASM refinement and generalizations of forward simulation in data refinement: a comparison. Theor. Comput. Sci. 336(2–3), 403–435 (2005). Scholar
  26. 26.
    Smith, G., Derrick, J.: Specification, refinement and verification of concurrent systems - an integration of Object-Z and CSP. Form. Methods Syst. Des. 18, 249–284 (2001)CrossRefGoogle Scholar
  27. 27.
    Spivey, J.M.: The Z Notation: A Reference Manual. International Series in Computer Science, 2nd edn. Prentice Hall, Upper Saddle River (1992)zbMATHGoogle Scholar
  28. 28.
    Stepney, S., Cooper, D., Woodcock, J.: More powerful data refinement in Z. In: Bowen, J.P., Fett, A., Hinchey M.G. (eds.) ZUM’98: The Z Formal Specification Notation. Lecture Notes in Computer Science, vol. 1493, pp. 284–307. Springer, Berlin (1998)Google Scholar
  29. 29.
    Woodcock, J., Stepney, S., Cooper, D., Clark, J., Jacob, J.: The certification of the mondex electronic purse to ITSEC level E6. Form. Asp. Comput. 20(1), 5–19 (2008). Scholar
  30. 30.
    Woodcock, J.C.P., Davies, J.: Using Z: Specification, Refinement, and Proof. Prentice Hall, New York (1996)zbMATHGoogle Scholar

Copyright information

© Springer Nature Switzerland AG 2020

Authors and Affiliations

  1. 1.De Montfort UniversityLeicesterUK
  2. 2.University of SheffieldSheffieldUK

Personalised recommendations