Software Development and Verification to ISO 26262
with Formal Methods
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!