[go: up one dir, main page]
More Web Proxy on the site http://driver.im/
Skip to main content
Springer Nature Link
Log in

On Education and Training in Formal Methods for Industrial Critical Systems

  • Conference paper
  • First Online:
Formal Methods for Industrial Critical Systems (FMICS 2021)

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

Abstract

The 2020 expert survey on formal methods has put one topic into the focus of the formal methods for industrial critical systems community: education and training. Of three overall conclusions, the first one finds the survey to indicate “a consensus about the essential role of education”. At the same time, survey results and individual expert statements indicate largely open challenges. In this work, we analyse the 2020 expert survey results from an education and training perspective, and we discuss the proposal of an integrative approach with respect to these challenges. A central enabler for the integrated approach is the modern, inclusive interpretation of formal methods as put forth in the survey report and a differentiated understanding of roles (or stakeholders) in formal methods for industrial critical systems.

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
£29.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
GBP 19.95
Price includes VAT (United Kingdom)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
GBP 35.99
Price includes VAT (United Kingdom)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
GBP 44.99
Price includes VAT (United Kingdom)
  • 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

Similar content being viewed by others

Notes

  1. 1.

    https://www.fmeurope.org/teaching/.

  2. 2.

    “A method is called formal method if and only if its techniques and tools can be explained in mathematics.” We have adopted this one for our course (cf. Sect. 6).

  3. 3.

    Where we would not exclude the 3rd row, as we shall add (cf. Sect. 3.1).

  4. 4.

    Also see Manfred Broy’s individual statement on managers [28].

  5. 5.

    Woodcock et al. [65] already report “a difficulty in communication between the verifiers and the signalling engineers, [...]” (solved by an ad-hoc solution) in the SACEM project; a problem that eng./utilise people are supposed to substantially mitigate.

  6. 6.

    We feel that the ‘formal methods engineer’ proposed in Frank de Boer’s individual statement [28] is positioned in the intersection yet a bit stronger on eng./conduct, while Stefan Kowalewski and Antti Valmari [28] seem to tend to eng./utilise.

  7. 7.

    See Jan Friso Groote’s individual statement on “change the (industrial) society” [28].

  8. 8.

    Also see Radu Mateescu’s statement on “‘formal methods culture’” [28].

  9. 9.

    Also see Stefan Kowalewski, Martin Leucker, and Cesare Tinelli in [28].

  10. 10.

    We feel that Benjamin Monate’s note on “be modest with formal methods” and incremental training [28] points into the exact same direction.

  11. 11.

    Also see individual statement of Joseph Sifakis [28].

  12. 12.

    Also see the individual statement of Edward A. Lee [28].

  13. 13.

    Mainly as undergraduate compulsory course, majority of audience on B. Sc. in C.S. study plan, 4th semester/2nd year, open to students on M. Sc. and other study plans; heterogeneous previous knowledge; also offered as graduate block course at NM-AIST, Tanzania, with very heterogeneous previous knowledge; see [62] for details.

