Taking Our Own Medicine: Applying the Refinement Calculus to State-Rich Refinement Model Checking

  • Leo Freitas
  • Ana Cavalcanti
  • Jim Woodcock
Part of the Lecture Notes in Computer Science book series (LNCS, volume 4260)


In this paper, we advocate the use of formal specification and verification in software development for high-integrity and safety-critical systems, where mechanical proof plays a central role. In particular, we emphasise the crucial importance of applying verification in the development of formal verification tools themselves. We believe this approach is very useful to increase the levels of confidence and integrity of tools that are built to find bugs based on formally specified models. This follows the trend set out by a UK grand challenge in computer research for verified software repository.

In this direction, we present our experiences on a case study on the development process of a refinement model checking tool for Circus, a concurrent refinement language that combines Z, CSP, guarded commands, and the refinement calculus, with the Unifying Theories of Programming of Hoare and He as the theoretical background.


 model checking theorem proving formal verification 


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Back, R.-J., von Wright, J.: Refinement Calculus: A Systematic Introduction. Graduate Text in Computer Science. Springer, Heidelberg (1998)Google Scholar
  2. 2.
    Bicarregui, J.C., Hoare, C.A.R., Woodcock, J.C.P.: The Verified Software Repository: a Step Towards the Verifying Compiler. UK Grand Challenge for Computer Research, Steering Committee (2004)Google Scholar
  3. 3.
    Bolton, C., Lowe, G.: A Hierachy of Failures-Based Models: Theory and Application. Theoretical Computer Science Journal (June 2004)Google Scholar
  4. 4.
    Burdy, L., Cheon, Y., Cok, D.R., Ernst, M.D., Kiniry, J.R., Leavens, G.T., Leino, K.R.M., Poll, E.: An Overview of JML Tools and Applications. In: Eighth International Workshop on Formal Methods for Industrial Critical Systems (FMICS). Electronic Notes in Theoretical Computer Science, pp. 73–89. University of Nijmegen. Elsevier (March 2003)Google Scholar
  5. 5.
    Cavalcanti, A.L.C., Woodcock, J.C.P.: ZRC—A Refinement Calculus for Z. Formal Aspects of Computing Journal 10(3), 267–289 (1999)CrossRefGoogle Scholar
  6. 6.
    Cavalcanti, A.L.C., Sampaio, A.C.A., Woodcock, J.C.P.: A Refinement Strategy for Circus. Formal Aspects of Computing Journal 15(2-3), 146–181 (2003)zbMATHCrossRefGoogle Scholar
  7. 7.
    Escher Technologies. Perferct Developer User’s Guide, v.3.0 (2004), Available on-line at:
  8. 8.
    Goldsmith, M.: FDR2 Manual (v2.82). Formal Systems (Europe) Ltd. (June 2005)Google Scholar
  9. 9.
    Hoare, C.A.R.: Communicating Sequential Process. International Series in Computer Science. Prentice-Hall, Englewood Cliffs (1985)Google Scholar
  10. 10.
    Hoare, C.A.R., Jifeng, H.: Unifying Theories of Programming. International Series in Computer Science. Prentice-Hall, Englewood Cliffs (1998)Google Scholar
  11. 11.
    Freitas, L.: Model Checking Circus. PhD thesis, Univeristy of York (October 2005)Google Scholar
  12. 12.
    Jones, C.B., Jones, K.D., Lindsay, P.A., Moore, R.: Mural: a Formal Development Support System. Springer, Heidelberg (1991)zbMATHGoogle Scholar
  13. 13.
    Malik, P., Utting, M.: CZT: A Framework for Z Tools. In: Treharne, H., King, S., Henson, M., Schneider, S. (eds.) ZB 2005: Formal Specification and Development in Z and B: 4th International Conference of B and Z Users, Guildford, UK, pp. 13–15. Springer, Heidelberg (2005)Google Scholar
  14. 14.
    Martin, J.M.R., Huddart, Y.: Parallel Algorithms for Deadlock and Livelock Analysis of Concurrent Systems. Communicating Process Architectures (2000)Google Scholar
  15. 15.
    Morgan, C.: Programming from Specifications. Prentice-Hall, Englewood Cliffs (1994)zbMATHGoogle Scholar
  16. 16.
    Oliveira, M.V.M., Xavier, M.A., Cavalcanti, A.L.C.: Refine and Gabriel: Support for Refinement and Tactics. In: Cuellar, J.R., Liu, Z. (eds.) 2nd IEEE International Conference on Software Engineering and Formal Methods, pp. 310–319. IEEE Computer Society Press, Los Alamitos (2004)Google Scholar
  17. 17.
    Oliveira, M.: Formal Derivation of State-Rich Reactive Programs using Circus. PhD thesis, University of York (2006)Google Scholar
  18. 18.
    Ryan, P., Schneider, S., Roscoe, B., Goldsmith, M., Lowe, G.: Modelling and Analysis of Security Protocols. Addison Wesley, Reading (2001)Google Scholar
  19. 19.
    Roscoe, A.W.: Model Checking CSP. In: A Classical Mind: Essays in Honour of C. A. R. Hoare, International Series in Computer Science, ch. 21, pp. 353–378. Prentice-Hall, Englewood Cliffs (1994)Google Scholar
  20. 20.
    Roscoe, A.W.: The Theory and Practice of Concurrency. Prentice-Hall, Englewood Cliffs (1997)Google Scholar
  21. 21.
    Saaltink, M.: Z/Eves 2.0 User’s Guide. ORA Canada (1999)Google Scholar
  22. 22.
    Woodcock, J., Davies, J.: Using Z: Specification, Refinement, and Proof. International Series in Computer Science. Prentice-Hall, Englewood Cliffs (1996)zbMATHGoogle Scholar
  23. 23.
    Woodcock, J.C.P., Cavalcanti, A.L.C.: The Semantics of Circus. In: Bert, D., Bowen, J.P., Henson, M.C., Robinson, K. (eds.) B 2002 and ZB 2002. LNCS, vol. 2272, pp. 184–203. Springer, Heidelberg (2002)CrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2006

Authors and Affiliations

  • Leo Freitas
    • 1
  • Ana Cavalcanti
    • 1
  • Jim Woodcock
    • 1
  1. 1.Department of Computer ScienceUniversity of YorkUK

Personalised recommendations