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.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Similar content being viewed by others
Notes
- 1.
- 2.
- 3.
Average computed by considering the last 5 years.
- 4.
All the statistics and percentages reported throughout the paper are rounded and therefore are approximate values.
- 5.
- 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
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)
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)
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)
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
Alur, R., Dill, D.L.: A theory of timed automata. Theoret. Comput. Sci. 126(2), 183–235 (1994)
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)
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)
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)
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)
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
Boute, R.: Teaching and practicing computer science at the university level. ACM SIGCSE Bull. 41(2), 24–30 (2009)
Boyatt, R., Sinclair, J.: Experiences of teaching a lightweight formal method. In: Proceedings of Formal Methods in Computer Science Education (2008)
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
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
Dadeau, F., Tissot, R.: Teaching model-based testing with Leirios test generator (2008)
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
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
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/
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
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
Filippidis, I.: A catalog of tools for verification and synthesis. github.com/fm-tools
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)
Garavel, H., Jorgensen, M.: A catalog of tools for the quantitative zoo. http://cadp.inria.fr/faq.html
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)
Gibson, P., Méry, D.: Teaching formal methods: lessons to learn. In: 2nd Irish Workshop on Formal Methods, vol. 2, pp. 1–13 (1998)
Guyomard, M.: Eb: A constructive approach for the teaching of data structures. In: Formal Methods in Computer Science Education, p. 25 (2008)
Habrias, H.: Teaching specifications, hands on. In: Formal Methods in Computer Science Education, pp. 5–15 (2008)
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
Hähnle, R., Bubel, R.: A Hoare-style calculus with explicit state updates. In: Formal Methods in Computer Science Education, pp. 49–60 (2008)
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
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
Jard, C.: Teaching distributed algorithms using spin. In: Formal Methods in Computer Science Education, p. 101 (2008)
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
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
Lau, K.: A beginner’s course on reasoning about imperative programs. In: Proceedings of CoLogNET/FME Symposium on TFM, pp. 1–16 (2004)
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
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)
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
Mandrioli, D., Ghezzi, C.: Theoretical Foundations of Computer Science. John Wiley & Sons, New York (1987)
Naumowicz, A.: Teaching how to write a proof. In: Formal Methods in Computer Science Education, p. 91 (2008)
Noble, J., Pearce, D.J., Groves, L.: Introducing alloy in a software modelling course. In: Formal Methods in Computer Science Education, p. 81 (2008)
Ö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
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
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
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
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
Robinson, K.: Reflecting on the future: Objectives, strategies and experiences. In: Formal Methods in Computer Science Education, p. 15 (2008)
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
Schwartz, B.: The Paradox of Choice (2004)
Simonot, M., Homps, M., Bonnot, P.: Teaching abstraction in mathematics and computer science (2012)
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)
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
Spichkova, M., Zamansky, A.: Teaching of formal methods for software engineering. In: ENASE, pp. 370–376 (2016)
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
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
University of Torino: GreatSPN: Graphical editor and analyzer for timed and stochastic petri nets (2001). http://www.di.unito.it/greatspn/index.html
Department of Information Technology at Uppsala University, Sweden, the Department of Computer Science at Aalborg University in Denmark: Uppaal (2008). http://www.uppaal.org/
Woodcock, J., Larsen, P.G., Bicarregui, J., Fitzgerald, J.: Formal methods: Practice and experience. ACM Comput. Surv. 41(4) (2009)
Zot: A bounded satisfiability checker (2012). github.com/fm-polimi/zot
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
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2020 Springer Nature Switzerland AG
About this paper
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)