Formal Engineering of Software at RAL
by Brian Matthews and Brian Ritchie
The complexity of software increases all the time, with more and
more tasks, many of them critical to the well-being of people, entrusted
to computers. As this dependency increases, it becomes vital that software
is well engineered to ensure that it behaves as intended, without leading
to potentially dangerous situations. Structured and object-oriented methods
have provided such engineering. However, as complexity and trust continue
to rise, these techniques reach their limits in ensuring correctness.
Formal methods of software engineering are advocated as a means of providing
a higher level of confidence in the correct functioning of software. Formal
methods use the rigour of mathematical notations to unambiguously specify
the behaviour of software; formal proof using mathematical logic to demonstrate
the correct behaviour; and mathematical relationships to convert those
specifications into programs while preserving correctness.
However, the acceptance of formal methods has been limited. Formal methods
are seen as too academic, too hard to learn and use, and too expensive.
Tool support is essential to manage the methods accurately, and this has
not been available. Consequently, formal methods have been seen as not
proven by industry, resulting in a vicious circle, as lack of uptake leads
to lack of development of the technology.
In the past ten years, RAL has been involved in a series of projects
to develop formal methods technology and to encourage its commercial uptake.
In this article, we give an overview of this activity.
MURAL
Between 1986 and 1992, RAL developed the Mural system with Manchester
University. The main objective was to support formal reasoning to verify
the internal consistency of specifications, and to validate a formal specification
against an informal description of the system, by proving properties which
it should exhibit. To this end, a generic proof assistant was developed.
RAL provided a support tool for the Vienna Development Method (VDM),
one of the most mature formal methods. This allowed the development of
VDM specifications, the generation and proof of obligations showing the
specification's correctness, and the formal development of refinements.
Mural was an important experiment in developing support tools for formal
methods, including proof tools, and user interfaces.
BUT
The B Method is another formal method which is being advocated for industrial
use. Between 1992 and 1994, the B User Trials project, involving RAL, Lloyds
Register of Shipping, Program Validation Ltd, and the Royal Military College
of Science, investigated B and its tool support in industrial case studies
and accompanying technological assessments. These sought to expose B to
real technical challenges to test its applicability. The project also developed
training material for the B Method.
RAL used a case study from the standardisation of the Graphics Kernel
System to compare B with the similar methods VDM and Z. Also, the support
for proof provided by the B-Toolkit was assessed.
The project determined that the B-Toolkit was indeed a practical for
industrial usage, with powerful support for development in the large, through
its module system, and for development of code, through formal refinement
and code generation. However, B is weaker at requirements capture, being
biased towards a "programmer-centred" algorithmic style.
MaFMeth
The team at RAL took this experience into the MaFMeth project, a European
ESSI application experiment with Bull S.A, and B-Core UK Ltd, active in
1995-1996. The objective was to give a complete formal development of part
of a real high-integrity system, taking measurements to evaluate the approach's
effectiveness.
The project took a formal development path which combined VDM and B,
using each where they have strengths: VDM for high-level requirements and
design; B for refinement and generation of code. This mixed approach allowed
the use of tools available for both languages, subjecting the development
to many analyses.
This approach proved successful. A statistical analysis of the results
showed that fewer errors resulted in the formal development compared with
a conventional development, and those errors were discovered earlier. However,
difficulties were introduced when (informally) moving between notations.
SPECTRUM
The idea of using VDM and B together led to the SPECTRUM European feasibility
study in 1997, with partners GEC Marconi, Dassault Electronique, Commissariat
à l'Energie Atomique, Space Software Italia, Institute of Applied
Computer Science (IFAD), and B-Core UK Ltd. SPECTRUM investigated the feasibility
of formally integrating the VDM and B methods and tools, to gain the advantages
identified in MaFMeth, without the problems. This results in an enhanced
integrated method covering the whole development lifecycle.
Case studies in using the combination of VDM and B in the safety-critical
domains of avionics, railways, nuclear power, and satellite control were
undertaken. In these studies, a design lifecycle has been identified which
exploits the interoperation of the methods to their best advantage, and
allows users to use the integration in different ways. The formal integration
of the two languages was sketched via translations, and shown to be sufficient
to support the integration of the tools. A market study was undertaken
to show the benefit of integrated method to the user partners and industry
at large. It is hoped to continue this work in the future.
Conclusion
RAL has thus played an active role in transfer of formal methods technology
into industry, both in the development of tools and in trials with industrial
partners. This work is continuing, including building on SPECTRUM, investigating
the formal underpinnings of the combined method, together with Imperial
College, London. Work is also branching out in other directions, for example,
collaboration is ongoing with IEI-CNR on using B to support the formal
development of databases. For more information on the web, see http://www.dci.clrc.ac.uk/ListActivities.asp?CLASS=4;CLASSTYPE=13
Please contact:
Brian Matthews and Brian Ritchie - CLRC
Tel: +44 1235 44 6648
E-mail: B.Matthews@rl.ac.uk,
B.Ritchie@rl.ac.uk
