Teaching Formal Methods in Context

  • Jim Davies
  • Andrew Simpson
  • Andrew Martin
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 3294)


The Software Engineering Programme at Oxford teaches formal methods as an integral part of its programme of professional education in software engineering. This paper explains how the methods are taught—in the context of emerging trends in software development, and in the context of existing practice—and how their use is promoted through course design and motivating examples.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Abrial, J.-R.: The B-Book: Assigning Programs to Meanings (1996)Google Scholar
  2. 2.
    Almstrum, V.L., Dean, C.N., Goelman, D., Hiburn, T.B., Smith, J.: Support for teaching formal methods. ACM SIGCSE Bulletin 33(2), 71–88 (2001)CrossRefGoogle Scholar
  3. 3.
    Ball, T., Cook, B., Levin, V., Rajamani, S.K.: SLAM and Static Driver Verifier: Technology Transfer of Formal Methods inside Microsoft. In: Boiten, E.A., Derrick, J., Smith, G.P. (eds.) IFM 2004. LNCS, vol. 2999, Springer, Heidelberg (2004)CrossRefGoogle Scholar
  4. 4.
    Bennett, S., McRobb, S., Farmer, R.: Object-Oriented Systems Analysis and Design. McGraw-Hill, New York (1999)Google Scholar
  5. 5.
    Blanchard, B.S.: System Engineering Management. Wiley, Chichester (1998)Google Scholar
  6. 6.
    Boute, R.: Can lightweight formal methods carry the weight? In: Proceedings of Teaching Formal Methods 2003, pp. 47–55 (2003)Google Scholar
  7. 7.
    Cavarra, A., Crichton, C., Davies, J.: A method for the automatic generation of test suites from object models. Information and Software Technology 46 (2004)Google Scholar
  8. 8.
    de Barros, R.S.M.: On the Formal Specification and Derivation of Relational Database Applications. PhD thesis, Department of Computing Science, The University of Glasgow (1994)Google Scholar
  9. 9.
    Dean, C.N., Hinchey, M.G. (eds.): Teaching and learning formal methods. Academic Press International Series in Formal Methods (1996)Google Scholar
  10. 10.
    DeRemer, F., Kron, H.: Programming-in-the-Large versus Programming-in-the-Small. In: International Conference on Reliable Software. SIGPLAN Notices, vol. 10 (1975)Google Scholar
  11. 11.
    Duce, D.A.: Proceedings of Teaching Formal Methods 2003. BCS (2003)Google Scholar
  12. 12.
    Edmond, D.: Refining database systems. In: Bowen, J.P., Hinchey, M.G. (eds.) ZUM 1995. LNCS, vol. 967, pp. 25–44. Springer, Heidelberg (1995)Google Scholar
  13. 13.
    Formal Methods Educational Site,
  14. 14.
    Fowler, M.: UML Distilled: A Brief Guide to the Standard Object Modeling Language, 3rd edn. September 19, Addison-Wesley, Reading (2003)Google Scholar
  15. 15.
    Habrias, H.: Investigation into the teaching of B worldwide (2003),
  16. 16.
    Hoare, C.A.R.: Communicating Sequential Processes. Prentice-Hall International, Englewood Cliffs (1985)zbMATHGoogle Scholar
  17. 17.
    IEEE Computer Society. The SoftWare Engineering Body of Knowledge (2004),
  18. 18.
    Kelemen, C., Tucker, A., Henderson, P., Bruce, K., Astrachan, O.: Has our curriculum become math-phobic (an American perspective). In: Proceedings of the 5th Annual SIGSCE/SIGCUE Conference on Innovation and Technology in Computer Science Education, July 2000, pp. 132–135 (2000)Google Scholar
  19. 19.
    Kleppe, A., Warmer, J., Bast, W.: MDA Explained: The Model Driven Architecture(TM): Practice and Promise, 1st edn. Addison-Wesley, Reading (2003)Google Scholar
  20. 20.
    Lethbridge, T.C.: What knowledge is important to a software professional? IEEE Computer 33(5), 44–50 (2000)Google Scholar
  21. 21.
    Martin, A.P., Simpson, A.C.: Generalizing the Z Schema Calculus: Database Schemas and Beyond. In: Proceedings of APSEC (Asia-Pacific Software Engineering Conference) 2003, pp. 28–37 (2003)Google Scholar
  22. 22.
    Naur, P., Randall, B.: Software Engineering: A Report on a Conference Sponsored by the NATO Science Committee (1969)Google Scholar
  23. 23.
    Page, R.L.: Software is discrete mathematics. In: Proceedings of the 8th ACM SIGPLAN International Conference on Functional Programming, pp. 79–86 (2003)Google Scholar
  24. 24.
    The Apache Maven Project. Maven (2004)Google Scholar
  25. 25.
    Simpson, A.C., Martin, A.P.: Supplementing the understanding of Z: a formal approach to database design. In: Proceedings of Teaching Formal Methods 2003, pp. 65–70 (2003)Google Scholar
  26. 26.
    Sommerville, I.: Software Engineering, 6th edn. Addison-Wesley, Reading (2001)Google Scholar
  27. 27.
    Spivey, J.M.: The Z Notation: A Reference Manual, 2nd edn. Prentice-Hall International, Englewood Cliffs (1992)Google Scholar
  28. 28.
    Stiles, D.: Informal formal methods in a computer engineering curriculum. In: Proceedings of Teaching Formal Methods 2003, pp. 40–46 (2003)Google Scholar
  29. 29.
    The Joint Task Force on Computing Curricula, IEEE Computer Society, Association for Computing Machinery. Computing Curricula 2001 (2001),
  30. 30.
    Tucker, A.B. (ed.): Computing Curricula 1991: Report of the ACM/IEEE-CS Joint Curriculum Task Force. IEEE Computer Society Press, Los Alamitos (1991)Google Scholar
  31. 31.
    Wing, J.M.: A specifier’s introduction to formal methods. IEEE Computer 23(9), 8–24 (1990)Google Scholar
  32. 32.
    Wing, J.M.: Weaving formal methods into the undergraduate computer science curriculum. In: Proceedings of the 8th International Conference on Algebraic Methodology and Software Technology, AMAST (2000)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2004

Authors and Affiliations

  • Jim Davies
    • 1
  • Andrew Simpson
    • 1
  • Andrew Martin
    • 1
  1. 1.Software Engineering ProgrammeUniversity of OxfordOxford

Personalised recommendations