nach oben

Erschienen in:

2020 | OriginalPaper | Buchkapitel

Reflections on Teaching Formal Methods for Software Development in Higher Education

verfasst von : Mansur Khazeev, Hamna Aslam, Daniel de Carvalho, Manuel Mazzara, Jean-Michel Bruel, Joseph Alexander Brown

Erschienen in: Frontiers in Software Engineering Education

Verlag: Springer International Publishing

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config

KI-gestützte Suche

Aus

Abstract

Despite the increasing attention to formal verification techniques by industry and academia, the programs of Higher Education to this regard still lie behind, and these concepts are not presented to the majority of Computer Science students trained to be future IT specialists. The primary reason is the presumed complexity of the concepts, tools, and formal processes together with a believed moderate interest of employers, which tends to demotivate students. The starting point of any process of change is typically higher education, which should introduce a thoughtful plan of teaching and practice for the students to get acquainted with these techniques. To do so, it is necessary to preliminary identify the obstacles. The user study described in this paper is examining AutoProof tool to identify the complexities attributed to formal methods. We worked with a cohort of master students in Software Engineering at an Information Technology University and monitored and analyzed their performance and feedback on a pedagogical experience. The work presented in this paper extends our previous research on formal methods education by confirming the findings and adding qualitative considerations to quantitative ones.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

über 102.000 Bücher
über 537 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Finance + Banking
Management + Führung
Marketing + Vertrieb
Maschinenbau + Werkstoffe
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 390 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Maschinenbau + Werkstoffe

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 340 Zeitschriften

aus folgenden Fachgebieten:

Bauwesen + Immobilien
Business IT + Informatik
Finance + Banking
Management + Führung
Marketing + Vertrieb
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Vorheriges Kapitel A Review of the Structure of a Course on Advanced Statistics for Data Scientists

Nächstes Kapitel Experience of Mixed Learning Strategies in Teaching Lean Software Development to Third Year Undergraduate Students

https://moodle.org/.

http://se.inf.ethz.ch/research/autoproof/tutorial/downloads/tutorial.pdf.

http://se.inf.ethz.ch/research/autoproof/manual/.

Barnett, M., Leino, K.R.M., Schulte, W.: The Spec# programming system: an overview. In: Barthe, G., Burdy, L., Huisman, M., Lanet, J.-L., Muntean, T. (eds.) CASSIS 2004. LNCS, vol. 3362, pp. 49–69. Springer, Heidelberg (2005). https://doi.org/10.1007/978-3-540-30569-9_3CrossRef

Bobrov, E., Bucchiarone, A., Capozucca, A., Guelfi, N., Mazzara, M., Masyagin, S.: Teaching DevOps in academia and industry: reflections and vision. In: Bruel, J.-M., Mazzara, M., Meyer, B. (eds.) DEVOPS 2019. LNCS, vol. 12055, pp. 1–14. Springer, Cham (2020). https://doi.org/10.1007/978-3-030-39306-9_1CrossRef

Bobrov, E., et al.: DevOps and its philosophy: education matters!. Microservices, pp. 349–361. Springer, Cham (2020). https://doi.org/10.1007/978-3-030-31646-4_14CrossRef

Burdy, L., et al.: An overview of JML tools and applications. Int. J. Soft. Tools Technol. Transf. 7(3), 212–232 (2004). https://doi.org/10.1007/s10009-004-0167-4CrossRef

Cataño, N.: An empirical study on teaching formal methods to millennials. In: Proceedings of the 1st International Workshop on Software Engineering Curricula for Millennials, SECM ’17, Buenos Aires, Argentina, pp. 3–8. IEEE Press (2017)

Clarke Jr., E.M., Grumberg, O., Peled, D.A.: Model Checking. MIT Press, Cambridge (1999)MATH

de Carvalho, D.: Teaching programming and design-by-contract. In: Auer, M.E., Tsiatsos, T. (eds.) ICL 2018. AISC, vol. 916, pp. 68–76. Springer, Cham (2020). https://doi.org/10.1007/978-3-030-11932-4_7CrossRef

ES: The Eiffel Method and Language. https://www.eiffel.org/doc/eiffel/Eiffel

Floyd, R.W.: Assigning meanings to programs. In: Proceedings of the Symposium on Applied Math, vol. 19, pp. 19–32. American Mathematical Society (1967)

10.

Freeman, S., et al.: Active learning increases student performance in science, engineering, and mathematics. Proc. Natl. Acad. Sci. 111(23), 8410–8415 (2014)CrossRef

11.

Furia, C.A., Poskitt, C.M., Tschannen, J.: The autoproof verifier: usability by non-experts and on standard code. In: Proceedings of Formal Integrated Development Environment, F-IDE 2015 (2015). Electron. Proc. Theor. Comput. Sci. 187, 42–55 (2015)

