Purpose
Formalize and validate a specification of level crossing requirements, using a number of different level crossing configurations, and using formal verification of safety
Client
Infrabel, the Belgian railway infrastructure manager
Signaling system
Computerized level crossing controllers
Formalize and Validate Safety and Design Specifications
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.
Related case studies
In this project Prover collaborated with RATP in creating a formal verification solution to meet RATP demand for safety verification of interlocking software. RATP had selected a computerized...
Class I freight railroad Canadian Pacific (CP) is increasing capacity and consistency in their design and test of interlocking software by using automation tools. In 2010, CP introduced automated...
Stockholm Central and adjacent interlocking systems are based on electro-mechanical relay technology. Swedish Rail requires that the safety of changes made to these interlocking systems is verified using...
How much can you save by implementing Signaling Design Automation?
In this meeting you’ll find out how digital twins and formal methods can help you achieve your rail control projects in less time and lower costs. And 100% secure system.
Purpose
Formalize and validate a specification of level crossing requirements, using a number of different level crossing configurations, and using formal verification of safety
Client
Infrabel, the Belgian railway infrastructure manager
Signaling system
Computerized level crossing controllers
Formalize and Validate Safety and Design Specifications
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.
Related case studies
In this project Prover collaborated with RATP in creating a formal verification solution to meet RATP demand for safety verification of interlocking software. RATP had selected a computerized...
Class I freight railroad Canadian Pacific (CP) is increasing capacity and consistency in their design and test of interlocking software by using automation tools. In 2010, CP introduced automated...
Stockholm Central and adjacent interlocking systems are based on electro-mechanical relay technology. Swedish Rail requires that the safety of changes made to these interlocking systems is verified using...
How much can you save by implementing Signaling Design Automation?
In this meeting you’ll find out how digital twins and formal methods can help you achieve your rail control projects in less time and lower costs. And 100% secure system.
+46 (0)8 617 68 00