Balancing Insight and Effort: The Industrial Uptake of Formal Methods - Formal Methods and Hybrid Real-Time Systems - page 247

4 An Educational Viewpoint

A fool with a tool is still a fool.

Grady Booch

We have argued that successful industry adoption of formal techniques requires the bal-
ancing of effort and insight, and that tools and development environments should sup-
port this trade-off. No matter how advanced the tools, they can only achieve a measure
of industry credibility if graduate engineers possess skills in abstraction and rigorous
thinking, and are open to selecting the right techniques for the job. It therefore seems
appropriate to ask how this should affect the aims, content and delivery of formal meth-
ods education.
We should not expect our students to share our motivations. In our experience, many
students are driven by the need to develop skills that will be useful in pursuing a career
and many are also driven by the satisfaction of building a working computer system and
seeing it run. If we care about the industry uptake of formal techniques, we should care
about all our students and not just the potential PhDs.

4.1 Aims
We suggest that the overriding aims of formal methods advocates in education should
be: (i) to help students develop transferable skills of abstraction and rigorous modelling
and analysis; and (ii) to develop the knowledge and skill needed to select tools and tech-
niques on the basis of cost and potential effectiveness. These are not impossibly vague
goals: Sobel's study [84], albeit the subject of a debate on experimental design [85,86],
was a first attempt to assess whether a training in formal techniques may improve stu-
dents' general analytic and problem solving skills [87]. In our teaching [88], with its
origins in industrial courses, we have been led to ask whether we really know what
skills we want to help our students develop and how we could establish whether our
current courses are achieving this. Kramer has recently argued that abstraction skills
are core to computing and that we should try to monitor the development of such skills
through students' development [89]. It has been pointed out that the sorts of test we
need are lacking, as most relevant tests focus on logical reasoning.
At a more practical level, we would like typical graduates, not only the most acad-
emically gifted, to at least know that next generation Integrated Development Environ-
ments will provide a higher static analysis capability than at present and will support
expressive annotation-based languages in the manner of JML [50] and Spec# [90], al-
lowing them to identify hitherto hard-to-detect errors in their code. We want them to
be surprised when such technology is not deployed in the companies where they work
and we would even like them to use it to get the edge on their fellow programmers!
In that way we hope that they will be able to find an appropriate balance in the use of
abstraction and rigour in their own work.

4.2 Content
Giving students a sense of the effort/insight trade-off means exposing them to a range
of analysis techniques as well as offering them experiences that help them to see the