Integrating Formal Methods: The SPECTRUM Projectby 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