UK Defence Standard 00-56 Issue 4 requires that the safety cases for the types of military equipment it covers are supported by evidence. Analytical evidence should provide the primary argument (part 1, section 11.3.1.2). The associated guidance (part 2, section 17.2.1) specifies that analyses should be rigorous and automated where possible.

DefStan 00-56 does not provide detailed guidance on constructing software safety cases. Where there are comparable civilian applications, common practice is to seek guidance from the appropriate civilian standards such as IEC 61508 and DO-178C. Otherwise, Defence Standard 00-55 issue 2 (which was technically superceded when 00-56 issue 3 was released) is often used. There are currently plans for a new issue of 00-55.

DefStan 00-55 issue 2 specifies that the software development process should include formal methods of software specification and design, structured design methods, static analysis (including semantic analysis), and dynamic testing. At lower SILs some of these techniques may be omitted if appropriate justification is provided; however formal specification is mandatory at SIL 3 and SIL 4, and semantic analysis is mandatory at SIL 4.

How we can help

Perfect Developer supports software specification, architecture and refinement - with formal proof at all levels. It therefore covers the rigorous analysis requirements of 00-56 at the specification, architecture and design levels. In many cases it can also be used to develop a formal model of the system, allowing you to generate formal proof that the software specification is correct with respect to safety properties and other systel-level functional requirements. It has been used successfully to express software specifications and develop formally-verified software designs in accordance with DefStan 00-55 SIL 4.

Escher C Verifier (eCv) supports the development of code in MISRA-C (and some C++, if desired) using the Verified Design-by-Contract paradigm. The contracts - which express the low-level requirements - are mathematically proven to be honoured by both caller and callee. In this way, eCv covers the rigorous analysis requirements of 00-56 at the implementation level as well as the semantic analysis requirements of 00-55. By linking the contracts to higher-level specifications, formal traceability between high- and low-level requirements can be demonstrated. Naturally, eCv also proves that the software is free from undefined behaviour, and enforces use of a safe subset of C (part 1, section 28.4 of DefStan 00-55).

Escher Verification Studio delivers both Perfect Developer and Escher C Verifier in a single product, providing the means to generate formal proof of correctness at all levels, making it ideal for developing safety-critical defence software. Alternatively, where Ada is the implementation language of choice, Perfect Developer can be paired with the SPARK Ada tools.

Both Perfect Developer and Escher C Verifier produce detailed proof traces and a verification summary report, for use as evidence when seeking certification. By generating proofs automatically, Perfect Developer and Escher C Verifier make the production of formally-verified software quick and economical.

Interested? Contact us for further details!