Formalize and Validate Safety and Design Specifications
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.