Automated formal safety verification on the desktop

Prover iLock Verifier provides efficient formal verification of safety requirements against system designs created in Prover iLock.

Formal verification is based on automatic proof search, and provides 100% verification coverage against forbidden, unsafe states: if the system under verification would allow any state that violates a safety requirement, Prover iLock Verifier detects and reports this as a counter example.

The built-in debugger provides efficient support for identifying why the system allows entering a forbidden, unsafe state.

Formal verification is strongly recommended for safety verification by standards such as CENELEC EN 50128. Prover iLock Verifier provides easy-to-use formal verification with high speed and capacity, ensuring predictable formal verification results for your interlocking systems.

Formal verification compared to testing and simulation

Formal verification is a fundamentally different verification approach compared to testing and simulation; to simulate all possible scenarios and combinations of events would be impossible except for the smallest of systems.

Testing relies on specifying a (potentially very long) list of test cases to simulate, and checking that the system behaves safely in each simulation trace. However long the list is, the coverage typically remains very close to 0%, due to the very large number of possible states in a system. The diagram below illustrates the difference in coverage.

Proven formal verification technology with unparalleled capacity & performance

Prover iLock Verifier is based on the market leading technology for safety verification of critical embedded systems, which has been proven by use in industries such as avionics, Electronic Design Automation, automotive and railway signaling.

Prover iLock Verifier provides the speed & capacity required to provide exhaustive formal verification of some of the largest interlocking systems in the world in just a few hours of CPU computation time. Prover Technology has invested more than 250 man-years of R&D in formal verification technology such as SAT-based model checking, abstraction, and interpolation. Prover iLock Verifier combines such verification methods with various strengths and weaknesses to provide unparalleled performance and capacity.