The IEC 61508-3:2010 standard for safety-critical embedded software:

• Highly recommends the use of formal modelling to cover software aspects of system safety validation at SIL 4 and recommends it at SIL 2 and SIL 3 (table B.5)
• Highly recommends the use of formal methods for software safety requirements specification at SIL 4 and recommends them at SIL 2 and SIL 3 (table A.1)
• Highly recommends the use of formal design and refinement methods for software architecture design and for software detailed design at SIL 4, and recommends them at SIL 2 and SIL 3 (tables A.2 and A.4)
• Highly recommends the use of formal proof during software verification at SIL 4 and recommends it at SIL 2 and SIL 3 (table A.9)
• Recommends the use of formal verification at SIL 3 and SIL 4 during software module testing and integration (table A.5)
• Recognizes that formal methods provide the highest level of rigour (R3) and therefore the highest level of confidence in the verification results (Annex C)
• Permits software module testing to be reduced in scope when appropriate formal methods are used (section 7.4.7.2 and table A.5 note 3)

How we can help

Perfect Developer supports software specification, architecture and refinement, with formal proof at all levels. In many cases, it can also be used to develop a formal model of the system. This allows you to generate formal proof that the software specification is correct with respect to the safety properties and other functional requirements of the system.

Escher C Verifier (eCv) supports the development of code in MISRA-C (and some C++) 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. By linking the contracts to higher-level specifications, formal traceability between high- and low-level requirements can be demonstrated. Additionally, eCv restricts use of the C language to a safe subset - highly recommended for SIL 3 and SIL 4 (table A.3) - and proves that the software is free from undefined behaviour.

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 SIL 3 and SIL 4 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!