Formal verification for Infrabel, Belgium

In this project, Prover provided tools and services to help Infrabel increase the quality of requirement specifications for tendering level crossing systems. Infrabel was preparing to replace about 800 relay-based level crossings with computerized controllers. Due to the safety-critical nature and the complexity of the requirement specifications for these systems, Infrabel decided to perform requirement validation to detect and eliminate specification errors and ambiguities. The purpose of this was to supply increased quality in specifications to suppliers, and thereby reducing the risk of delays in the delivery of computerized rail control. Infrabel selected Prover to do the formal validation of requirement specification, with a technical solution based on;

• Safety requirements formalized in the PiSPEC language
• Design requirements formalized in the PiSPEC language
• Prover iLock tool suite for configuration of level crossing applications and safety verification of the applications

In total 54 families of level crossing configurations were specified (27 with barriers and 27 without), made subject to formal verification of some 119 safety requirements. This helped uncover unexpected behaviour in the level crossing requirement specification and enabled correction and update of the requirement specification prior to the tendering process.