Prover Certifier

Formal Verification for CENELEC Certification

Prover Certifier is the only software product on the market that allows you to automatically produce complete safety evidence for CENELEC EN50128 SIL 4 certification using formal verification. Rather than spending resources on time-consuming tasks such as manual reviews and safety testing, you let Prover Certifier construct a formal correctness proof of your system.

Not only is the proof completed in a fraction of the time it takes to produce traditional safety evidence, it also provides 100 % coverage as formal verification is guaranteed to discover every error, even those that are extremely hard to find by testing. Since Prover Certifier has been carefully
developed in a CENELEC SIL 4-compliant process, its judgment can be fully
trusted and can replace other evidence.

There is no need to perform extensive reviews and safety testing anymore, so you save both time and costs, and minimize the risk of human error in the review process. Your system will be taken into revenue service much earlier and you can be certain that it will always be safe.

Applications

Prover Certifier provides certifiable safety verification for a wide range of systems, including:

  • Communication-Based Train Control (CBTC) systems
  • European Rail Traffic Management Systems (ERTMS)
  • Railway interlocking systems

Features
  • Independent and certifiable formal safety verification of high-level design as well as implementation code languages
  • CENELEC SIL 4 compliance based on techniques such as diversification, proof logging and proof checking
  • Mature and proven formal verification technology


Prover Certifier Generic Flow

The high-level design of the system is translated into a Design Model that can be used as input to Prover Certifier. The software code on the other hand is translated into a Code Model. The translators are developed by independent teams applying CENELEC SIL 2 standards, thus forming a diversified solution which is sufficient for higher levels (including SIL 4). The two independently produced models are equivalence-checked by Prover Certifier, which also formally verifies that all safety requirements are met.

The CENELEC standards

The development of safety-critical systems is surrounded by rules and regulations whose purpose is to ensure extremely low risks for residual safety issues. The concept of Safety Integrity Level (SIL) of the CENELEC standards EN50126, EN50128 and EN 50129 is a measure of the level of safety required. The higher the level, the stricter the requirements on the development process. SIL 4 is the highest safety integrity level specified by the standard.

This standard's approach for certification focuses on ensuring that the code is correctly produced from a functional specification that has been shown to be safe. The Prover Certifier approach is based on verifying that the produced code is safe, and imposes CENELEC SIL 4 requirements on the software which performs this verification. In other terms, the certification task is delegated to a formal verification process which has at least the same SIL classification as the code.


Contact Prover