Skip to main content
SpringerLink
Log in

Teaching Formal Methods: Lessons Learnt from Using Event-B

  • Conference paper
  • First Online:
Formal Methods Teaching (FMTea 2019)

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

Included in the following conference series:

Abstract

This paper summarises our experience in teaching Formal Methods to Computer Science and Software Engineers students from various universities around the world, including the University of Madeira in Portugal, the Pontificia Universidad Javeriana and the University of The Andes in Colombia, Carnegie Mellon University (CMU) in the USA, and Innopolis University (INNO) in Russia. We report challenges we have faced during the past 10 to 15 years when teaching formal methods using the Event B formalism, and describe how we have evolved the structure of our courses to respond to those challenges. We strive to help students to build skills on Formal Methods that they can employ later on in their future IT jobs in software Industry. Our goal is to promote the wide use of Formal Methods by software Industry. We consider that this goal cannot be achieved without first universities transferring to Industry students with a strong background in Formal Methods and related formal tools. Formal Methods are key to software development because they are based on Discrete Mathematics which can be used to properly reason about properties that the software one develops should have. We have conducted two surveys among our students, the first one at CMU and the second one at INNO, that we use here to document and justify our decisions in terms of the course structure. The first survey is about the use of Event B as main mathematical formalism, and the second one is about the organisation of teams of students within the classroom to work on software projects that use Event B as main mathematical formalism. Our hope is that our work can be reused by other Faculty to make their own decisions on course structure and content in the teaching of their Formal Methods courses.

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

Access this chapter

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

Institutional subscriptions

References

  1. Abrial, J.-R.: Modeling in Event-B: System and Software Design. Cambridge University Press, New York (2010)

    Book  Google Scholar 

  2. Abrial, J.-R., Butler, M., Hallerstede, S., Hoang, T.S., Mehta, F., Voisin, L.: Rodin: an open toolset for modelling and reasoning in Event-B. Softw. Tools Technol. Transf. 12(6), 447–466 (2010)

    Article  Google Scholar 

  3. Abrial, J.-R., Hallerstede, S.: Refinement, decomposition, and instantiation of discrete models: application to Event-B. Fundamentae Informatica 77(1–2), 1–28 (2007)

    MathSciNet  MATH  Google Scholar 

  4. Arney, D.E., Jones, P., Lee, I., Ray, A.: Generic infusion pump hazard analysis and safety requirements version 1.0. Technical report, University of Pennsylvania (2009)

    Google Scholar 

  5. Cataño, N.: An empirical study on teaching formal methods to millennials. In: First International Workshop on Software Engineering Curricula for Millennials (SECM/ICSE), Buenos Aires, Argentina. ACM and IEEE Digital Libraries (2017)

    Google Scholar 

  6. Cataño, N., Barraza, F., García, D., Ortega, P., Rueda, C.: A case study in JML-assisted software development. In: Machado, P., Andrade, A., Duran, A. (eds.) Brazilian Symposium on Formal Methods (SBMF). Electronic Notes in Theoretical Computer Science, vol. 240, pp. 5–21, July 2009

    Article  Google Scholar 

  7. Catano, N., Rueda, C.: Matelas: a predicate calculus common formal definition for social networking. In: Frappier, M., Glässer, U., Khurshid, S., Laleau, R., Reeves, S. (eds.) ABZ 2010. LNCS, vol. 5977, pp. 259–272. Springer, Heidelberg (2010). https://doi.org/10.1007/978-3-642-11811-1_20

    Chapter  Google Scholar 

  8. Gibson, J.P., Méry, D.: Teaching formal methods: lessons to learn. In: 2nd Irish Workshop on Formal Methods, Cork, Ireland, 2–3 July 1998 (1998)

    Google Scholar 

  9. Google Inc.: The Android Platform (2017). http://developer.android.com/design/index.html

  10. Jaume, M., Laurent, T.: Teaching formal methods and discrete mathematics. In: Proceedings 1st Workshop on Formal Integrated Development Environment, F-IDE 2014, Grenoble, France, 6 April 2014, pp. 30–43 (2014)

    Article  Google Scholar 

  11. Leavens, G.T., Baker, A.L., Ruby, C.: Preliminary design of JML: a behavioral interface specification language for Java. ACM SIGSOFT 31(3), 1–38 (2006)

    Article  Google Scholar 

  12. Leuschel, M., Butler, M.: ProB: a model checker for B. In: Araki, K., Gnesi, S., Mandrioli, D. (eds.) FME 2003. LNCS, vol. 2805, pp. 855–874. Springer, Heidelberg (2003). https://doi.org/10.1007/978-3-540-45236-2_46

    Chapter  Google Scholar 

  13. Méry, D.: Teaching programming methodology using Event B. In: Habrias, H. (ed.) The B Method: from Research to Teaching, Nantes, France, July 2008. Henri Habrias, APCB

    Google Scholar 

  14. Meyer, B.: Applying “design by contract”. Computer 25(10), 40–51 (1992)

    Article  Google Scholar 

  15. Rivera, V., Cataño, N., Wahls, T., Rueda, C.: Code generation for Event-B. Int. J. Softw. Tools Technol. Transf. (STTT) 19, 1–22 (2015)

    Google Scholar 

  16. Robinson, K.: Reflections on the Teaching of System Modelling and Design. AVOCS (2010)

    Google Scholar 

  17. Spivey, M.: An introduction to Z and formal specifications. Softw. Eng. J. 4(1), 40–50 (1989)

    Article  Google Scholar 

  18. Stanley Warford, J.: An experience teaching formal methods in discrete mathematics. SIGCSE Bull. 27(3), 60–64 (1995)

    Article  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Innopolis University, Kazan, Tatarstan, Russia

    Néstor Cataño

Authors
  1. Néstor Cataño
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Néstor Cataño .

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

Cataño, N. (2019). Teaching Formal Methods: Lessons Learnt from Using Event-B. 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_14

Download citation

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

  • 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