Prover Technology has announced that Infrabel, the Belgian railway infrastructure manager, has placed an order for using Prover iLock for validation of level crossing control requirements.

The Belgian railway network is one of the busiest in Europe, with more than 1,800 level crossing systems. Infrabel chose Prover iLock in order to validate the requirement specifications for new, computerised level crossing systems. Requirement validation detects specification errors and ambiguities, enabling improved quality of requirements specifications and reducing the risk of delays in delivery of computerised rail control.

As part of the order, Prover Technology will formalise Infrabel’s level crossing requirements in the formal specification language PiSPEC, and perform requirements validation using the Prover iLock software tool suite.

Requirements validation with Prover iLock

Based on design, test and safety requirements defined in the formal specification language PiSPEC, the Prover iLock tool suite offers efficient support for requirements validation based on functional simulation and formal safety verification.

The use of formal verification for safety assessment is required by leading railway infrastructure managers, and highly recommended by standards such as CENELEC EN 50128. The reason: formal verification can establish that a rail control system is safe in all possible situations that can arise, as opposed to traditional and time-consuming methods based on test and review.