The ISO 26262-6:2011 standard for automotive software product development:

• Recommends that formal or semi-formal notations are used for software architecture design, particularly at ASIL B, C and D (table 2)
• Encourages the use of formal verification to verify the software architecture design at ASIL C and ASIL D (table 6)
• Recommends the use of prototype generation to verify the software architecture design (table 6)
• Recommends that formal or semi-formal notations are used for software unit design, particularly at ASIL B, C and D (table 7)
• Encourages the use of formal verification to verify the software design and implementation at ASIL C and ASIL D (table 9)

How we can help

Perfect Developer supports software specification, architecture and refinement - with formal proof at all levels - and prototype generation in C++. Depending on the application, it can sometimes 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.

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 serve as low-level requirements - are mathematically proven to be honoured by both caller and callee. 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 as recommended by ISO 26262-6 (table 1).

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 formally-verified ASIL C and ASIL D software.

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!