First Meeting (2018/02/23)

Agenda and Minutes

Feb 23, 2018 Meetings

February 23-24, 2018, FME Teaching Committee, first meeting: Agenda and references

Agenda

  1. Welcome and introductions
  2. What does Teaching FM will focus on?
  • Database of courses
  • Resources
  • BoK (body of knowledge)
  • Examples/Case Studies repositories
  1. Short term goals
  • Database of formal methods courses
  • What is a formal methods course
  • Format of database (pointers to courses, not content)
  • Assign person(s) to design the database and maintain it on some webpage, should be yearly updated and made available to FME
  • Some deadline for all of us populating it with what we know of so far (May-June 2018?)
  • Some kind of presence at the FM Conference this year? Workshop chairs: Maurice ter Beek, CNR/ISTI, IT and Helen Treharne, University of Surrey, UK
  1. Improve the teaching of FM
  • MOOC courses?
  • Database of formal methods case studies
  • There are databases/repositories for software: GitHub
  • There are databases/repositories for biological models: BioModels
  • Are there any such repositories for formal models? Archive of Formal Proofs (for Isabelle)
  • Body of Knowledge
  1. Coordinate the FM education of researchers
  • If someone needs a course on some method, connect teachers with respective researchers
  • organize seasonal schools on FM; is Marktoberdorf “the” current FM school? what other schools are there, if?
  • apply for some mobility funding for researchers to travel in order to get familiar with some method
  • organize some MSc program in FM, with the graduated getting a FME badge/certification
  • if some requirements are met?
  • what about teachers? can they earn badges in what they are teaching and if yes, what should be the criteria?
  • if we find there’s interest, we could later transform this into a PhD program
  1. Make industry and life sciences beneficiaries of FM
  • provide case studies from Academia to Industry/Science to demonstrate potential
  • get interesting/real life problems to analyse from Industry/Science to Academia

References

——————————— References ——————————-

[1] J. Davies, J. Gibbons, M. Hinchey and K. Taguchi (editors), “Preface Special Issue on Formal Methods Education and Training”, ACM SIGCSE Bulletin inroads, vol. 41, issue 2, June, pp14-16 (2009)

