RATP operates one of the most important multimodal transportation networks in the world. When the first software-based train control system was deployed on this network at the end of the 80’s, RATP has experienced the use of formal methods to master the safety critical part of the software. Since then, RATP has developed, improved and promoted the use of formal proof for validation or assessment purpose, aiming to extend its scope. The next step is the application of formal proof at system level for the demonstration of railway systems safety by using a composite methodology combining top-down and bottom-up approaches.