12.

Gibson, P., Méry, D.: Teaching formal methods: lessons to learn. In: Proceedings of the 2nd Irish Conference on Formal Methods, IW-FM’98, Swindon, GBR, pp. 56–68. BCS Learning & Development Ltd. (1998)

13.

Object Management Group: Object constraint language. https://www.omg.org/spec/OCL/About-OCL/

14.

Hoare, C.A.R., Misra, J., Leavens, G.T., Shankar, N.: The verified software initiative: a manifesto. ACM Comput. Surv. 41(4), 22:1–22:8 (2009)

15.

Ishikawa, F., Yoshioka, N., Tanabe, Y.: Keys and roles of formal methods education for industry: 10 year experience with top SE program. In: Bollin, A., Margaria, T., Perseil, I. (eds.) Proceedings of the First Workshop on Formal Methods in Software Engineering Education and Training, FMSEE&T 2015, co-located with 20th International Symposium on Formal Methods (FM 2015), Oslo, Norway, 23 June 2015. CEUR-WS.org (2015). CEUR Workshop Proc. 1385, 35–42 (2015)

16.

Jaume, M., Laurent, T.: Teaching formal methods and discrete mathematics. In: Dubois, C., Giannakopoulou, D., Méry, D. (eds.) Proceedings 1st Workshop on Formal Integrated Development Environment, Grenoble, France, 6 April 2014. Open Publishing Association (2014). Electron. Proc. Theor. Comput. Sci. 149, 30–43 (2014)

17.

Khazeev, M., Mazzara, M., Aslam, H., de Carvalho, D.: Towards a broader acceptance of formal verification tools. In: Auer, M.E., Hortsch, H., Sethakul, P. (eds.) ICL 2019. AISC, vol. 1135, pp. 188–200. Springer, Cham (2020). https://doi.org/10.1007/978-3-030-40271-6_20CrossRef

18.

Liu, S., Takahashi, K., Hayashi, T., Nakayama, T.: Teaching formal methods in the context of software engineering. ACM SIGCSE Bull. 41(2), 17–23 (2009)CrossRef

19.

Mazzara, M., Naumchev, A., Safina, L., Sillitti, A., Urysov, K.: Teaching DevOps in corporate environments. In: Bruel, J.-M., Mazzara, M., Meyer, B. (eds.) DEVOPS 2018. LNCS, vol. 11350, pp. 100–111. Springer, Cham (2019). https://doi.org/10.1007/978-3-030-06019-0_8CrossRef

20.

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

21.

Miller, J.F.: Teaching and learning formal methods, improving productivity. In: Butterfield, A., Haegele, K. (eds.) 3rd Irish Workshop on Formal Methods, Galway, Ireland, July 1999. Workshops in Computing. BCS (1999)

22.

O’Regan, G.: Z formal specification language. Concise Guide to Formal Methods. UTCS, pp. 151–166. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-64021-1_8CrossRefMATH

23.

Pressman, R.S.: Software Engineering: A Practitioner’s Approach, 7th edn. McGraw-Hill Higher Education, New York (2010). OCLC: ocn271105592MATH

24.

Sobel, A.E.K., Saiedian, H., Stavely, A., Henderson, P.: Teaching formal methods early in the software engineering curriculum. In: Proceedings of the 13th Conference on Software Engineering Education & Training, CSEET ’00, p. 55. IEEE Computer Society (2000)

25.

Sotiriadou, A., Kefalas, P.: Teaching formal methods in computer science undergraduates. In: International Conference on Applied and Theoretical Mathematics (2000)

26.

Tretmans, J., Wijbrans, K., Chaudron, M.: Software engineering with formal methods: the development of a storm surge barrier control system revisiting seven myths of formal methods. Formal Meth. Syst. Des. 19(2), 195–215 (2001)CrossRef

27.

Tschannen, J., Furia, C.A., Nordio, M., Polikarpova, N.: AutoProof: auto-active functional verification of object-oriented programs. In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 566–580. Springer, Heidelberg (2015). https://doi.org/10.1007/978-3-662-46681-0_53CrossRef

Titel: Reflections on Teaching Formal Methods for Software Development in Higher Education
verfasst von: Mansur Khazeev
Hamna Aslam
Daniel de Carvalho
Manuel Mazzara
Jean-Michel Bruel
Joseph Alexander Brown
Verlag: Springer International Publishing
Buch: Frontiers in Software Engineering Education
Print ISBN: 978-3-030-57662-2

Electronic ISBN: 978-3-030-57663-9

Copyright-Jahr: 2020
DOI: https://doi.org/10.1007/978-3-030-57663-9_3

Springer Professional

Abstract

Bitte loggen Sie sich ein, um Zugang zu Ihrer Lizenz zu erhalten.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"

Premium Partner