My recommendations
for teaching formal methods are probably made from a more industrial
point of view than most of the other contributions from the advisory
board. For the last 10 years I have been involved with transferring
the VDM technology we have developed at IFAD to primarily industrial
companies. Thus I probably have a more pragmatic approach to formal
methods education than most university researchers and lecturers.
However, I still feel that my experience can be used with advantage
for academic formal methods education.
I believe that formal methods education should be introduced in stages and that in order to keep the interest for the students the use of tools is extremely important. Furthermore I feel that it is important to the students that the use of formal methods in themselves simply is a means to achieve better systems/software and not a goal in itself. It is my experience from some formal methods promoters that this is not sufficiently stressed. Thus it is in my opinion important to be able to envisage how one's formal method and the associated tools could be applied in a real system/software development environment.
The first stage of formal methods I believe is to teach students to do abstraction to produce abstract models and validate such models. The stress should be on practical modelling skills rather than language and tool detail. The examples and coursework exercises should preferably be based on industrial applications instead of the usual toy examples that do not inspire the students interest for the course. The tools should support understanding of specifications by admitting execution of formal models. This is a quick way of validation, which in my experience is an efficient way to get students appreciating the strength of abstraction. John Fitzgerald and I wrote a book, Modelling Systems Practical Tools and Techniques in Software Development, aiming to achieve this. Course material is also available.
The next stage of formal methods is to enhance the number of validation techniques that can be employed using formal methods. This involves both the use of theorem provers, model checkers and proof support systems. Note again that the ease for using the systems and the examples chosen should be appealing for the students. In addition I feel that it is very important that the students become aware of the effort for using this technology compared to conventional techniques used in industry. Unless the students get a feel for this it will be very hard for them afterwards to be able to have an influence in the improvement of the development processes and products in industrial environments. Most industrial organisations are not yet ready to start using this kind of technology and thus a gradual introduction is necessary. Use evolution rather than revolution.
In order to aid the academic education of formal methods IFAD
has decided to make our VDMTools freely
available for academic site licenses. There is not yet any
proof support available but this will follow later this year on
the beta-release
web page for VDMTools. I hope that this will be beneficial
for all of us.