Skip to main content
SpringerLink
Log in
Book cover

Formal Methods Teaching Workshop

FMTea 2019: Formal Methods Teaching pp 196–211Cite as

Teaching Introductory Formal Methods and Discrete Mathematics to Software Engineers: Reflections on a Modelling-Focussed Approach

  • Conference paper
  • First Online:

  • 522 Accesses

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 11758))

Abstract

Much has been written about the challenges of teaching discrete mathematics and formal methods. In this paper we discuss the experiences of delivering a course that serves as an introduction to both. The one-week intensive course, Software Engineering Mathematics, is delivered as part of the University of Oxford’s Software Engineering Programme to groups of professional software and security engineers studying for master’s degrees on a part-time basis. We describe how a change in the course’s emphasis—involving a shift towards a focus on modelling-based group exercises—has given rise to some pleasing results.

This is a preview of subscription content, log in via an institution.

Chapter
USD   29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD   39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD   54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Learn about institutional subscriptions

Notes

  1. 1.

    http://www.cs.ox.ac.uk/softeng/.

  2. 2.

    We would argue that, in this context, at least, the two go hand-in-hand—a ‘complementary partnership’ in the words of Kramer [21].

  3. 3.

    See [43] for a useful classification of ‘lightweight formal methods’. While Z does not appear in the discussion, we would argue that it’s ideally suited to be used as a ‘lightweight’ method.

