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

insights that come from a range of analytic techniques, from manual to automated. In
our own teaching experience [88], we apply a “lightweight” approach using VDM++.
We emphasise practical applications, teaching through a range of examples derived
from industry application. A strength of the approach is the relative familiarity of the
structure of VDM++ to undergraduates already versed in object-oriented programming.
However, analysis is so far limited to specification testing and proof obligation genera-
tion. Advanced techniques including proof and model checking, are taught separately.
Practical experience, discussions centered around formal models and sharing of insights
are central to the approach if we are to help students move from superficial and atomistic
learning to a deeper appreciation of the costs and benefits of abstraction and rigour.
In a revision to its undergraduate curriculum in formal techniques, Newcastle is look-
ing at beginning with JML (because Java is taught extensively in the first part of the cur-
riculum), raising students' expectations about the forms of push-button analysis that can
be applied to their programs. Similar concepts (pre-/post specification, use of invariants
etc.) can then be lifted to the design level by teaching model-oriented specification in
VDM++ with tool support and introducing validation through structured argument. At
the final level, aimed at software engineering specialists who may well become tools
developers themselves, we will introduce proof and model-checking as the technology
that underpins the advanced analysis of both programs and design models.

4.3 Delivery

There has been much debate around the placing of formal methods in the wider com-
puting curriculum. Should they be treated as a distinct discipline or should they be fully
integrated with other material? van Lamsweerde [63] argues for the integration of for-
mal methods into normal development activities. This surely suggests that training in
formal techniques should be, to a large extent, part of the normal components of com-
puter science and software engineering curricula. Wing's suggested approach [91] is
to teach common elements (state machines, invariants, abstraction mappings, composi-
tion, induction, specification and verification) and to use tools to reinforce theory. She
identifies the difficulty of winning fellow faculty members round as a real impediment
to this [92].
Recent work [93] suggests that students' performance improves when they are pro-
vided with Integrated Development Environments encompassing specification support
tools, static analysers and provers. It remains to be seen if this level of tooling deepens
students' understanding of the models that they are creating and the formalism used.
However, it may be seen as a step in the right direction by freeing students to concen-
trate on the meaning of a model rather than automatically checkable characteristics.

5 Concluding Remarks

Will formal methods remain niche technology with localised use dependent on energetic
champions? We believe that some major changes are required to help the mainstream
get the benefits of abstraction and rigour in system modelling and analysis. Tools are
vital and, we have argued, a full range of tools have to be offered in a way that allows