Formal Verification

Prover provides tools and services for Formal Verification.

enablING 100% Certainty THROUGH MATHEMATICAL PROOF

What is Formal Verification?

Formal Verification is a technique to ensure systems fulfil selected properties with 100% certainty. For example, for a rail control system, it can be checked that signals cannot display green aspects unless certain switches are in correspondence.

While testing of big systems can never reach full coverage due to the number of combinations that would have to be tested, this method provides full certainty because it uses a mathematical argument without gaps. It is precise, unambiguous and covers 100% of the domain under investigation.

Formal methods

A requirement in railway safety assessment

Several infrastructure managers now require Formal Verification as part of the railway safety assessment. Even when not required, suppliers now choose to do it because of the increased safety and the possibility of decreasing testing by finding issues with automated techniques.

What is needed for you to get started?

Two kinds of expertise are needed to successfully deploy Formal Verification as a methodology: Expertise in Formal Verification and expertise in railway control systems. With our help, tools and guidance, any company can set up and deploy formal safety verifications.

Formal Verification since 1989

Prover has performed Formal Verification for almost 30 years of relay-based interlockings, computer-based interlockings (such as Siemens Westrace, Ansaldo Microlok, Alstom iVPI, GE ElectroLogiXS, SCADE-based designs etc), CBTC systems, ETCS systems, micro processors, embedded systems in cars, and more.

Prover provides products, training and support to set up your own team and process. We will support you during the introduction and assist if expert services are needed.

Formal Verification as a service

Should you prefer to buy Formal Verification as a service, Prover will provide you with that. Our experienced and highly skilled professional services team will then formally verify your system using a set of our products tailored to your needs. Any violations of railway safety requirements are then reported to you, along with the causes. Read more about our services.

Our services

Our products portfolio

Prover iLock®: railway interlocking simulator, document & code generator, and verifier
Prover Certifier: CENELEC SIL-4 certifiable safety evidence generator
PSL: model checker capable of formally verifying big industrial systems
SCADE FV: CENELEC SIL-4 formal verification of systems built with SCADE

How to build a solid safety case for your rail control system using Formal Verification

Download guide

References

Prover’s innovative solution bring benefits to many types of Rail Control Projects.

View all

Implementing Prover Trident for SL, Stockholm
In signaling design automation projects, we start by developing a digital twin of your existing, future, and conceptual systems.
Our Formal Verification Solution for RATP, Paris
In this project Prover collaborated with RATP in creating a formal verification solution to meet RATP demand for safety verification of interlocking software. RATP had selected a computerized...
Implementing the Prover iLock tool-suite for Canadian Pacific
Class I freight railroad Canadian Pacific (CP) is increasing capacity and consistency in their design and test of interlocking software by using automation tools. In 2010, CP introduced automated...

View all

SOFTWARE SOLUTION

Prover Certifier – Ensure railway safety with 100% certainty

The only sign-off verification tool on the market that allows you to automatically produce complete safety evidence using formal verification.

To Prover Certifier

How much can you save by implementing Signaling Design Automation?

In this meeting you’ll find out how digital twins and formal methods can help you achieve your rail control projects in less time and lower costs. And 100% secure system.