Formal verification tools certified for rail control

We are happy to announce that Prover Certifier has received its CENELEC EN 50128, tool class T2 certification from TÜV Nord!

Prover is the leading provider of formal verification solutions for automation of safety verification and assessment tasks for rail control software. The formal verification tool PSL uses mathematical algorithms to prove, with 100 % coverage, that the system fulfills its safety requirements. For requirements that are fulfilled it produces a proof log that can be checked with the sign-off verification tool Prover Certifier. For violated properties it produces a counterexample and provides powerful built-in debugging aid.

The prevailing international standard for development of safety critical rail control software is CENELEC EN 50128. Prover’s formal verification solutions are developed according to this standard, making it possible to base a SIL-4 safety case of your software on formal verification. As the formal verification is fully automated, and gives 100 % coverage, this will reduce the cost for the safety assessment at the same time as it increases the confidence of the safety.

PSL and Prover Certifier are key parts of the Prover Trident design automation solution for requirement specification, configuration, design, implementation, functional testing, and safety verification of rail control software. PSL and Prover Certifier have successfully been used by leading rail control suppliers and infrastructure managers for the SIL-4 safety assessment of a large number of rail control projects.

To simplify the use of formal verification in safety assessment and to reduce the effort for the approval of such processes, Prover is working with TÜV Nord to provide certification of that the tools fulfill the relevant requirements of CENELEC EN 50128. Prover Certifier has now received this certification for tool class T2 from TÜV Nord. This is just the beginning, and more certifications are planned for the near future!