
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.
- 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.
- 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.
- 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.
- 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.
- 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.
- 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!
Share this article

Learn more about how to develop specifications with Digital Twins
Fill out your information here.
More News & Articles
Explore how Prover is revolutionizing railway signaling with AI and formal methods. Discover Prover Labs: a hub for innovation, collaboration, and shaping AI-driven automation for enhanced safety, efficiency, and precision in signaling design.
Prover introducing Signaling Design Automation to students at CentraleSupélec in Paris.
Prover PSL, the leading model checker used for formal verification in the rail and metro signaling domain, is now even faster.