Patterns for external behaviour and safety
7.2 Patterns for safety properties
7.2.2 Patterns for safety properties extracted from the train route table
This section will focus on safety properties that can be checked for bothrandom andordered track relay behaviour. These properties are derived from train route tables. After having introduced the properties, it will be analysed whether these properties ensure safety. The properties will be formulated in such a way that the train positions fromordered track relay behaviour are not required.
Further information on train routes and train route tables can be found in section 2.4.
7.2.2.1 Locking of conflicting routes
As mentioned in section 2.4, a train route table specifies the routes that are considered as being conflicting. Therefore, it is relevant to verify that conflicting train routes are never locked at the same time.
Having a train route locked is usually indicated by having some points in a certain position combined with having a steel core relay in a certain state.
Therefore, one can tell whether a given train route is locked by examining the state of the interlocking system.
Suppose thatL1is true when a specific train route,TR1, is locked. Furthermore, assume that train route TR2 is locked when L2 is true and train route TR3 is locked when L3 is true. That TR2 andTR3 are never locked when TR1 is locked can then be formulated in the following way:
7.2 Patterns for safety properties 130
ltl assertion
[ notT2orT3WhenT1 ] InterlockingSystem` G(L1⇒ ∼(L2∨L3))
7.2.2.2 Signals
Train route tables specify that some conditions need to be fulfilled when chang-ing the entrance signal of a train route to adrive aspect. These conditions can be found in a train route table. For instance, when an entrance signal allows a train to approach a station, the condition for letting a train enter one of the routes that go past the signal must be fulfilled. These conditions are:
• A train route that uses the train as an entrance signal is locked.
• The points are in the legal position for the locked train route.
• The track sections specified for the locked train route are free.
• The signals display the aspects specified for the locked train route.
For a given station, assume that we have a signalA and two entrances routes, TR1 andTR2, that go pastA. Suppose thatCTR1 andCTR2 are the condi-tions for entering TR1 andTR2 respectively.
IfaGreenis the relay that is drawn whenAallows trains to enter the station, the following assertion expresses that Awill only allow trains to enter the station when the conditions for doing so are fulfilled:
ltl assertion
[ enterFromAWhenSafe ] InterlockingSystem` G(idle∧aGreen⇒CTR1∨CTR2)
The formula states that if signalAis green in an idle state, one of the conditions CTR1 andCTR2 is true.
7.2.2.3 Stop fald
A train route table specifies when the entrance signal of a given train route should stop displaying adrive aspect. Suppose that signalAfrom the previous
7.2 Patterns for safety properties 131
section must stop displaying a drive aspect when trackT (monitored by track relay t) is occupied. The following assertion expresses that the signal stops displaying adrive aspect when the given track is occupied:
ltl assertion
[ stopFallA ] InterlockingSystem` G(idle∧ ∼t⇒ ∼aGreen)
It is necessary to add idleon the left-hand side of implication in order give the system time to respond to the occupation ofT.
7.2.2.4 Point positions
It is relevant to verify that if a train route is locked, the points of this train route are in the position specified for it.
SupposeLis the condition for having a train route locked andCP is true if the points associated to the given train route are in the acceptable positions defined by the train route table for the given train route. The following assertion will then express that the points are in the right position when the route is locked:
ltl assertion
[ pointsInPositionWhenLocked ] InterlockingSystem` G(L⇒CP)
In that way, a train following the train route will not derail if the route remains locked until the train has passed the point. However, the formula in itself is not enough to ensure that derailing does not take place. If the route is unlocked before a given train has passed the point, one cannot be sure that the point does not switch position before the train has passed it.
7.2.2.5 Train route release
As mentioned before, if a train is following a train route and the train route is unlocked before the train reaches the end of it, a point of the train route might be switched before the given train has passed it. In other words, if the train route is unlocked too early, derailing might happen. This section will introduce
7.2 Patterns for safety properties 132
patterns that can be used for model checking that a given train route remains locked long enough.
Figure 7.10: Scenario: locking of a train route under random track relay be-haviour. The conditions Release 1 and Release 2 are used to check that the route is not released too early.
A train route table establishes when a train route is to be released. Usually rules for releasing train routes specify conditions on the occupation of two track circuits. Suppose the involved track circuits are T1 and T2. The following states can then be used to specify the rule for unlocking the train route:
• State 1: T1 is occupied andT2 is free.
• State 2: T2 is occupied andT1 is free.
An example of a rule can then be that a given train route must not be unlocked unlessstate 1 occurs at some point and thatstate 2 occurs at some point later before the route is unlocked.
7.2 Patterns for safety properties 133
A scenario using random track relay behaviour in which a train route becomes locked and unlocked can be seen in figure 7.10. As seen in the scenario, the route remains locked until state 1 and state 2 have happened in the order specified by the rule. The patternstate 2 eventually followed bystate 1 is observed, but the release does not happen before the pattern state 1 eventually followed by state 2 is observed.
For checking that the unlocking does not happen too early, we will introduce twoLTL assertions.
SupposeL is the condition for having the train route in figure 7.10 locked and t1 andt2 are the track relays monitoringT1 andT2.
The following assertions can then specify that the train route is not unlocked beforestate 1 has occurred:
ltl assertion
[ release1 ] InterlockingSystem`
G(∼L∧X(L)⇒X(W(L, L∧ ∼t1∧t2)))
release1 is illustrated in figure 7.10. When the train route is unlocked in the current state and locked in the next state, it should hold that, from the next state, the route must remain locked until state 1 occurs and that the route is still locked in that state. The boxes marked Release 1 indicate that the weak until operator ensures that the route remains locked untilstate 1.
The second assertion is:
ltl assertion
[ release2 ] InterlockingSystem` G(L∧X(∼L)⇒t1∧ ∼t2)
release2 is also illustrated in figure 7.10. When the train route is locked in the current state and unlocked in the next state, we have state 2. The box markedRelease 2 indicates if the assertion applies to the state before the route is unlocked.
Together the two rules specify that if the train route becomes locked at some point, state 1 must happen before the unlocking of the route and that if the unlocking happens, we havestate 2.
7.2 Patterns for safety properties 134
7.2.2.6 Indirect verification of basic safety goals
We have now introducedLTL assertions for expressing that:
1. Conflicting train routes are not locked at the same time.
2. The signals can only allow the trains to pass them if the conditions for doing so are true. Such conditions are given by the train route tables.
Some signals must display some specific aspects, some points need to be in a specific position, some track circuits need to be free, combined with having a train route locked.
3. A signal displaying adrive aspect changes tostop aspect when a specific track section is occupied.
4. The points are in the required position by a train route as long as the train route is locked.
5. A train route is not released too early.
One can notice that property 3 is included in property 2. Property 2 states among other things that a signal cannot display adrive aspect if a track in the train route is occupied. This includes the track which is referred to by property 3.
Neither of these properties will alone ensure the overall basic safety goals. The interesting question is then whether a combination of these ensure that neither collision norderailing take place.
To ensure that collisions do not take place, the following needs to be verified:
• Conflicting train routes cannot be locked at the same time: prop-erty 1 will ensure this.
• That a train can only enter or leave a station when it is con-sidered as being safe: property 2 will ensure that. By verifying that property for every signal, several trains will not be allowed to enter con-flicting train routes at the same time.
• That a train entering a train route will follow it: for instance, if the points are changed when a train is using its train route, this train will be sent away from it. In order to enforce this requirement, property 4 and 5 are needed. As these properties state that the points will remain in their
7.3 Conclusion 135
position when a train route is locked and the train route is not released too early (i.e. before all the points of the train route were passed), it means that the train cannot leave its route.
By ensuring that two conflicting train routes cannot be locked at the same time, that a train is only allowed to enter or leave a station when it is safe and that it has a route to follow, combined with ensuring that the train will actually follow its route until it reaches the end of it, one can be sure that collisions do not take place.
Also, the combination of 4 and 5 ensures that no derailing takes place. As the points are in the required position when a given train route is locked and a given train route cannot be released too early, derailing cannot happen.
In other words, properties 1, 2, 4, and 5 are enough for ensuring the basic safety goals. If one verifies these properties for every point, signal, and train route, one can verify that the basic safety goals are ensured by a given interlocking system.
7.3 Conclusion
In this chapter, patterns were introduced for adding external behaviour (i.e.
behaviours of points, track relays, and buttons) to a transition system that models the internal behaviour of an interlocking system (see chapter 6).
For points and buttons, only one version of behaviour is suggested. However, for track relays, two kinds of behaviour have been introduced:
• Random track relay behaviour (see section 7.1.1.1), where a track section can become occupied or freed when the system isidle.
• Ordered track relay behaviour (see section 7.1.1.2), where track sections are occupied by trains only.
Two kind of patterns forLTLassertions that specify safety properties have been introduced:
• Patterns for checking the basic safety goals(section 7.2.1).
They can be integrated with a scheme containing a transition system that
7.3 Conclusion 136
models internal behaviour and ordered track relay behaviour. These as-sertions check directly whether a collision or a derailing is possible in this transition system.
• Patterns for safety properties extracted from the train route table of the station (section 7.2.2).
They can be integrated with a scheme containing a transition system that models internal behaviour, button behaviour, point behaviour, and either random or ordered track relay behaviour and used for model checking that the requirements expressed by the train route table are respected.
It has been concluded that the basic safety goals can be proved indirectly by proving the properties derived from the train route table. Therefore, one can verify the basic safety goals under random track relay behaviour when making the following assumptions:
• Only one external event can happen at a time.
• An external event can only occur when the system is idle.
• Trains respect the aspects displayed by signals.
• Points cannot be switched when they are occupied.
• Points cannot be switched when a train route containing them is locked.
• Only one button can be pushed at a time.
• All buttons have to be released before any other external transition can be taken.
When using the patterns provided for ordered track relay behaviour, the follow-ing extra assumption are made:
• Trains are not longer than two track sections.
• Trains can only change direction at some specific track sections.
One can try adding trains with different lengths to ordered track relay behaviour, but as mentioned in section 7.1.1.3, ordered track relay behaviour will not scale easily. Scaling it will lead to a high number of position variables and a larger state space.
7.3 Conclusion 137
It is possible to indirectly prove the basic safety goals using random track relay behaviour. This behaviour includes more states possible in the real world than ordered track relay behaviour and is therefore considered as being stronger when model checking safety properties. However, in chapter 8, we will still apply both kinds of patterns to a concrete railway station.