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.
Share this article
Learn to build a solid safety case for rail control systems using formal verification
Fill out your information here.
More News & Articles
Prover uses formal methods to make railway signaling provably safe. Our solutions build safe, reliable, and cost-efficient systems that move and protect millions of passengers every day. Through our Open Signaling Initiative, we're reshaping how the industry builds and maintains signaling systems across Europe and beyond. Now we're looking for someone to join us and bring AI, LLMs, and agentic workflows into the heart of how we work and what we build.
Meet Prover at RailTech Europe in Utrecht, March 4–5. Visit Booth 2.509 and join our workshop on migration of signaling systems to PLC-based SIL 4 solutions.
We are seeking an Office Coordinator to our Stockholm office.
The Office Coordinator plays a key role in ensuring that our office operates efficiently and in line with Prover’s standards of professionalism and quality. The role combines office management with broad administrative support to management and staff.
