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

in recent years (Section 2). In Section 3, we consider the range of tool features now
becoming available. For each, we discuss the insights to be gained and the effort to be
invested in using them. In Section 4 we discuss the consequences for education and
training if future generations of engineers and research scientists are to take advantage
of the full range of formalisms and tools becoming available now. Finally in Section 5
we give a few concluding remarks.

2 Background: VDM

We have been active in the use of the Vienna Development Method (VDM), one of
the longest established model-oriented formalisms. We studied under Dines Bjørner
and Cliff Jones 1 . Larsen studied in “the Danish School” of VDM, which emphasised
explicit specification of functionality, leading to the possibility of executable models.
Fitzgerald was rooted in “the British School” which gave greater prominence to the
need for proof and, where possible, implicit specification by postconditions denoting
relations on inputs, results and persistent state variables. The Danish School empha-
sised large-scale systems and compiler technology; the British School was focussed on
validation through proof and refinement-based development. Jones provides an inter-
esting account of the scientific development of VDM [11]. Our collaboration has, so
some extent, been the story of an accommodation between these two schools.
We worked together briefly on the BSI/ISO standardisation panel of VDM's specifi-
cation language (VDM-SL) [12,13]. Larsen took a leading role in completing the deno-
tational semantics of the full language [14]. He went on to pioneer the development of
industry-strength tool support for VDM-SL in IFAD. Fitzgerald was meanwhile work-
ing on the interaction between modular structuring mechanisms and user-guided proof
in the typed Logic of Partial Functions [15] and started work with the British Aerospace
Dependable Computing Systems Centre at Newcastle University.
Our first close collaboration was on the ConForm project funded under the Euro-
pean Systems and Software Initiative and conducted at British Aerospace Systems and
Equipment (as it then was) in Plymouth. The project involved the concurrent devel-
opment of a security-related software component using, in one stream, current best
practice and, in the other stream, model-oriented specification. The specification was
developed in VDM-SL by BAe engineers, with the IFAD tools and several ad hoc tools
to integrate the formal model with structured methods already in use in the company. A
study of the two parallel developments, while far from being a controlled experiment,
indicated how formally-based tools might be used in practice. As a consequence of our
logging all queries raised against the requirements documents, the study also provided
evidence of the kinds of insight that arise when formal models are constructed [16].
The ConForm experience led us to develop a lightweight and tool-supported ap-
proach to formal modelling that we first presented in 1998 [17]. Subsequently both of
us have used VDM with many different industrial users in various application domains.
Some of the work has been reported in public, e.g. [18,19,20,21].

1

Variously referred to as “the VDM twins” and, with Peter Lucas, as “the Ancient Greeks” be-
hind the original VDM, latterly FME and FM, Symposia! Both of them frequently emphasise
the crucial contributions of Lucas, Bekic and many others to the foundations of VDM.