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

level of automation may be desirable. In the latter the real insight gained by guiding
a proof may help understanding of the rest of the model, in particular detecting and
eliminating defects [73,74].

Until recently, we have not seen a strong enough industrial case for bringing proof
support into VDMTools because of the computational overheads and also the possibility
of having to build an interface for user guidance of the specialised proof process. Our
experience with manual proof support for the proof theory of VDM-SL [15] indicated
that many proof obligations are generated by even a simple model and it is vital to be
able to discharge as many of these as possible without user guidance. In the PROSPER
project [75], it was possible to discharge the vast majority of generated proof obligations
automatically (up to 90 % for a railway application [76]) and we are now working
on reproducing this for VDM++ using HOL4. We leave undischarged obligations for
inspection, but view the development of good human-guided but machine-assisted proof
tools (based on an appreciation of the cognitive aspects of proof) as an essential research
goal.

3.4 Connection to the Development Environment

Modelling and analysis techniques based on formal notations will rarely be used for the
development of an entire system, so their products should fit with the results of apply-
ing other techniques, as well as with the processes employed in the development team.
In order to balance the effort spent on producing the formal models with the insight
gained this is clearly one of the areas with potential for payback in terms of minimising
the time that needs to be spent in the final implementation phases. Supporting this for
VDMTools meant spending major efforts on tasks that formalists might find uninter-
esting, but which are essential for deployment. For example, we have had to develop
interfaces to proprietary WYSIWYG document editors, use ASCII syntax, build code
generators, application programmer interfaces and even links to UML tools! Here we
list some of the features that we consider particularly significant in connecting our tools
to people and processes in the development environment.

Code generators: If a formal modelling language has an executable subset, there is
also potential for automating a part of the coding process. This adds value to the
formal models being produced and thus affects the balance between the effort spent
producing the model and its value as a basis for an implementation. Generated
code will rarely be as efficient as a hand-coded implementation. However, given a
reliable code generator, there is some confidence that the generated code accurately
reflects the properties of the model. Critical applications demand the use of certified
code generators [77]. The use of code generation for production code comes at a
price in terms of the degree of abstraction that can be permitted in the model.
Combination with other notations: It is essential for industrial uptake that a tool for
formal modelling is able to support whatever standards for processes and other
tools are being used. It is even better if users are able to move back and forth
between the various models and notations that are used, seeing updates in model
reflected consistently in others. Considerable work has gone into developing appro-
priate couplings between formal methods tools and UML, the de-facto standard in