Case study: Paris Metro Signaling System

The developers of this signaling system sought to reduce the separation between trains in the Paris rapid-transit system by 30 seconds, to two minutes. Its developers used formal methods extensively for verification and validation. They were required to convince the RATP (the Paris rapid-transit authority) that the system met safety requirements. This was the first use of safety-critical software in a French railway system. The new system, called SACEM, allows for 60,000 passengers per hour. Its successful deployment has eliminated the need for another railway line (and the associated rail cars and labor), a savings of hundreds of millions of dollars.