Advertisement

The Z Notation: Whence the Cause and Whither the Course?

  • Jonathan P. BowenEmail author
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 9506)

Abstract

The Z notation for the formal specification of computer-based systems has been in existence since the early 1980s. Since then, an international Z community has emerged, academic and industrial courses have been developed, an ISO standard has been adopted, and Z has been used on a number of significant software development projects, especially where safety and security have been important. This chapter traces the history of the Z notation and presents issues in teaching Z, with examples. A specific example of an industrial course is presented. Although subsequent notations have been developed, with better tool support, Z is still an excellent choice for general purpose specification and is especially useful in directing software testing to ensure good coverage.

Keywords

State Component State Schema Operation Schema Predicate Part Program Research Group 
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.

Notes

Acknowledgements

Material for the Z course was kindly made available by Altran UK (formerly Altran Praxis), a software engineering company based in the United Kingdom with extensive experience of the industrial use of formal methods in general and the Z notation in particular. The extracts of the Z course included in Appendix B are copyright Altran UK and are reproduced here with permission. I am very grateful to Jonathan Hammond of Altran UK for his help and advice in this matter. Thomas Lancaster of Birmingham City University invited me to contribution to a Z course for final year undergraduates. The questions and answers on an example air traffic control system as presented here were originally developed as a result.

The Z notation in the main part of this chapter has been formatted using the Open image in new window style file zed-csp.sty and type-checked using the Open image in new window type-checker [40]. It is believed that the drawing in Fig. 2 is by Ib Holm Sørensen (who died in 2012), from an idea by Bernard Sufrin.

Many thanks to my good colleague, Prof. Zhiming Liu, for inviting me to present at the Summer School on Engineering Trustworthy Software Systems (SETSS) at Southwest University in Chongqing, China, during September 2014, and thank you to all at Southwest University for a very pleasant and well organized visit, together with financial support. I am grateful too for financial support from Museophile Limited.

Finally, very many thanks to the Israel Institute for Advanced Studies at the Hebrew University of Jerusalem, who funded me as a Visiting Scholar for a Computability Research Group during the completion of this chapter and provided a very supportive academic environment in which to do it.

Supplementary material

