CARE - formal development of high-integrity software

As computer-controlled systems become more pervasive in society, it is increasingly important to be able to assure their correctness, particularly in safety-critical areas such as aviation, railways and health. CARE is a technology for developing trustworthy software of the highest possible assurance: it provides a means for proving correctness, which significantly increases assurance compared to testing alone.

Software is increasingly being used in safety-critical devices such as implantable defibrillators.

CARE is a software development method and toolset that supports the generation of formally verified software from formal specification. Formal verification of software is often regarded as a difficult, time-consuming task requiring esoteric mathematical skills. CARE aims to bring formal verification within the reach of software engineers trained in formal specification, without requiring them to be experts in formal mathematics.

The CARE process for developing formally verified software.

CARE is Computer Assisted Refinement Engineering.

The use of CARE begins after system requirements have been defined and analysed for criticality, and after software requirements have been mathematically modelled by writing a formal specification. Starting with the formal specification, software engineers use CARE to develop compilable code, with integrated checking that the code is provably correct. The process of developing software using CARE involves selecting `refinements' from a library of pre-proven `templates' and adapting them to suit the problem at hand. A substantial library of basic refinements is supplied with the CARE toolset.

The CARE approach is thus analogous in many ways to electronic engineering: library fragments correspond roughly to integrated circuits which are designed and verified by a small group of specialists, while another, larger group of users selects those circuits from data-books and combines them into products.

• Overview of the CARE method and toolset
• Recent CARE papers
• Collaboration with Telectronics

For more information, email Peter Lindsay