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