Modernizing the Signaling System of New York City Subway

The subway of New York is one of the busiest in the world, with close to six million riders on an average weekday, but it is also one of the oldest, and in large its signaling system is way past its normally expected life time. An outdated signaling systems brings delays to the traffic since it will fail more frequently, but it also adds to the overcrowding of the subway by not making the most efficient use of the existing infrastructure. With a modern signaling system, you are able to run the trains closer together, thus increasing the potential traffic volume.

The Metropolitan Transportation Authority (MTA), is well aware of this, and have begun to replace this signaling system with a state of the art Communications Based Train Control (CBTC) system. However, the challenges faced when making upgrades to a subway network that is operating 24/7 with millions of riders depending on its availability are immense, and it is difficult to move quickly enough with this urgently needed signal upgrade. The New York times recently posted a very insightful article on this matter: Key to Improving Subway Service in New York? Modern Signals.

Another concern when modernizing any signaling system, and in particular one as complex and high profile as this, is of course to maintain the highest level of safety, or in some cases to even improve it. For MTA one part of this is related to adopting state of the art developing methodologies for software controlling the signals, including the use of formal verification techniques to prove the absence of logical errors in the system. This is not only necessary to guarantee the safety, but also to speed up the safety assessment process which often is a major bottleneck in the commissioning of a new signaling system.

Prover has been working with the team responsible for the vital safety assurance for the subway signaling systems at MTA for a number of years, to define a precise set of safety principles that all new computer-based interlocking systems shall meet. These requirements have been formalized in the PiSPEC language, and the software of each commissioned system is verified against these requirements using Prover iLock Verifier, as part of the independent safety assessment.