References

  1. Almi, N.E.A.M., Rahman, N.A., Purusothaman, D., Sulaiman, S.: Software engineering education: The gap between industry’s requirements and graduates’ readiness. In: Proceedings of the IEEE Symposium on Computers and Informatics (ISCI 2011), pp. 542–547 (2011)

    Google Scholar 

  2. Barr, T.: Improving software engineering education by modeling real-world implementations. In: Proceedings of the 8th edition of the Educators’ Symposium (EduSymp 2012), pp. 36–39. ACM (2012)

    Google Scholar 

  3. Cowling, A.J.: The role of modelling in teaching formal methods for software engineering. In: Bollin, A., Margaria, T., Perseil, I. (eds.) Proceedings of the 1st Workshop on Formal Methods in Software Engineering Education and Training (FMSEE&T 2015). CEUR Workshop Proceedings, vol. 1385 (2015)

    Google Scholar 

  4. Cristiá, M.: Why, how and what should be taught about formal methods? In: Bollin, A., Margaria, T., Perseil, I. (eds.) Proceedings of the 1st Workshop on Formal Methods in Software Engineering Education and Training (FMSEE&T 2015). CEUR Workshop Proceedings, vol. 1385 (2015)

    Google Scholar 

  5. Davies, J.W.M., Gibbons, J., Welch, J., Crichton, E.: Model-driven engineering of information systems: 10 years and 1000 versions. Sci. Comput. Program. 89, 88–104 (2014)

    Article  Google Scholar 

  6. Davies, J., Simpson, A., Martin, A.: Teaching formal methods in context. In: Dean, C.N., Boute, R.T. (eds.) TFM 2004. LNCS, vol. 3294, pp. 185–202. Springer, Heidelberg (2004). https://doi.org/10.1007/978-3-540-30472-2_12

    Chapter  Google Scholar 

  7. Devlin, K.: Why universities require computer science students to take math. Commun. ACM 46(9), 37–39 (2003)

    Article  Google Scholar 

  8. Dijkstra, E.W.: The humble programmer. Commun. ACM 15(10), 859–866 (1972)

    Article  Google Scholar 

  9. Fincher, S., Utting, I.: Pedagogical patterns: their place in the genre. In: Caspersen, M.E., Joyce, D.T., Goelman, D., Utting, I. (eds.) Proceedings of the 7th Annual SIGCSE Conference on Innovation and Technology in Computer Science Education, (ITiCSE 2002), pp. 199–202. ACM, June 2002

    Google Scholar 

  10. Finkelstein, A.: Software engineering education: a place in the sun? In: Proceedings of the 16th International Conference on Software Engineering (ICSE 1994), pp. 358–359. IEEE Computer Society Press (1994)

    Google Scholar 

  11. Fraser, S., et al.: Meeting the challenge of software engineering education for working professionals in the 21st century. In: Proceedings of the 18th Annual SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA 2003), pp. 262–264 (2003)

    Google Scholar 

  12. Hayes, I.J.: Specification Case Studies, 2nd edn. Prentice-Hall, Hertfordshire (1992)

    MATH  Google Scholar 

  13. Honiden, S., Tahara, Y., Yoshioka, N., Taguchi, K., Washizaki, H.: Top SE: educating superarchitects who can apply software engineering tools to practical development in Japan. In: Proceedings of the 29th International Conference on Software Engineering (ICSE 2007), pp. 708–718. IEEE Computer Society Press (2007)

    Google Scholar 

  14. Ishikawa, F., Taguchi, K., Yoshioka, N., Honiden, S.: What top-level software engineers tackle after learning formal methods: experiences from the top SE project. In: Gibbons, J., Oliveira, J.N. (eds.) TFM 2009. LNCS, vol. 5846, pp. 57–71. Springer, Heidelberg (2009). https://doi.org/10.1007/978-3-642-04912-5_5

    Chapter  Google Scholar 

  15. Jackson, D.: Lightweight formal methods. In: Oliveira, J.N., Zave, P. (eds.) FME 2001. LNCS, vol. 2021, pp. 1–1. Springer, Heidelberg (2001). https://doi.org/10.1007/3-540-45251-6_1

    Chapter  Google Scholar 

  16. Jackson, M.: Aspects of abstraction in software development. Softw. Syst. Model. 11(4), 495–511 (2012)

    Article  Google Scholar 

  17. Jacky, J.: The Way of Z: Practical Programming With Formal Methods. Cambridge University Press, Cambridge (1997)

    Google Scholar 

  18. Jaume, M., Laurent, T.: Teaching formal methods and discrete mathematics. In: Dubois, C., Giannakopoulou, D., Méry (eds.) Proceedings of the 1st Workshop on Formal Integrated Development Environment (F-IDE 2014), pp. 30–43 (2014)

    Article  Google Scholar 

  19. Kiniry, J.R., Zimmerman, D.M.: Secret ninja formal methods. In: Cuellar, J., Maibaum, T., Sere, K. (eds.) FM 2008. LNCS, vol. 5014, pp. 214–228. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-68237-0_16

    Chapter  Google Scholar 

  20. Kramer, J.: Is abstraction the key to computing? Commun. ACM 50(4), 36–42 (2007)

    Article  Google Scholar 

  21. Kramer, J.: Abstraction and modelling—a complementary partnership. In: Czarnecki, K., Ober, I., Bruel, J.-M., Uhl, A., Völter, M. (eds.) MODELS 2008. LNCS, vol. 5301, pp. 158–158. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-87875-9_11

    Chapter  Google Scholar 

  22. Kramer, J., Hazzan, O.: The role of abstraction in software engineering. ACM SIGSOFT Softw. Eng. Not. 31(6), 38–39 (2006)

    Article  Google Scholar 

  23. Larsen, P.G., Fitzgerald, J., Riddle, S.: Learning by doing: practical courses in lightweight formal methods using VDM+. Technical Report CS-TR-992, University of Newcastle upon Tyne (2006)

    Google Scholar 

  24. Mandrioli, D.: On the heroism of really pursuing formal methods: title inspired by Dijkstra’s “On the Cruelty of Really Teaching Computing Science”. In: Proceedings of the Third FME Workshop on Formal Methods in Software Engineering (Formalise 2015), pp. 1–5. IEEE Computer Society Press (2015)

    Google Scholar 

  25. Martin, A.P., Simpson, A.C.: Generalizing the Z schema calculus: database schemas and beyond. Proc. APSEC 2003, 28–37 (2003)

    Google Scholar 

  26. Mead, N.R., Ellis, H.J.C., Moreno, A., MacNeil, P.: Can industry and academia collaborate to meet the need for software engineers? Cutter IT J. 14(6), 32–39 (2001)

    Google Scholar 

  27. Morgan, C.C., Sufrin, B.A.: Specification of the UNIX filing system. IEEE Trans. Software Eng. 10(2), 128–142 (1984)

    Article  Google Scholar 

  28. Nishihara, H., Shinozaki, K., Hayamizu, K., Aoki, T., Taguchi, K., Kumeno, F.: Model checking education for software engineers in Japan. SIGCSE Bulletin 41(2), 45–50 (2009)

    Article  Google Scholar 

  29. Reed, J.N., Sinclair, J.E.: Motivating study of formal methods in the classroom. In: Dean, C.N., Boute, R.T. (eds.) TFM 2004. LNCS, vol. 3294, pp. 32–46. Springer, Heidelberg (2004). https://doi.org/10.1007/978-3-540-30472-2_3

    Chapter  Google Scholar 

  30. Robinson, K.: Embedding formal development in software engineering. In: Dean, C.N., Boute, R.T. (eds.) TFM 2004. LNCS, vol. 3294, pp. 203–213. Springer, Heidelberg (2004). https://doi.org/10.1007/978-3-540-30472-2_13

    Chapter  Google Scholar 

  31. Roscoe, A.W.: Understanding Concurrent Systems. Springer, London (2010). https://doi.org/10.1007/978-1-84882-258-0

    Book  MATH  Google Scholar 

  32. Simpson, A.C.: Discrete Mathematics by Example. McGraw-Hill, Boston (2002)

    Google Scholar 

  33. Simpson, A.C., Martin, A.P., Cremers, C., Flechais, I., Martinovic, I., Rasmussen, K.: Experiences in developing and delivering a programme of part-time education in software and systems security. In: Proceedings of the 37th International Conference on Software Engineering (ICSE 2015), vol. 2. pp. 435–444. IEEE Computer Society Press (2015)

    Google Scholar 

  34. Simpson, A.C., Martin, A.P., Gibbons, J., Davies, J.W.M., McKeever, S.W.: On the supervision and assessment of part-time postgraduate software engineering projects. In: Proceedings of the 25th International Conference on Software Engineering (ICSE 2003), pp. 628–633. IEEE Computer Society Press (2003)

    Google Scholar 

  35. Spivey, J.M.: The Z Notation: A Reference Manual, 2nd edn. Prentice-Hall International, Englewood Cliffs (1992)

    MATH  Google Scholar 

  36. Subrahmanyam, G.V.B.: A dynamic framework for software engineering education curriculum to reduce the gap between the software organizations and software educational institutions. In: Proceedings of the 22nd IEEE International Conference on Software Engineering Education and Training (CSEET 2009), pp. 248–254 (2009)

    Google Scholar 

  37. Tarkan, S., Sazawal, V.: Chief chefs of Z to alloy: using a kitchen example to teach alloy with Z. In: Gibbons, J., Oliveira, J.N. (eds.) TFM 2009. LNCS, vol. 5846, pp. 72–91. Springer, Heidelberg (2009). https://doi.org/10.1007/978-3-642-04912-5_6

    Chapter  Google Scholar 

  38. Vaughn, R.B., Carver, J.: Position paper: The importance of experience with industry in software engineering education. In: Proceedings of the 19th IEEE International Conference on Software Engineering Education and Training (CSEET 2006), p. 19 (2006)

    Google Scholar 

  39. Warford, J.S.: An experience teaching formal methods in discrete mathematics. ACM SIGCSE 27(3), 60–64 (1995)

    Article  Google Scholar 

  40. Wing, J.M.: Computational thinking. Commun. ACM 49(3), 33–35 (2006)

    Article  Google Scholar 

  41. Woodcock, J.C.P., Davies, J.W.M.: Using Z: Specification, Refinement, and Proof. Prentice Hall, Englewood Cliffs (1996)

    MATH  Google Scholar 

  42. Woodcock, J.C.P., Larsen, P.G., Bicarregui, J., Fitzgerald, J.: Formal methods: Practice and experience. ACM Comput. Surv. 41(4), Article number 19 (2009)

    Article  Google Scholar 

  43. Zamansky, A., Spichkova, M., Rodriguez-Navas, G., Herrmann, P., Blech, J.O.: Towards classification of lightweight formal methods. In: Proceedings of the 13th International Conference on Evaluation of Novel Approaches to Software Engineering (ENASE 2013) (2018)

    Google Scholar 

Download references

Acknowledgements

The author would like to thank the anonymous reviewers for their helpful and constructive comments.

Author information

Authors and Affiliations

  1. Department of Computer Science, University of Oxford, Wolfson Building, Parks Road, Oxford, OX1 3QD, UK

    Andrew Simpson

Authors
  1. Andrew Simpson
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Andrew Simpson .

Editor information

Editors and Affiliations

  1. University of Surrey, Guildford, UK

    Brijesh Dongol

  2. Åbo Akademi University, Turku, Finland

    Luigia Petre

  3. The University of Queensland, Brisbane, QLD, Australia

    Graeme Smith

Rights and permissions

Reprints and permissions

Copyright information

© 2019 Springer Nature Switzerland AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Simpson, A. (2019). Teaching Introductory Formal Methods and Discrete Mathematics to Software Engineers: Reflections on a Modelling-Focussed Approach. In: Dongol, B., Petre, L., Smith, G. (eds) Formal Methods Teaching. FMTea 2019. Lecture Notes in Computer Science(), vol 11758. Springer, Cham. https://doi.org/10.1007/978-3-030-32441-4_13

Download citation

  • DOI: https://doi.org/10.1007/978-3-030-32441-4_13

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-030-32440-7

  • Online ISBN: 978-3-030-32441-4

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation