Escher Technologies Escher Technologies
Home Tools Services Support News Company Contact Publications Articles
Escher Technologies
arrowEscher Verification Studio
arrowEscher C Verifier
arrowPerfect Developer
arrowEvaluating the tools
arrowWhat others say
arrowCritical embedded software
arrowYour development process
arrowPD and SPARK Ada
arrowSummary of benefits
“Our need is to meet the requirements of defence standard 00-55 to Safety Integrity Level 4.
Escher Technologies software met our requirements best.”

Guy Mason
Senior Software Engineer
General Dynamics UK Ltd.
Perfect Developer - Making software bugs extinct!

Software Development and Verification to
UK Defence Standard 00-56 with Formal Methods

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 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!


Home    TOPTOP
Copyright © 1997-2017 Escher Technologies Limited. All rights reserved. Information is subject to change without notice.      Link to  Privacy/Cookie Policy (new window)