References

  1. 1.
    Abrial, J.R.: Data semantics. In: Klimbie, J.W., Koffeman, K.L. (eds.) IFIP TC2 Working Conference on Data Base Management, pp. 1–59. Elsevier Science Publishers, North-Holland, April 1974Google Scholar
  2. 2.
    Bagheri, S.M., Smith, G., Hanan, J.: Using Z in the development and maintenance of computational models of real-world systems. In: Canal, C., Idani, A. (eds.) SEFM 2014 Workshops. LNCS, vol. 8938, pp. 36–53. Springer, Heidelberg (2015)Google Scholar
  3. 3.
    Boulanger, J.L. (ed.): Formal Methods: Industrial Use from Model to the Code. ISTE, Wiley, London (2012)Google Scholar
  4. 4.
    Bowen, J.P.: Formal specification and documentation of microprocessor instruction sets. Microprocessing and Microprogramming 21(1–5), 223–230 (1987)CrossRefGoogle Scholar
  5. 5.
    Bowen, J.P. (ed.): Proceeding of Z Users Meeting, 1 Wellington Square, Oxford. Oxford University Computing Laboratory, Oxford, December 1987Google Scholar
  6. 6.
    Bowen, J.P.: Formal specification in Z as a design and documentation tool. In: Proc. 2nd IEE/BCS Conference on Software Engineering, pp. 164–168, No. 290 in Conference Publication. IEE/BCS, July 1988Google Scholar
  7. 7.
    Bowen, J.P.: POS: formal specification of a UNIX tool. IEE/BCS Softw. Eng. J. 4(1), 67–72 (1989)MathSciNetCrossRefGoogle Scholar
  8. 8.
    Bowen, J.P.: X: why Z? Comput. Graph. Forum 11(4), 221–234 (1992)MathSciNetCrossRefGoogle Scholar
  9. 9.
    Bowen, J.P.: Glossary of Z notation. Inf. Softw. Technol. 37(5–6), 333–334 (1995)CrossRefGoogle Scholar
  10. 10.
    Bowen, J.P.: Formal Specification and Documentation Using Z: A Case Study Approach. International Thomson Computer Press, London (1996)Google Scholar
  11. 11.
    Bowen, J.P.: Experience teaching Z with tool and web support. ACM SIGSOFT Softw. Eng. Notes 26(2), 69–75 (2001)CrossRefGoogle Scholar
  12. 12.
    Bowen, J.P.: Z: A formal specification notation. In: Frappier, M., Habrias, H. (eds.) Software Specification Methods: An Overview Using a Case Study, chap. 1, pp. 3–20. ISTE (2006)Google Scholar
  13. 13.
    Bowen, J.P.: Alan Turing. In: Robinson, A. (ed.) The Scientists: An Epic of Discovery, pp. 270–275. Thames and Hudson, London (2012)Google Scholar
  14. 14.
    Bowen, J.P., Fett, A., Hinchey, M.G. (eds.): ZUM’98: The Z Formal Specification Notation. LNCS, vol. 1493, pp. 24–26. Springer, Heidelberg (1998)Google Scholar
  15. 15.
    Bowen, J.P., Gimson, R.B., Topp-Jørgensen, S.: Specifying system implementations in Z. Technical Monograph PRG-63, Oxford University Computing Laboratory, Oxford, February 1988Google Scholar
  16. 16.
    Bowen, J.P., Gordon, M.J.C.: A shallow embedding of Z in HOL. Inf. Softw. Technol. 37(5–6), 269–276 (1995)CrossRefGoogle Scholar
  17. 17.
    Bowen, J.P., Hinchey, M.G.: Ten commandments ten years on: lessons for ASM, B, Z and VSR-net. In: Abrial, J.-R., Glässer, U. (eds.) Rigorous Methods for Software Construction and Analysis. LNCS, vol. 5115, pp. 219–233. Springer, Heidelberg (2009)CrossRefGoogle Scholar
  18. 18.
    Bowen, J.P., Hinchey, M.G.: Formal methods. In: Gonzalez, T.F., Diaz-Herrera, J., Tucker, A.B. (eds.) Computing Handbook, vol. 1, 3rd edn., chap. 71, pp. 1–25. CRC Press (2014)Google Scholar
  19. 19.
    Bowen, J.P., Hinchey, M.G., Janicke, H., Ward, M., Zedan, H.: Formality, agility, security, and evolution in software development. IEEE Comput. 47(10), 86–89 (2014)CrossRefGoogle Scholar
  20. 20.
    Breuer, P.T., Bowen, J.P.: Towards correct executable semantics for Z. In: Bowen, J.P., Hall, J.A. (eds.) Z User Workshop, Cambridge 1994. Workshops in Computing, pp. 185–209. Springer, London (1994)CrossRefGoogle Scholar
  21. 21.
    Ciancarini, P., Cimato, S., Mascolo, C.: Engineering formal requirements: an analysis and testing method for Z documents. Ann. Softw. Eng. 3, 189–219 (1997)CrossRefGoogle Scholar
  22. 22.
    Copeland, J., Bowen, J.P., Sprevak, M., Wilson, R.J., et al.: The Turing Guide. Oxford University Press (to appear 2016)Google Scholar
  23. 23.
    Cristia, M., Hollmann, D., Albertengo, P., Frydman, C., Monetti, P.R.: A language for test case refinement in the test template framework. In: Qin, S., Qiu, Z. (eds.) ICFEM 2011. LNCS, vol. 6991, pp. 601–616. Springer, Heidelberg (2011)CrossRefGoogle Scholar
  24. 24.
    Gimson, R., Bowen, J.P., Gleeson, T.: Distributed computing software project. In: 2nd Workshop on Making Distributed Systems Work, pp. 1–3. ACM, September 1986Google Scholar
  25. 25.
    Gnesi, S., Margaria, T.: Formal Methods for Industrial Critical Systems: A Survey of Applications. IEEE Computer Society Press, Wiley, Chichester (2012)CrossRefGoogle Scholar
  26. 26.
    Hall, J.A.: Z word tools. SourceForge (2008). http://sourceforge.net/projects/zwordtools/. Accessed 28 September 2015
  27. 27.
    Henson, M.C., Reeves, S., Bowen, J.P.: Z logic and its consequences. CAI. Comput. Inform. 22(4), 381–415 (2003)MathSciNetzbMATHGoogle Scholar
  28. 28.
    Hinchey, M.G., Jackson, M., Cousot, P., Cook, B., Bowen, J.P., Margaria, T.: Software engineering and formal methods. Commun. ACM 51(9), 54–59 (2008)CrossRefGoogle Scholar
  29. 29.
    Hoare, C.A.R.: An axiomatic basis for computer programming. Commun. ACM 12(10), 576–580 (1969)CrossRefzbMATHGoogle Scholar
  30. 30.
    Hoare, C.A.R.: Communicating Sequential Processes. Series in Computer Science. Prentice Hall International, London (1985)zbMATHGoogle Scholar
  31. 31.
    Hörcher, H.M.: Improving software tests using Z specifications. In: Bowen, J.P., Hinchey, M.G. (eds.) ZUM’95: The Z Formal Specification Notation. LNCS, vol. 967, pp. 152–166. Springer, Heidelberg (1995)CrossRefGoogle Scholar
  32. 32.
    ISO: Information technology - Z formal specification notation - syntax, type system and semantics. International Standard 13568, ISO/IEC, July 2002Google Scholar
  33. 33.
    Jones, R.B.: ICL ProofPower. BCS-FACS FACTS Series III 1(1), 10–13 (1992)Google Scholar
  34. 34.
    Morris, F.L., Jones, C.B.: An early program proof by Alan Turing. IEEE Ann. Hist. Comput. 6(2), 139–143 (1984)MathSciNetCrossRefzbMATHGoogle Scholar
  35. 35.
    Nicholls, J.E.: A survey of Z courses in the UK. In: Nicholls, J.E. (ed.) Z User Workshop, Oxford 1990. Workshops in Computing, pp. 343–350. Springer, Heidelberg (1991)CrossRefGoogle Scholar
  36. 36.
    Nicholls, J.E. (ed.): Z User Workshop, York 1991. Workshops in Computing. Springer, London (1992)Google Scholar
  37. 37.
    Saaltink, M.: The Z/EVES system. In: Till, D., Bowen, J.P., Hinchey, M.G. (eds.) ZUM 1997. LNCS, vol. 1212. Springer, Heidelberg (1997)Google Scholar
  38. 38.
    Smith, G.: The Object-Z Specification Language, Advances in Formal Methods, vol. 1. Springer, Heidelberg (2012)Google Scholar
  39. 39.
    Spivey, J.M.: The Z Notation: A reference manual. Series in Computer Science, Prentice Hall International (1989/1992/2001). http://spivey.oriel.ox.ac.uk/mike/zrm/
  40. 40.
    Spivey, J.M.: The fuzz type-checker for Z. Technical report, University of Oxford, UK (2008). http://spivey.oriel.ox.ac.uk/mike/fuzz/
  41. 41.
    Stocks, P., Carrington, D.: A framework for specification-based testing. IEEE Trans. Softw. Eng. 22(11), 777–793 (1996)CrossRefGoogle Scholar
  42. 42.
    Turing, A.M.: On computable numbers with an application to the Entscheidungsproblem. Proc. London Math. Soc. 2(42), 230–265 (1936/7)Google Scholar
  43. 43.
    Turing, A.M.: Checking a large routine. In: Campbell-Kelly, M. (ed.) The early British computer conferences, pp. 70–72. MIT Press, Cambridge (1949/1989)Google Scholar
  44. 44.
    Vilkomir, S.A., Bowen, J.P.: Formalization of software testing criteria using the Z notation. In: Proceeding 25th Annual International Computer Software and Applications Conference (COMPSAC 2001), Chicago, pp. 351–356. IEEE Computer Society Press, 8–12 October 2001Google Scholar
  45. 45.
    Vilkomir, S.A., Bowen, J.P.: From MC/DC to RC/DC: formalization and analysis of control-flow testing criteria. Formal Aspects Comput. 18(1), 42–62 (2006)CrossRefzbMATHGoogle Scholar

Copyright information

© Springer International Publishing Switzerland 2016

Authors and Affiliations

  1. 1.Department of Informatics, School of EngineeringLondon South Bank UniversityLondonUK
  2. 2.Israel Institute for Advanced StudiesThe Hebrew University of JerusalemJerusalemIsrael
  3. 3.Museophile LimitedOxfordUK

Personalised recommendations