Infrabel, Belgium

Formalize and Validate Safety and Design Specifications

Purpose

Formalize and validate a specification of level crossing requirements, using a number of different level crossing configurations, and using formal verification of safety

Infrastructure Manager

Infrabel, the Belgian railway infrastructure manager

Signaling system

Computerized level crossing controllers

In this project, Prover Technology provided tools and services to help Infrabel increase the quality of requirement specifications for tendering of 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 risk of delays in delivery of computerized rail control. Infrabel selected Prover Technology 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.