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