Formal Verification
Formal Verification as a Service
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.
Prover has performed formal verification 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.