References

  1. AbsInt: Astreé software (2020). http://www.absint.com/astree

  2. Aceto, L., Ingólfsdóttir, A., Larsen, K.G., Srba, J.: Reactive Systems: Modelling, Specification and Verification. Cambridge University Press, Cambridge (2007)

    Google Scholar 

  3. Aceto, L., Ingólfsdóttir, A., Larsen, K.G., Srba, J.: Teaching concurrency: theory in practice. In: Gibbons et al. [30], pp. 158–175

    Google Scholar 

  4. Anderson, L.W., Krathwohl, D.R., et al. (eds.): A Revision of Bloom’s Taxonomy of Educational Objectives. Longman, New York (2001)

    Google Scholar 

  5. Apt, K.R., de Boer, F.S., Olderog, E.: Verification of Sequential and Concurrent Programs. Texts in Computer Science. Springer, London (2009). https://doi.org/10.1007/978-1-84882-745-5

  6. Balzert, H.: Lehrbuch der Softwaretechnik: Basiskonzepte und Requirements Engineering, 3rd edn. Spektrum (2009)

    Google Scholar 

  7. Bauer, F.L.: Software engineering. In: IFIP Congress, no. 1, pp. 530–538 (1971)

    Google Scholar 

  8. Bjørner, D.: Software Engineering: Abstraction and Modelling. EATCS, vol. 1. Springer, Heidelberg (2006). https://doi.org/10.1007/3-540-31288-9

  9. Bjørner, D., Havelund, K.: 40 years of formal methods - some obstacles and some possibilities? In: Jones, C.B., Pihlajasaari, P., Sun, J. (eds.) FM 2014. LNCS, vol. 8442, pp. 42–61. Springer, Cham (2014). https://doi.org/10.1007/978-3-319-06410-9_4

  10. Bourque, P., Fairley, R. (eds.): Guide to the Software Engineering Body of Knowledge, Version 3.0. IEEE (2014)

    Google Scholar 

  11. Boute, R.T., Oliveira, J.N. (eds.): Formal Methods in the Teaching Lab, Workshop Preprints (2006)

    Google Scholar 

  12. Bowen, J.P., et al.: An invitation to formal methods. IEEE Comput. 29(4), 16–30 (1996)

    Google Scholar 

  13. Bowen, J.P., Hinchey, M.G.: Seven more myths of formal methods. IEEE Softw. 12(4), 34–41 (1995)

    Google Scholar 

  14. Bowen, J.P., Hinchey, M.G.: Ten commandments of formal methods. Computer 28(4), 56–63 (1995)

    Google Scholar 

  15. Bowen, J.P., Hinchey, M.G.: Ten commandments of formal methods ...ten years later. Computer 39(1), 40–48 (2006)

    Google Scholar 

  16. Brakman, H., Driessen, V., Kavuma, J., Bijvank, L.N., et al.: Supporting formal method teaching with real-life protocols. In: Boute and Oliveira [11], pp. 59–68

    Google Scholar 

  17. Burgueño, L., Vallecillo, A., Gogolla, M.: Teaching UML and OCL models and their validation to software engineering students: an experience report. Comput. Sci. Educ. 28(1), 23–41 (2018)

    Google Scholar 

  18. Cerone, A., Roggenbach, M. (eds.): Formal Methods - Fun for Everybody, FMFun, Proceedings. CCIS, vol. 1301. Springer, Cham (2020). https://doi.org/10.1007/978-3-030-71374-4

  19. Cerone, A., Roggenbach, M., Davenport, J., Denner, C., Farrell, M., et al.: Rooting formal methods within higher education curricula for computer science and software engineering - a white paper. CoRR abs/2010.05708 (2020)

    Google Scholar 

  20. Cerone, A., Roggenbach, M., Schlingloff, B.H., et al.: Teaching formal methods for software engineering - ten principles. informatica didactica 9 (2011)

    Google Scholar 

  21. Cohen, E., et al.: VCC: a practical system for verifying concurrent C. In: Berghofer, S., et al. (eds.) TPHOLs. LNCS, vol. 5674, pp. 23–42. Springer, Heidelberg (2009). https://doi.org/10.1007/978-3-642-03359-9_2

  22. Damm, W., Harel, D.: LSCs: Breathing life into Message Sequence Charts. FMSD 19(1), 45–80 (2001)

    Google Scholar 

  23. Davies, J., Simpson, A., Martin, A.P.: Teaching formal methods in context. In: Dean and Boute [24], pp. 185–202

    Google Scholar 

  24. Dean, C.N., Boute, R.T. (eds.): TFM. LNCS, vol. 3294. Springer, Heidelberg (2004). https://doi.org/10.1007/978-3-540-30472-2

  25. Dietsch, D., Langenfeld, V., Westphal, B.: Formal requirements in an informal world. In: FORMREQ, pp. 14–20. IEEE (2020)

    Google Scholar 

  26. Dongol, B., Petre, L., Smith, G. (eds.): FMTea, LNCS, vol. 11758. Springer, Cham (2019). https://doi.org/10.1007/978-3-030-32441-4

  27. Feo Arenis, S., Westphal, B., Dietsch, D., Muñiz, M., Andisha, A.S., Podelski, A.: Ready for testing: ensuring conformance to industrial standards through formal verification. Form. Asp. Comput. 28(3), 499–527 (2016)

    Google Scholar 

  28. Garavel, H., ter Beek, M.H., van de Pol, J.: The 2020 expert survey on formal methods. In: ter Beek, M.H., Nickovic, D. (eds.) FMICS. LNCS, vol. 12327, pp. 3–69. Springer, Cham (2020). https://doi.org/10.1007/978-3-030-58298-2_1

  29. Giannakopoulou, D., Pressburger, T., Mavridou, A., Rhein, J., Schumann, J., Shi, N.: Formal requirements elicitation with FRET. In: Sabetzadeh, M., Vogelsang, A., et al. (eds.) REFSQ Workshops. CEUR, vol. 2584. CEUR-WS.org (2020)

    Google Scholar 

  30. Gibbons, J., et al. (eds.): TFM, LNCS, vol. 5846. Springer, Heidelberg (2009). https://doi.org/10.1007/978-3-642-04912-5

  31. Gibson, J.P., Méry, D.: Teaching formal methods: lessons to learn. In: Flynn, S., Butterfield, A. (eds.) 2nd Irish Workshop on Formal Methods, Cork, Ireland, 2–3 July 1998. Workshops in Computing, BCS (1998)

    Google Scholar 

  32. Glinz, M.: The teacher: “concepts!” the student: “tools!”. Softwaretechnik-Trends 16(1) (1996)

    Google Scholar 

  33. Hall, A.: Seven myths of formal methods. IEEE Softw. 7(5), 11–19 (1990)

    Google Scholar 

  34. Harel, D.: Statecharts: a visual formalism for complex systems. SCP 8(3), 231–274 (Jun 1987)

    Google Scholar 

  35. Harel, D.: Some thoughts on statecharts, 13 years later. In: Grumberg, O. (ed.) CAV. LNCS, vol. 1254, pp. 226–231. Springer, Cham (1997). https://doi.org/10.1007/978-3-030-58298-2_1

  36. Heitmeyer, C.L.: On the need for practical formal methods. In: Ravn, A.P., Rischel, H. (eds.) FTRTFT. LNCS, vol. 1486, pp. 18–26. Springer, Heidelberg (1998). https://doi.org/10.1007/BFb0055332

  37. Holloway, C.M.: Why engineers should consider formal methods. In: 16th Digital Avionics Systems Conference, Proceedings. vol. 1, pp. 1.3–16 (1997)

    Google Scholar 

  38. 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 et al. [30], pp. 57–71

    Google Scholar 

  39. Istenes, Z. (ed.): Formal Methods in Computer Science Education, FORMED2008, Budapest, Hungary, 29 March 2008, Proceedings (2008)

    Google Scholar 

  40. Jackson, D.: A direct path to dependable software. CACM 52(4) (2009)

    Google Scholar 

  41. Kiniry, J.R., Zimmerman, D.M.: Secret ninja formal methods. In: Cuéllar, J., Maibaum, T.S.E., et al. (eds.) FM. LNCS, vol. 5014, pp. 214–228. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-68237-0_16

  42. Klose, J., Wittke, H.: An automata based interpretation of live sequence charts. In: Margaria, T., Yi, W. (eds.) TACAS. LNCS, vol. 2031, pp. 512–527. Springer, Heidelberg (2001). https://doi.org/10.1007/3-540-45319-9_35

  43. Lamport, L.: Who builds a house without drawing blueprints? CACM 58(4), 38–41 (2015)

    Google Scholar 

  44. Langenfeld, V., Dietsch, D., Westphal, B., Hoenicke, J.: Scalable analysis of real-time requirements. In: Damian, D., et al. (eds.) RE, pp. 234–244. IEEE (2019)

    Google Scholar 

  45. Larsen, K.G., Pettersson, P., Yi, W.: Uppaal in a nutshell. Int. J. Softw. Tools Technol. Transf. 1(1), 134–152 (1997)

    Google Scholar 

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

    Google Scholar 

  47. Loomes, M., Christianson, B., Davey, N.: Formal systems, not methods. In: Dean and Boute [24], pp. 47–64

    Google Scholar 

  48. Ludewig, J., Lichter, H.: Software Engineering, 3rd edn. dpunkt (2013)

    Google Scholar 

  49. Mandrioli, D.: Advertising formal methods and organizing their teaching: yes, but ... In: Dean and Boute [24], pp. 214–224

    Google Scholar 

  50. Mandrioli, D.: On the heroism of really pursuing formal methods. In: Gnesi, S., Plat, N. (eds.) FormaliSE, pp. 1–5. IEEE (2015)

    Google Scholar 

  51. Nielson, F., Nielson, H.R.: Formal Methods. Springer, Heidelberg (2019). https://doi.org/10.1007/978-3-030-05156-3

  52. Noble, J., Pearce, D.J., Groves, L.: Introducing alloy in a software modelling course. In: Istenes [39], pp. 81–90

    Google Scholar 

  53. Ölveczky, P.C.: Designing Reliable Distributed Systems - A Formal Methods Approach Based on Executable Modeling in Maude. Undergraduate Topics in Computer Science, Springer, London (2017). https://doi.org/10.1007/978-1-4471-6687-0

  54. OMG: OCL, Version 2.4. OMG Document Number formal/2014-02-03 (2014)

    Google Scholar 

  55. OMG: UML, Version 2.5.1. OMG Document Number formal/2017-12-05 (2017)

    Google Scholar 

  56. Reed, J.N., Sinclair, J.: Motivating study of formal methods in the classroom. In: Dean and Boute [24], pp. 32–46

    Google Scholar 

  57. Robinson, K.: Reflecting on the future: objectives, strategies and experiences. In: Istenes [39], pp. 15–24

    Google Scholar 

  58. Roggenbach, M., Cerone, A.: Formal Methods for Software Engineering. Springer, Cham (2021, to appear)

    Google Scholar 

  59. Sommerville, I.: Software Engineering, 9th edn. Pearson, London (2010)

    Google Scholar 

  60. Stachowiak, H.: Allgemeine Modelltheorie. Springer, New York (1973)

    Google Scholar 

  61. Westphal, B.: Teaching software modelling in an undergraduate introduction to software engineering. In: Burgueño, L., Pretschner, A., Voss, S., et al. (eds.) EduSymp@MODELS, pp. 690–699. IEEE (2019)

    Google Scholar 

  62. Westphal, B.: On complementing an undergraduate software engineering course with formal methods. In: Daun, M., et al. (eds.) CSEE&T, pp. 1–10. IEEE (2020)

    Google Scholar 

  63. Wing, J.M.: A specifier’s introduction to formal methods. IEEE Comput. 23(9), 8–24 (1990)

    Google Scholar 

  64. Wing, J.M.: Invited talk: weaving formal methods into the undergraduate computer science curriculum. In: Rus, T. (ed.) AMAST. LNCS, vol. 1816, pp. 2–9. Springer, Heidelberg (2000). https://doi.org/10.1007/3-540-45499-3_2

  65. Woodcock, J., Larsen, P.G., Bicarregui, J., Fitzgerald, J.S.: Formal methods: practice and experience. ACM Comput. Surv. 41(4), 19:1–19:36 (2009)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Albert-Ludwigs-Universität Freiburg, Freiburg, Germany

    Bernd Westphal

Authors
  1. Bernd Westphal
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Bernd Westphal .

Editor information

Editors and Affiliations

  1. Technical University of Denmark, Kongens Lyngby, Denmark

    Alberto Lluch Lafuente

  2. KBR/NASA Ames Research Center, Moffett Field, CA, USA

    Anastasia Mavridou

Rights and permissions

Reprints and permissions

Copyright information

© 2021 Springer Nature Switzerland AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Westphal, B. (2021). On Education and Training in Formal Methods for Industrial Critical Systems. In: Lluch Lafuente, A., Mavridou, A. (eds) Formal Methods for Industrial Critical Systems. FMICS 2021. Lecture Notes in Computer Science(), vol 12863. Springer, Cham. https://doi.org/10.1007/978-3-030-85248-1_6

Download citation

  • DOI: https://doi.org/10.1007/978-3-030-85248-1_6

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-030-85247-4

  • Online ISBN: 978-3-030-85248-1

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation