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!

Embedded Software Development and Verification to IEC 61508
with Formal Methods

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


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)