Formal Verification of Application Code and Relays

The Verifier Module uses formal verification to search for scenarios that cause the Application Code to enter forbidden unsafe states. If an unsafe scenario exists, the tool finds it, generates the corresponding test, and displays it in the debugger. The engineer then pin-points and fixes the unsafe logic, and re-runs Prover iLock Verifier.

The process is repeated until all unsafe logic has been corrected. At this point, the Verifier Module mathematically proves that it is impossible for the Application Code to enter any of the unsafe states specified in the PiSPEC Safety Specification.

This approach is fundamentally different from testing, simulation and review. To test or simulate all possible scenarios and combinations of events is impossible even for small applications. Test methods rely on specifying a (potentially long) list of scenarios to test, typically the scenarios that are expected to occur in operation, and checking that the Application Code copes with those as expected. Whether the operation of the Application Code is safe also for the remaining scenarios remains unknown. The diagram below illustrates the difference in coverage.

With the introduction of Prover iLock Verifier, you no longer have to limit yourself to checking a few scenarios. Prover iLock Verifier proves that the Application Code is safe for all. While new to some, formal verification is a mature and proven verification approach that has been used extensively within the railway, semiconductor, avionics and automotive industries for more than twenty years.

Proof Logging (not available for all targets)

Prover iLock Verifier is the only solution on the market that supports proof logging. During the safety analysis, the tool generates a Proof Log, often several gigabytes large, that can be checked by an independent Proof Log Checker for certification purposes. If no errors are found in the proof log (as is expected), the independent Proof Log Checker issues a Safety Certificate. This approach meets CENELEC SIL 4 requirements for elimination of safety tests, and allows for cost-efficient and independent certification, through Proof Log Checker development.

Unparalleled Capacity & Performance

For Partner Hardware with “verification-friendly” execution model, applications controlling hundreds of train routes may be verified exhaustively in just a few CPU hours. Prover Technology has invested more than 250 man-years of R&D in areas like SAT and BDD-based model- checking, abstraction, simulation, and interpolation. Prover iLock Verifier combines these and other methods with various strengths and weaknesses to ensure unparalleled performance and capacity.