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
MORE ABOUT FORMAL VERIFICATION
Increased railway safety using signaling design automation
In this, the third and final, blog post on Signal Design Automation we will look at how Formal Verification and automation are used at Stockholm Metro to increase railway safety. [...]
Webinar: Formal Verification a solution for railway safety
We have now published a new date when we will run our popular webinar about Formal Verification. The date for the webinar is the 28th of April. Safety verification is [...]
Floating Point Model Checking Put to the Test
In a previous blog post, a playful concrete example was given to show off PSL's newly added support for IEEE 754 floating point calculations. We have tested the performance in [...]
Why Formal Verification – The Solution to the Verification Problem
If you have read the first two parts of this series (Read Part 1 here and Part 2 here), then you know that verifying an interlocking that satisfies safety requirements [...]
Why Formal Verification – The Suitability of Formal Verification
Hopefully you have read part 1 on this blog, where I tried to convince you that traditional methods will not get you very far when verifying safety requirements for railway [...]
Why Formal Verification – Verifying Safety Requirements on Railway Systems
The subject I am going to write about this time is not an easy one. I will try to explain why formal verification is good. In particular, why it is [...]