Railway and metro signaling is entering a new era; one defined by openness, flexibility, and collaboration. In June 2025, Prover launched the Open Signaling Initiative, a dedicated hub for the growing Open Signaling Initiative. The goal is simple: empower infrastructure managers, system integrators, hardware and software suppliers, and safety assessors to work together in reshaping how signaling systems are built, operated, and maintained.

With openness at its core, the initiative drives innovation, enhances long-term sustainability, and gives industry players the flexibility they need to meet future demands.

The need for a more open approach

Today, most signaling systems are delivered as closed, monolithic packages. Many infrastructure managers are seeking solutions based on open signaling principles and standardisation. When existing monolithic systems reach end-of-life, they’re often replaced in one costly leap, a practice that has become the industry norm. The result: high expenses and limited flexibility, slowing down innovation.

Historically, signaling systems were built from off-the-shelf components that any qualified engineer could replace or modify. The Open Signaling Initiative restores that openness while embracing the power of modern, computer-based systems.

Principles of open signaling

Already in use across several projects, the open signaling approach is built on three key principles:

• Open interfaces
  Use of standard communication protocols such as OPC UA, MQTT, and EULYNX/RaSTA, along with data formats like railML, to ensure interoperability.
• Loosely coupled components
  Separation of platform and logic allows individual components to be swapped out without affecting the entire system.
• COTS hardware
  Commercial-off-the-shelf platforms offer cost-efficiency and long-term flexibility.

What does it mean for the railway industry?

With open signaling, infrastructure managers can remain in control. They can reduce risk, modernize systems incrementally, and avoid the disruption and cost of “big bang” replacements.

Systems built on open signaling principles deliver:

• Greater flexibility in procurement
• Easier safety assurance through formal verification
• Long-term sustainability through obsolescence management
• A broader ecosystem of suppliers and integrators

Prover’s role

Prover supports the Open Signaling Initiative through tools and processes grounded in formal methods. Our Signaling Design Automation (SDA) process includes:

• Specification writing using formal logic
• Developing application logic directly from verified specifications
• Platform-independent code generation
• Performing formal verification to support your safety case

Our tools meet CENELEC EN 50716/50128 SIL 4 requirements and have been proven in multiple high-integrity signaling projects.

How do I get involved and get the benefits of the Open Signaling Initiative?

Visit the Open Signaling Initiative to explore how the initiative can benefit your organization. Learn more about the approach, see who’s already contributing, and discover how you can take part.

Whether you’re working to modernize aging relay-based systems or developing next-generation technology, your involvement matters. Join us in making signaling more open, collaborative, and future-ready.

Let’s build a more open future together

The Open Signaling Initiative offers a clear roadmap for gradual, controlled change. It’s about creating a signaling ecosystem that’s modular, flexible, and built to evolve – much like modern IT systems. This shift gives infrastructure managers and technology providers greater freedom of choice, encourages innovation, and supports long-term sustainability.

A more open future isn’t just a vision, it’s already in motion.

Discover how you can contribute at www.opensignaling.org.

A part of a modern standard methodology for formal verification is to do reachability analysis. At Prover, we use it as an integrated part of our process to validate requirements and constraints, as well as to find design flaws.

While proof obligations are properties that must always be true (which you are required to prove), reachability obligations are properties that should be possible to make true. They state that there must be a way for the system under investigation to reach a state where they are true. There must not necessarily be one state that makes them all true at the same time (which might be impossible), but rather one scenario per reachability obligation.

Constraints for proof obligations and reachability obligations

For train and metro signaling systems, safety is very important, so proof obligations have been used for a long time: state your safety properties as proof obligations and let a model checker prove that they are always fulfilled by the signaling system. For example, a safety property might say that whenever a train receives permission to proceed (e.g. by a signal or a radio message), all switches in the route must be locked in the correct position. Formal verification is sometimes performed based on assumptions about the environment. Perhaps about the behavior of trains, or about physical equipment such as relays. Such assumptions are added as constraints in the verification model. The name constraints comes from the fact that they can be viewed as constraining the search space for possible states of the system.

Correctly used, constraints exclude non-realistic scenarios and let the model checker focus on realistic scenarios only. A mistake in the formulation of constraints can, however, have very severe consequences. If too many scenarios are excluded, then they will be ignored by the model checker, even if they can happen and would be dangerous.

For reachability analysis, constraints contribute by restricting how reachability obligations are allowed to be reached. The scenario produced will fulfill the constraints. If this is not possible, the reachability obligation is called unreachable.

Ways to find erroneous constraints

There are a number of techniques that help identify erroneous constraints.