[2] J. Davies, J. Gibbons, M. Hinchey and K. Taguchi (editors), “Proceedings of the First International Workshop on Formal Methods Education and Training” Technical Report GRACE-TR-2008-03, Grace Center, National Institute of Informatics (2008) Note: “XXX education and training” is a conventional naming of conferences/workshops on education in Software Engineering (e.g., CSEE&T (Software Engineering Education and Training). I preferred this rather than “Teaching Formal Methods”.

[3] H. Nishihara, K. Shinozaki, K. Hayamizu, T. Aoki, K. Taguchi, F. Kumeno, “Model Checking Education for Software Engineers in Japan”, in ACM SIGCSE Bulletin inroads, vol 41, issue 2, June, pp45-50 (2009)

[4] K. Taguchi, H. Nishihara, T. Aoki, F. Kumeno, K. Hayamizu, K. Shinozaki, “Building a Body of Knowledge on Model Checking for Software Development”, in Proceedings of COMPSAC ’13, pp784-789, IEEE (2013) [5] F. Ishikawa, K. Taguchi, N. Yoshioka, S. Honiden, “What Top-Level Engineers Tackle after Learning Formal Methods –Experiences from the Top SE Project”, in Proceedings of Teaching Formal Methods (TFM) ’09, Eindhoven (2009)

[6] C. Artho, K. Taguchi, Y. Tahara, S. Honiden, Y. Tanabe, “Teaching Software Model Checking” Proceedings in Formal Methods in Computer Science Education (FORMED) ’08, pp171-179, Budapest (2008)

[7] S. Honiden, Y. Tahara, N. Yoshioka, K. Taguchi, H. Washizaki, “TopSE: Educating Superarchitects Who Can Apply Software Engineering Tools to Practical Development in Japan”, in Proceedings of IEEE/ACM International Conference on Software Engineering (ICSE) ’07, pp708-718, Minneapolis (2007) Note: ICSE traditionally has a session on education. This paper appeared in the session.

[8] J. Bowen, S. Reeves: From a Community of Practice to a Body of Knowledge: A Case Study of the Formal Methods Community. FM 2011: 308-322

[9] S. Gruner, A. Kumar, T. Maibaum: Towards a Body of Knowledge in Formal Methods for the Railway Domain: Identification of Settled Knowledge. FTSCS 2015: 87-102

Minutes

  1. We introduced ourselves.
  • Luigia Petre
    • Working with Action Systems and Event-B at Åbo Akademi University in Turku, Finland. Currently on sabbatical at University of South Florida in Tampa, US. Originally from Romania. Been involved in organising several formal methods conferences. In the process of changing my teaching profile, but have taught before courses on Software Architecture, Networks, Approximation and Randomised Algorithms. Interested in integrating formal methods.
  • Rustan Leino
  • Leila Ribeiro
  • Alexandra Mendes
  • Joao Ferreira
  • Catherine Dubois
    • I work at ENSIIE, a computer science engeneering school in France, near Paris. My research topics concern deductive formal methods and currently I am very much i interested in interoperability of provers. I teach formal methods in different courses. The first course is a brief introduction to reasoning about programs (Hoare logic, Frama-C WP), the rest of the course being about testing. A second course (42 hours) is about B and refinement and application to security (access control policies). And a last course (again 42 hours) concerns Coq, type theory and formal semantics. I also teach an introduction to abstract interpretation in a master course.
  • Dino Mandrioli
    • I am at Politcnico di Milano I teach a basic course on theoretical computer science and algorihms (automata, languages, computatbility, complexity, fundamental algorithms) at the undergraduate level and a Formal methods for concurrent and real-time systems one (Hoare method, timed Petri nets, logic proofs, industrial case studies) for graduate students. As for research, my group developed the logic language TRIO for the specificaion and verification of real-time systems and applied it in various industrial cooperations. Recently, we addressed our efforts towards innnovative techniques to empower model checking.
  • Bernd Fisher
  • Kenji Taguchi
  • Graeme Smith
    • I work at the University of Queensland, Australia. I currently research in the area of formal verification of concurrent programs, and have an ongoing collaboration with John Derrick at the University of Sheffield, UK. I also teach formal methods in 2 courses. The first course is an introduction to reasoning about programs. I cover Hoare logic and use the KeY tool to allow students to perform program verification on a simple while-language in the first part of the course, and on Java programs (using JML as the specification language) later in the course. The course also introduces weakest preconditions and the refinement calculus. The second course is on concurrent programming. It is not primarily a formal methods course, but I do teach the students how to use the Spin model checker to check properties of simple concurrent code
  1. We wanted to set up the focus of this teaching committee. At least we have identified the following directions we would like to focus on
  • Database of formal methods courses
    • we will start from the 2004 database that Jose Nuno Oliveira has compiled
    • Alexandra and Joao will scan the database to prune it of old courses no longer active and they will have a version of it in GitHub where everyone will be able to upload courses
    • in the meantime everyone should collect courses that they think qualify as formal methods courses; we leave it at the discretion of each of us as to what qualifies and what not; for instance there are programming courses with only some invariants that could also be good to add now in the beginning, and maybe we store them under a distinct section
    • while we collect these courses, we can also think if the database we now have needs some extensions, maybe we need some extra information stored for each course, so that we easily find information given some search terms
  • Repository of examples and case studies on using formal methods
    • this we felt would be very good to have and sadly missing right now, from the simple examples that one can use in class for explaining simple things to the more complex case studies that really show the potential of various methods
    • there is GitHub for software and BioModels for biological case studies; there is even the Archive of Formal Proofs for Isabelle models, but not for formal methods in general
    • we need a strategy for designing it and then we will start populating it; any ideas here?
  • Body of Knowledge on Formal Methods
    • we have a starting point here, led by Kenji Taguchi, Jonathan Bowen, and others
    • need to study it and start adding to it
    • there are some links in the attached word doc to what exists now
  • Repository of exercises and exam questions on formal methods (under lock, to be released by their authors for fellow-teachers when needed, ie not for students)
    • this should be similar to the repository of case studies in principle, so when we design one, we have the other too, with the exception of securing the exam questions
  • List of summer/winter schools on formal methods
  1. “FME Approved” courses - we need to discuss this more
  • FME is a professional society, so we could take advantage of this
  • Organising certification (and curricula) might be difficult, we should focus on a lighter objective; keep this on our minds
  1. We don’t plan anything at the moment for FM in Oxford, we will maybe send some info later on
  • Someone mentioned getting a 2-minute slot to promote what we are doing. This might be a way to help get the database(s) populated.
  • We discussed about having online forms to distribute so that we get input from other people too
  1. We will have the next meeting in May, Luigia sends a Doodle poll searching for a reasonable date for everyone. In the meantime we keep in touch via email.

The aim of the FME Teaching Committee is to support a worldwide improvement in learning formal methods, mainly by teaching but also via self-learning.