Skip to main content
Springer Nature Link
Log in

Teaching Formal Methods: An Experience Report

  • Conference paper
  • First Online:
Frontiers in Software Engineering Education (FISEE 2019)

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 12271))

Included in the following conference series:

Abstract

The general attitude of students towards formal specification and verification of systems is not exactly what one could call enthusiastic. Generally, software engineering courses at universities include an introduction to specification with formal notations such as Z, Alloy, UML, etc. However, it seems that the importance of formal specification to replicate expected system behavior does not sink in as it should with the students. Moreover, other products of computer science (e.g., machine learning algorithms, robot systems deployment), rather than software, benefit from formal specification as well. This paper is a general report of our observations on teaching formal methods on undergraduate and graduate levels at Politecnico di Milano.

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

Access this chapter

Log in via an institution

Subscribe and save

Springer+ Basic
$34.99 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Chapter
USD 29.95
Price excludes VAT (USA)
eBook
USD 39.99
Price excludes VAT (USA)
Softcover Book
USD 54.99
Price excludes VAT (USA)

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Similar content being viewed by others

Notes

  1. 1.

    fmeurope/teaching.

  2. 2.

    fme-teaching/courses.

  3. 3.

    Average computed by considering the last 5 years.

  4. 4.

    All the statistics and percentages reported throughout the paper are rounded and therefore are approximate values.

  5. 5.

    polimi/fm2019.

  6. 6.

    A TRIO operator formalized as which means \(\phi \) occurs d time units in the future, where holds at time t if, and only if, \(\phi \) holds at time \(t+d\).

