Formal Verification

Prover provides tools and services for Formal Verification

What is Formal Verification

Formal Verification is a technique to check that systems fulfill 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, formal verification provides full certainty because it uses a mathematical argument without gaps.

Several infrastructure managers now require formal verification to be done as part of the safety assessment. Even when not required, suppliers now choose to do formal verification because of the increased safety and the possibility to decrease testing by finding issues with automated techniques.

What Prover Can Offer You

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 in order for you to set up your own team and process to do formal verification. We will support you during the introduction as well as be there all along if expert services are needed.

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 perform formal verification of your system using a set of our products tailored to your needs. Any violations of safety requirements are then reported to you along with what the causes are.

Prover’s Products

Prover’s line of formal verification products is extensive and ever-growing to go above and beyond the industry standards. Check out the following list of our latest products to see what intrigues you:

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
Prover Extractor: creates and verifies databases from Microstation drawings
Prover Trident: complete process and tool suite for interlocking design automation

SCADE FV: CENELEC SIL-4 formal verification of systems built with SCADE
LCF: domain specific language tailored for signaling engineering
PiSPEC: formal language dedicated for signaling engineering
HLL: formal high level language that includes predicate logic and supports important common programming features such as arrays and numbers