FME Teaching Committee
Teaching Formal Methods
Second meeting's memo, 23.5.2018
1. Welcome back:
This time Alexandra and Joao could not make it, otherwise everyone was in, despite the challenging hours. We had this meeting exactly three months after the first one. Thanks Kenji and Dino in particular for agreeing to join this slot, although not among their initial favourites.
2. The github repository of FM courses
We have thought on how to store our repository of courses. Dino and Bernd mentioned ResearchGate (https://www.researchgate.net) and Researchr (https://researchr.org/), but in the end we agreed to give GitHub a try. GitHub is primarily a tool for storing and sharing code, but other repositories can be formed, for instance all the papers published on a topic, check the Github repository for reaction systems:
https://github.com/RS-Repo/library. The papers are now stored as “Issues”, and Rustan made a good point in that maybe we should investigate whether the Wiki menu is more appropriate. Bernd thought the “Issues” might offer better measurability. We agreed to investigate this.
3. Courses we found
Graeme sent FM courses he uncovered in Australia and New Zealand. It’s quite nice to see our first courses collected! In particular, New Zealand seems strong! Graeme made these lists by individually emailing people he knew from a forum called “Formal Methods Australia” and from other sources. The response was great, and people commented on how teaching in Formal Methods decreased and how they are quite interested in our actions, wanting to follow and contribute if possible.
4. FMBoK
No new developments so far and we agreed we have to start from somewhere. Bernd proposed the ACM classification of terms (http://delivery.acm.org/10.1145/2380000/2371137/ACMCCSTaxonomy.html?ip=105.226.111.82&id=2371137&acc=OPEN&key=4D4702B0C3E38B35%2E4D4702B0C3E38B35%2E4D4702B0C3E38B35%2E6D218144511F3437&__acm__=1527107802_08980bfd5d30a9c8c73731f196803528) also check this link
https://www.acm.org/about-acm/class. We should also check the FMBoK efforts of Jonathan Bowen, Kenji Taguchi and others, sent as links and references in a previous email. I re-attach the file to this email for easier handling. We could also check the Software Engineering BoK for reference.
5. Other advances on repositories
Not yet.
In addition to what we agreed to store in repos last time though (case studies, simpler and more complex and exam questions), Graeme pointed out that resources on how to teach formal methods are quite valuable as well. A first paper to check on this topic was “(In)formal methods: the lost art” by Carroll Morgan, 2016, link here:
@inproceedings{DBLP:conf/setss/Morgan14,
author = {Carroll Morgan},
title = {(In-)Formal Methods: The Lost Art - {A} Users' Manual},
booktitle = {Engineering Trustworthy Software Systems - First International School,
{SETSS} 2014, Chongqing, China, September 8-13, 2014. Tutorial Lectures},
pages = {1--79},
year = {2014},
crossref = {DBLP:conf/setss/2014},
url = {https://doi.org/10.1007/978-3-319-29628-9_1},
doi = {10.1007/978-3-319-29628-9_1},
timestamp = {Wed, 17 May 2017 14:24:31 +0200},
biburl = {https://dblp.org/rec/bib/conf/setss/Morgan14},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
There is/was? also a course:
http://www.cse.unsw.edu.au/~cs6721/.
6. Some common doc storage for us
We agreed on GoogleDocs, at least for the time being.
7. Other issues
The issue of taking advantage of the Formal Methods community arose and we discussed how we can obtain info on FM courses from people we will anyway meet at FM conference in Oxford, at Formalise in Götenborg, Sweden, at ABZ in Southampton, etc. We agreed that maybe we ask the chairs to inform participants of our committee and to create some handouts for people to fill in wrt FM courses they know about. Rustan made a good point that it is interesting to see how FM teaching evolves over time, for instance to also ask questions like “what tool do you use to teach model checking”.
8. Next steps
This is how we continue.
- Luigia creates a repository in github and adds the courses sent by Graeme there. We then think whether we are happy with this storing mechanism or not.
- We all check the ACM classification and the previous work on FMBoK and come up with proposals on how to revive this initiative.
- Luigia copies all our materials to GoogleDocs and so we’ll have a sharing mechanism
- We make a format for what to ask people about (in emails or in handouts at conferences) wrt FM courses
- We meet again in September, Luigia sends Doodle poll at the end of August...
First meeting's memo, 23.2.2018
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
- 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
- Marktoberdorf, yearly: https://asimod.in.tum.de/2017/index.shtml or the wikipedia link: https://en.wikipedia.org/wiki/Summer_School_Marktoberdorf
- Bertinoro: http://www.sti.uniurb.it/events/sfm16quanticol/
- SRI: (Rustan mentioned)
- Tallinn: (Rustan mentioned, Bernd concurred)
- UK: Middlands
- China: Ian Hayes speaker
- http://www.swu-rise.net.cn/SETSS2017/
- Petter Miller in Zurich in autumn (Rustan mentioned)
- Betrand Meyer on Elba (Rustan mentioned)
- Laser Summer School. It is larger than formal methods.
- ISoLa? (Rustan mentioned)
- DeepSpec
- https://deepspec.org/event/dsss18/
- 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
4. 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
5. 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.
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
3. 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
4. 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
5. 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
6. 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
- old Subgroup of Education http://www4.di.uminho.pt/FME-SoE/index.html
- the course list compiled up to 2004, http://www4.di.uminho.pt/FME-SoE/resources.html by Jose Nuno Oliveira: https://link.springer.com/chapter/10.1007/978-3-540-30472-2_16
- FME members suggest (there was a survey)
- FME could try to have more political involvement with respect to the education systems in Europe to raise concern about the importance of giving, at least, one full mandatory course on FM in every undergraduate curricula.
- Maybe organising an informal event like ”Fun with Formal Methods”: http://www.iis.nsk.su/fwfm2013
- Formal Methods BoK: http://formalmethods.wikia.com/wiki/FMBoK (maintained by Jonathan Bowen)
- References collected by Kenji Taguchi with respect to BoK on FM:
--------------------------------- 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.
Jonathan Bowen' paper on FMBoK
[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
Stefan Gruner' paper on FMBoK
[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