References

  1. Abrial, J.R.: Teaching formal methods: an experience with event-B (invited speaker’s extended abstract). In: Formal Methods in Computer Science Education, p. 1 (2008)

    Google Scholar 

  2. Aceto, L., Ingólfsdóttir, A., Larsen, K.G., Srba, J.: Teaching concurrency: theory in practice. In: Proceedings of the Inernational Conference on TFM, pp. 158–175 (2009)

    Google Scholar 

  3. Ahrendt, W., Bubel, R., Hähnle, R.: Integrated and tool-supported teaching of testing, debugging, and verification. In: Proceedings of the International Conference on TFM, pp. 125–143 (2009)

    Google Scholar 

  4. Almeida, A.A., Rocha-Oliveira, A.C., Ramos, T.M.F., de Moura, F.L.C., Ayala-Rincón, M.: The computational relevance of formal logic through formal proofs. In: Dongol, B., Petre, L., Smith, G. (eds.) FMTea 2019. LNCS, vol. 11758, pp. 81–96. Springer, Cham (2019). https://doi.org/10.1007/978-3-030-32441-4_6

    Chapter  Google Scholar 

  5. Alur, R., Dill, D.L.: A theory of timed automata. Theoret. Comput. Sci. 126(2), 183–235 (1994)

    Article  MathSciNet  Google Scholar 

  6. Artho, C., Taguchi, K., Tahara, Y., Honiden, S., Tanabe, Y.: Teaching software model checking. In: Workshop on Formal Methods in Computer Science Education, pp. 171–179 (2008)

    Google Scholar 

  7. Back, R.J., Mannila, L., Peltomaki, M., Sibelius, P.: Structured derivations: a logic based approach to teaching mathematics. In: FORMED 2008: Formal Methods in Computer Science Education (2008)

    Google Scholar 

  8. Back, R.J., Von Wright, J., et al.: Structured derivations: a method for doing high-school mathematics carefully. In: Turku Centre for Computer Science (1999)

    Google Scholar 

  9. Bohórquez, J., Rocha, C.: Assisted calculational proofs and proof checking based on partial orders. In: Formal Methods in Computer Science Education, p. 37 (2008)

    Google Scholar 

  10. Börger, E.: A practice-oriented course on the principles of computation, programming, and system design and analysis. In: Dean, C.N., Boute, R.T. (eds.) TFM 2004. LNCS, vol. 3294, pp. 65–84. Springer, Heidelberg (2004). https://doi.org/10.1007/978-3-540-30472-2_5

    Chapter  Google Scholar 

  11. Boute, R.: Teaching and practicing computer science at the university level. ACM SIGCSE Bull. 41(2), 24–30 (2009)

    Article  Google Scholar 

  12. Boyatt, R., Sinclair, J.: Experiences of teaching a lightweight formal method. In: Proceedings of Formal Methods in Computer Science Education (2008)

    Google Scholar 

  13. Carro, M., Mariño, J., Herranz, Á., Moreno-Navarro, J.J.: Teaching how to derive correct concurrent programs from state-based specifications and code patterns. In: Dean, C.N., Boute, R.T. (eds.) TFM 2004. LNCS, vol. 3294, pp. 85–106. Springer, Heidelberg (2004). https://doi.org/10.1007/978-3-540-30472-2_6

    Chapter  Google Scholar 

  14. Cataño, N.: Teaching formal methods: Lessons learnt from using event-B. In: Dongol, B., Petre, L., Smith, G. (eds.) FMTea 2019. LNCS, vol. 11758, pp. 212–227. Springer, Cham (2019). https://doi.org/10.1007/978-3-030-32441-4_14

    Chapter  Google Scholar 

  15. Dadeau, F., Tissot, R.: Teaching model-based testing with Leirios test generator (2008)

    Google Scholar 

  16. 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 

  17. Duke, R., Miller, T., Strooper, P.: Integrating formal specification and software verification and validation. In: Dean, C.N., Boute, R.T. (eds.) TFM 2004. LNCS, vol. 3294, pp. 124–139. Springer, Heidelberg (2004). https://doi.org/10.1007/978-3-540-30472-2_8

    Chapter  Google Scholar 

  18. FBK-IRST, group at Carnegie Mellon University, T.M.C., the Mechanized Reasoning Group at University of Genova, at University of Trento, T.M.R.G.: NuSMV (2015). http://nusmv.fbk.eu/

  19. Fernández-Iglesias, M.J., Llamas-Nistal, M.: An undergraduate course on protocol engineering – how to teach formal methods without scaring students. In: Dean, C.N., Boute, R.T. (eds.) TFM 2004. LNCS, vol. 3294, pp. 153–165. Springer, Heidelberg (2004). https://doi.org/10.1007/978-3-540-30472-2_10

    Chapter  Google Scholar 

  20. Ferreira, J.F., Mendes, A., Backhouse, R., Barbosa, L.S.: Which mathematics for the information society? In: Gibbons, J., Oliveira, J.N. (eds.) TFM 2009. LNCS, vol. 5846, pp. 39–56. Springer, Heidelberg (2009). https://doi.org/10.1007/978-3-642-04912-5_4

    Chapter  Google Scholar 

  21. Filippidis, I.: A catalog of tools for verification and synthesis. github.com/fm-tools

  22. Furia, C.A., Mandrioli, D., Morzenti, A., Rossi, M.: Modeling time in computing: a taxonomy and a comparative survey. ACM Comput. Surv. 42(2), 6:1–6:59 (2010)

    Google Scholar 

  23. Garavel, H., Jorgensen, M.: A catalog of tools for the quantitative zoo. http://cadp.inria.fr/faq.html

  24. Gibson, J.P., Lallet, E., Raffy, J.L.: How do i know if my design is correct. In: Formal Methods in Computer Science Education, pp. 61–70 (2008)

    Google Scholar 

  25. Gibson, P., Méry, D.: Teaching formal methods: lessons to learn. In: 2nd Irish Workshop on Formal Methods, vol. 2, pp. 1–13 (1998)

    Google Scholar 

  26. Guyomard, M.: Eb: A constructive approach for the teaching of data structures. In: Formal Methods in Computer Science Education, p. 25 (2008)

    Google Scholar 

  27. Habrias, H.: Teaching specifications, hands on. In: Formal Methods in Computer Science Education, pp. 5–15 (2008)

    Google Scholar 

  28. Habrias, H., Faucou, S.: Linking paradigms, semi-formal and formal notations. In: Dean, C.N., Boute, R.T. (eds.) TFM 2004. LNCS, vol. 3294, pp. 166–184. Springer, Heidelberg (2004). https://doi.org/10.1007/978-3-540-30472-2_11

    Chapter  Google Scholar 

  29. Hähnle, R., Bubel, R.: A Hoare-style calculus with explicit state updates. In: Formal Methods in Computer Science Education, pp. 49–60 (2008)

    Google Scholar 

  30. Hallerstede, S., Leuschel, M.: How to explain mistakes. In: Gibbons, J., Oliveira, J.N. (eds.) TFM 2009. LNCS, vol. 5846, pp. 105–124. Springer, Heidelberg (2009). https://doi.org/10.1007/978-3-642-04912-5_8

    Chapter  Google Scholar 

  31. Hartel, P.H., van Es, B., Tromp, D.: Basic proof skills of computer science students. In: Hartel, P.H., Plasmeijer, R. (eds.) FPLE 1995. LNCS, vol. 1022, pp. 269–283. Springer, Heidelberg (1995). https://doi.org/10.1007/3-540-60675-0_50

    Chapter  Google Scholar 

  32. Jard, C.: Teaching distributed algorithms using spin. In: Formal Methods in Computer Science Education, p. 101 (2008)

    Google Scholar 

  33. Kofroň, J., Parízek, P., Šerý, O.: On teaching formal methods: behavior models and code analysis. In: Gibbons, J., Oliveira, J.N. (eds.) TFM 2009. LNCS, vol. 5846, pp. 144–157. Springer, Heidelberg (2009). https://doi.org/10.1007/978-3-642-04912-5_10

    Chapter  Google Scholar 

  34. Kramer, J.: Abstraction and modelling: A complementary partnership. In: Gibbons, J., Oliveira, J.N. (eds.) TFM 2009. LNCS, vol. 5846, pp. 1–1. Springer, Heidelberg (2009). https://doi.org/10.1007/978-3-642-04912-5_1

    Chapter  Google Scholar 

  35. Lau, K.: A beginner’s course on reasoning about imperative programs. In: Proceedings of CoLogNET/FME Symposium on TFM, pp. 1–16 (2004)

    Google Scholar 

  36. Lau, K.-K.: A beginner’s course on reasoning about imperative programs. In: Dean, C.N., Boute, R.T. (eds.) TFM 2004. LNCS, vol. 3294, pp. 1–16. Springer, Heidelberg (2004). https://doi.org/10.1007/978-3-540-30472-2_1

    Chapter  Google Scholar 

  37. Anderson, L.W., Krathwohl, D.R., Bloom, B.S.: A taxonomy for learning, teaching, and assessing: A revision of Bloom’s taxonomy of educational objectives (2001)

    Google Scholar 

  38. Mandrioli, D.: Advertising formal methods and organizing their teaching: Yes, but. In: Dean, C.N., Boute, R.T. (eds.) TFM 2004. LNCS, vol. 3294, pp. 214–224. Springer, Heidelberg (2004). https://doi.org/10.1007/978-3-540-30472-2_14

    Chapter  Google Scholar 

  39. Mandrioli, D., Ghezzi, C.: Theoretical Foundations of Computer Science. John Wiley & Sons, New York (1987)

    MATH  Google Scholar 

  40. Naumowicz, A.: Teaching how to write a proof. In: Formal Methods in Computer Science Education, p. 91 (2008)

    Google Scholar 

  41. Noble, J., Pearce, D.J., Groves, L.: Introducing alloy in a software modelling course. In: Formal Methods in Computer Science Education, p. 81 (2008)

    Google Scholar 

  42. Ölveczky, P.C.: Teaching formal methods based on rewriting logic and maude. In: Gibbons, J., Oliveira, J.N. (eds.) TFM 2009. LNCS, vol. 5846, pp. 20–38. Springer, Heidelberg (2009). https://doi.org/10.1007/978-3-642-04912-5_3

    Chapter  Google Scholar 

  43. Paige, R.F., Ostroff, J.S.: Specification-driven design with eiffel and agents for teaching lightweight formal methods. In: Dean, C.N., Boute, R.T. (eds.) TFM 2004. LNCS, vol. 3294, pp. 107–123. Springer, Heidelberg (2004). https://doi.org/10.1007/978-3-540-30472-2_7

    Chapter  Google Scholar 

  44. Poll, E.: Teaching program specification and verification using JML and ESC/Java2. In: Gibbons, J., Oliveira, J.N. (eds.) TFM 2009. LNCS, vol. 5846, pp. 92–104. Springer, Heidelberg (2009). https://doi.org/10.1007/978-3-642-04912-5_7

    Chapter  Google Scholar 

  45. 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 

  46. 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 

  47. Robinson, K.: Reflecting on the future: Objectives, strategies and experiences. In: Formal Methods in Computer Science Education, p. 15 (2008)

    Google Scholar 

  48. da Rosa, S.: Designing algorithms in high school mathematics. In: Dean, C.N., Boute, R.T. (eds.) TFM 2004. LNCS, vol. 3294, pp. 17–31. Springer, Heidelberg (2004). https://doi.org/10.1007/978-3-540-30472-2_2

    Chapter  Google Scholar 

  49. Schwartz, B.: The Paradox of Choice (2004)

    Google Scholar 

  50. Simonot, M., Homps, M., Bonnot, P.: Teaching abstraction in mathematics and computer science (2012)

    Google Scholar 

  51. Simonot, M., Homps, M., Bonnot, P.: Teaching abstraction in mathematics and computer science - A computer-supported approach with alloy. In: Proceedings of the 4th International Conference on Computer Supported Education, vol. 2, pp. 239–245 (2012)

    Google Scholar 

  52. Spichkova, M.: “Boring formal methods" or “Sherlock Holmes deduction methods"? In: Milazzo, P., Varró, D., Wimmer, M. (eds.) STAF 2016. LNCS, vol. 9946, pp. 242–252. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-50230-4_18

    Chapter  Google Scholar 

  53. Spichkova, M., Zamansky, A.: Teaching of formal methods for software engineering. In: ENASE, pp. 370–376 (2016)

    Google Scholar 

  54. Sznuk, T., Schubert, A.: Tool support for teaching Hoare logic. In: Giannakopoulou, D., Salaün, G. (eds.) SEFM 2014. LNCS, vol. 8702, pp. 332–346. Springer, Cham (2014). https://doi.org/10.1007/978-3-319-10431-7_27

    Chapter  Google Scholar 

  55. 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 

  56. University of Torino: GreatSPN: Graphical editor and analyzer for timed and stochastic petri nets (2001). http://www.di.unito.it/greatspn/index.html

  57. Department of Information Technology at Uppsala University, Sweden, the Department of Computer Science at Aalborg University in Denmark: Uppaal (2008). http://www.uppaal.org/

  58. Woodcock, J., Larsen, P.G., Bicarregui, J., Fitzgerald, J.: Formal methods: Practice and experience. ACM Comput. Surv. 41(4) (2009)

    Google Scholar 

  59. Zot: A bounded satisfiability checker (2012). github.com/fm-polimi/zot

Download references

Acknowledgements

The credit of the statistics reported on our course goes to its official responsibles, previously prof. emeritus Dino Mandrioli and currently prof. Pierluigi San Pietro.

Author information

Authors and Affiliations

  1. Computing and Software, McMaster University, Hamilton, Canada

    Mehrnoosh Askarpour

  2. DEIB, Poltecnico di Milano, Milan, Italy

    Marcello M. Bersani

Authors
  1. Mehrnoosh Askarpour
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Marcello M. Bersani
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Mehrnoosh Askarpour .

Editor information

Editors and Affiliations

  1. University of Toulouse, Blagnac, France

    Jean-Michel Bruel

  2. University of Luxembourg, Esch-sur-Alzette, Luxembourg

    Alfredo Capozucca

  3. Innopolis University, Innopolis, Russia

    Manuel Mazzara

  4. Schaffhausen Institute of Technology, Schaffhausen, Switzerland

    Bertrand Meyer

  5. Innopolis University, Innopolis, Russia

    Alexandr Naumchev

  6. Innopolis University, Innopolis, Russia

    Andrey Sadovykh

Rights and permissions

Reprints and permissions

Copyright information

© 2020 Springer Nature Switzerland AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Askarpour, M., Bersani, M.M. (2020). Teaching Formal Methods: An Experience Report. In: Bruel, JM., Capozucca, A., Mazzara, M., Meyer, B., Naumchev, A., Sadovykh, A. (eds) Frontiers in Software Engineering Education. FISEE 2019. Lecture Notes in Computer Science(), vol 12271. Springer, Cham. https://doi.org/10.1007/978-3-030-57663-9_1

Download citation

  • DOI: https://doi.org/10.1007/978-3-030-57663-9_1

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-030-57662-2

  • Online ISBN: 978-3-030-57663-9

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation