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
The CBTC User Group – discussing the CBTC signaling systems of today and tomorrow
Together with the metros of Copenhagen (Metroselskabet, MS), New York City (New York City Transit, NYCT) and Stockholm (Storstockholms Lokaltrafik, SL), Prover has founded the CBTC user’s group to [...]
Verification of Safety Requirements
There are two main kinds of accidents that are worth worrying about: collisions and derailments. An interlocking is safe if it prevents such accidents from happening. Of course, an [...]
Why the railway industry needs to modernize its methods of safety assurance
For the next big advancement in the development of faster and more efficient transportation, the railway industry has to go through a digital transformation. For this, safety is critical. [...]
Model Based Development Webinar with Ansys
Study our recorded webinar with Ansys Together with Ansys, we held a webinar on Formal Verification for Model-Based Development. Prover supplies the model checker PSL, which powers Ansys new SCADE [...]
Save the date – SDA Forum in Paris March 23rd
2017 an idea was born at Prover Technology. We wanted to create a forum for sharing experiences, best practices, and for networking. Our intention was to gather leading signaling management [...]
HLL crash course for Safety Engineers
Beginning May 18th, I led a four-day online crash course on HLL for a dozen Safety Engineers. Due to the French COVID-19 lockdown, the course was conducted via Microsoft Teams, [...]