Integrating Formal Methods: The SPECTRUM Project
by Juan Bicarregui
Formal methods of software development offer the opportunity of improved
software quality, but their uptake is hindered by the diversity of competing
methods. The Vienna Development Method (VDM) and the B Method are two formal
methods currently in use by industry and supported by mature commercial
tools. These methods are essentially similar, but the coverage of the tools
for VDM and B differ significantly in their capabilities for static analysis,
proof, animation and code generation. This complementary functionality
could benefit users from both communities, but because of the differences
between the methods such cooperation is not currently possible.
The SPECTRUM project brings together suppliers and users of the VDM
and B toolkits to investigate the feasibility of integrating support for
these two formal methods. By doing this, a design given in one notation
could switch to the other for part of the design, exploiting the strengths
of each method for different phases of the design process. Further, the
facilities of both tools will be available from either notation.
The approach adopted in SPECTRUM centres on determining the commonalties
between the VDM-SL and AMN notations, via the development of translations
between them. From this common core should emerge common techniques for
modularisation and proof construction that will support the analysis and
automation tasks.
The user partners in SPECTRUM represent a cross-section of safety-critical
applications in avionics, terrestrial transportation, satellite control
and nuclear power. The potential of using the combination of methods within
a commercial software development process is being investigated via case
studies in these application areas. It is anticipated that advantages in
terms of development cost and product quality can be gained from using
the SPECTRUM technology.
The tool suppliers are assessing the commercial case for the provision
of the required functionality. The long term aim of the SPECTRUM programme
is to integrate the two toolkits so that the benefits of both can be gained
from either. More information on the SPECTRUM project at: http://www.dci.clrc.ac.uk/Projects/Spectrum/
Please contact:
Juan Bicarregui - CLRC
Tel: +44 1235 446380
E-mail: J.C.Bicarregui@rl.ac.uk