1. Bounded Consistency Checks. This technique, usually abbreviated BCC, has been available for a long time. It checks that constraints are consistent, meaning that they are not mutually contradictory. If they are inconsistent, they exclude all possible scenarios, including the realistic ones, which can be dangerous. Though useful, this check is also very coarse. It will only discover if all possible scenarios are excluded, not if some realistic scenarios are excluded. In other words, if the check shows that you have an inconsistency, you need to fix it, but if not, you have no guarantee that your constraints are correct. Realistic scenarios could still be excluded in the analysis.
2. Reachability analysis. You state Reachability Obligations (ROs) that express states that the system shall be able to enter. For example, you can state that every route can be used. The model checker will then try, for each route, to find a scenario that leads to the route being used. If that succeeds, it means that these scenarios can occur, but also that they are not excluded by any constraints. In particular, it follows that the constraints are consistent, so this check says more than BCC. Much more, in fact, because it does not only tell you that there is at least one scenario that is permitted by the constraints, it also tells you that there are scenarios that reach specific, realistic, intended states. You can use these reachability obligations as regression tests, that will tell you immediately if you happen to introduce a constraint that excludes scenarios where routes are used. You can also add reachability obligations for equipment that you know can fail, and where you want to watch that no constraint is introduced that will exclude such failure from the model. For example, you can express “the lamp is turned on by the signaling system but does not acknowledge back that it works” or “the switch is being thrown to the left but not detected in the left position”. If these scenarios are not reachable, it is a clear sign that some constraints are unrealistically strict.
3. Proof coverage. If a proof obligation is surprisingly shown Valid, or a reachability obligation surprisingly turns out to be Unreachable, it can be a sign of the presence of an erroneous constraint or a bad definition. This situation is difficult to debug, because a model checker cannot provide any counterexample to inspect in this case. It can, however, tell you which parts of the model were used when arriving at the conclusion. By inspecting them you might be able to understand where the conclusion came from.
4. Constraints softening. Another technique available to analyze surprisingly Valid proof obligations or Unreachable reachability obligations is to soften constraints. By pointing out constraints that you want to soften, you instruct your model checker to interpret them as soft constraints. Soft constraints are assumptions that are not forced but are rather used as preferences when selecting models. They do not affect truth values of proof obligations and reachability obligations (as proper constraints do); they only contribute to the selection of which scenario to produce as a counterexample for a proof obligation, or as an example for a reachability obligation. We think of them as noise reduction, because they can make models considerably less chaotic, and thus eliminate “noise” that distracts from the important aspects of the model. The model checker will produce a scenario where the soft constraints are fulfilled as much as possible. You can then ask for information about which soft constraints were violated in the model produced. If these violated soft constraints are softened proper constraints, then it’s a good idea to review them thoroughly, because they might be stronger than you intended.

Ways to validate requirements at early stages

Reachability analysis can also be used to validate requirements. In railway signaling projects, an ontology (for example an object model) and safety requirements are usually produced during the tender phase, while the design is made much later. Mistakes in the safety requirements, such as them being mutually contradictory, are important to find early, in order not to base development on faulty requirements that will have to be changed later, causing large extra costs. Tool support for finding such mistakes is crucial.

One option is to model all variables of the ontology (object model) as free variables, and to implement the safety requirements as proof obligations. They cannot be proved until a design is available, and any attempt at proving them will fail with a counterexample, because all design variables are free. What you can do, however, is to assume those proof obligations, that is, using them as constraints, and try to prove some reachability obligations, for example that all signals can clear (not at the same time, but individually). If the requirements are not mutually contradictory, and do not forbid signal clearing directly or indirectly, you will, for each signal, receive a scenario where the signal clears in the end, and where all safety properties are fulfilled in every step. This shows that the requirements can indeed be fulfilled. In fact, by inspecting the scenarios that lead to signals clearing, you should be able to find all steps that you expect to be necessary for the signal to clear, such as switches being thrown to correct positions, objects being locked, and so on. If those steps are not there to find, it might be a sign that some requirements about the missing steps are lacking.

How to do reachability analysis

There are two possible ways to do reachability analysis.

1. Any model checker can be used, if you are prepared to use a workaround. Say that you want to show that a system can reach a state where a lamp becomes lit. You formalize the opposite proof obligation “the lamp cannot be lit” and ask the model checker for a counterexample. If it finds a counterexample, you have proof that it is possible to find a state where the lamp is lit. This approach works but has three drawbacks.
   • It requires a workaround. This is less intuitive and more error prone.
   • It does not handle the potential issue of undefined values. For example, if you try to show that “1/x = 2” can occur for some integer x, you need to search for a counterexample to “1/x ≠ 2”. Actually, for x = 0 this statement is not even well defined, so x = 0 works as a counterexample. But this example does not work well as a reachability proof, because “1/0 = 2” is not true.
   • The interpretation of the results is error prone. You need to remember that some proof obligations are supposed to be falsifiable, and that it is an error if they are valid, because they are formulated as opposite to what you really want to see. This can be confusing and lead to erroneous conclusions.
2. With a dedicated add-on for reachability analysis. The advantages of this approach are:

• • Proof obligations and reachability obligations can be expressed simultaneously and proved simultaneously in one run.
  • Having reachability obligations explicitly mentioned in input files makes them useful as a way to discover if the system becomes over-constrained by mistake (regression testing).
  • Reachability obligations that can be undefined (involving partial functions such as division or arrays that can be out of bounds) are handled differently than with the workaround: reachability means that there is a scenario where these are both well-defined and true in the last state.

Prover PSL 6 comes with an add-on for reachability analysis. It also comes with proof coverage inspection and constraints softening, which were other features mentioned above.

The add-on for reachability analysis is provided for free to our Prover PSL users until March 2025. Try it today and share your feedback!

Experience the power of strategy fusion!

Prover PSL 5.8 introduces strategy fusion, a game-changing feature that allows you to fuse multiple model-checking strategies into one (patent pending). No longer will you need to choose between strategies; strategy fusion blends the strengths of each by running them in parallel, letting them tackle assigned problems effectively as a team. And they become stronger together!

For new users: simplicity meets performance

We’ve crafted a powerful default strategy using Strategy Fusion, perfect for those new to Prover PSL. You don’t need to be an expert in strategy craftsmanship to get started. Simply run Prover PSL without specifying any strategy, and the default will handle most tasks with ease.

For experienced users: enhanced performance

Seasoned users will notice significant performance boosts in both SAT solving and advanced model checking. Prover PSL continues to deliver the best model-checking performance on the market.

Upgrade to Prover PSL 5.8 today and experience model checking with strategy fusion!