Application: Stenstrup Station
8.3 Safety properties
wheregIdleis the original guard of thesetIdletransition rule auto-generated by the Java program.
8.3 Safety properties
Now that the internal and external behaviours of Stenstrup are formalized by a complete transition system, it is time to introduce the safety properties that have to be respected by the transition system. As explained in section 7.2, there are two categories of properties. The first directly expresses the basic safety goals using ordered track relay behaviour. The second expresses the basic safety goals by proving the properties of the train route table. The second category can be used for both kinds of track relay behaviour.
As explained in appendix C.4.3, all the properties can be found on the attached CD.
8.3.1 Basic safety properties
The following sections give examples of how the patterns introduced in section 7.2.1 can be applied to Stenstrup station, when assuming an ordered track relay behaviour.
8.3.1.1 No collision
The pattern for specifying that no collision takes place (see section 7.2.1.1, page 125) will now be instantiated.
To check that there is no possible collision, one can use the position variables in-troduced for the behaviour of the track relays. The principle of this is explained in section 7.2.1.1: a track section can only be occupied by one train at a time, i.e. for track 01, at most one of the position variables a12 t01 fwd, t01 fwd, t01 t02 fwd, t01 t04 fwd, t02 t01 back, t04 t01 back, t01 back and t01 a12 back can be true in one state. The corresponding assertion is (using the functionv defined in section 7.2.1.1):
ltl assertion
[ no collision t01 ] InterlockingSystem`
8.3 Safety properties 148
G(
v(a12 t01 fwd) + v(t01 fwd) + v(t01 t02 fwd) + v(t01 t04 fwd) + v(t02 t01 back)+ v(t04 t01 back ) + v(t01 back) + v(t01 a12 back)≤1),
8.3.1.2 No derailing
The pattern for specifying that no collision takes place (see section 7.2.1.2, page 127) will now be instantiated.
To verify that derailing does not take place on point01, one has to check that:
• when the point is occupied, it is not in its intermediate position. The occupation of the point is monitored by track relayt01.
ltl assertion
[ no derailing t01 ] InterlockingSystem` G(∼t01⇒plus01∨minus01),
• when the point and track section04 are occupied by a train, the point is in theminus position.
ltl assertion
[ no derailing t01t04 ] InterlockingSystem` G(
(v(t01 t04 fwd) + v(t04 t01 back)≥1) ⇒ minus01),
• when the point and track section02 are occupied by a train, the point is in theplus position.
ltl assertion
[ no derailing t01t02 ] InterlockingSystem` G(
(v(t01 t02 fwd) + v(t02 t01 back)≥1) ⇒ plus01),
8.3 Safety properties 149
8.3.2 Safety properties extracted from the train route ta-ble
The second approach to verifying that the basic safety goals are implemented by the interlocking system is to use the requirements of the train route table specific to Stenstrup. The following sections give examples of how the patterns introduced in section 7.2.2 can be applied to Stenstrup Station. This will in-directly ensure that there is no possibility of collision or derailing and can be done under the two behaviours introduced in section 7.1.1, because the resulting assertions will not depend on train positions.
8.3.2.1 Locking of conflicting routes
The pattern for specifying that conflicting train routes are not locked at the same time (see section 7.2.2.1, page 129) will now be instantiated.
In the train route table shown in figure 2.6, page 18, the conflicting train routes are indicated one by one. The locking of train routes 2 and3 is indicated by the steel core relayiadub, the locking of5 and6 byibdub, the locking of7 and 8 byuadub, and the locking of 9 and10 byubdub. For instance, if we look at train routes 2 and3, they are conflicting with train routes 5,6,7, and8. That means thatiadubshould not be dropped at the same time asibdub oruadub. 2 is also in conflict with10, and3 is in conflict with9. However,2 and10 cannot be locked at the same time because they require different positions for point02.
The same goes for3 and9, and for2 and3.
The following assertion checks that if either train route 2 or 3 is locked, none of their conflicting train routes are locked.
ltl assertion
[ conflict locking ia ] InterlockingSystem` G(∼iadub⇒ibdub∧uadub)
8.3.2.2 Signals
The pattern for specifying that the signals behave as specified in the train route table (see section 7.2.2.2, page 130) will now be instantiated.
8.3 Safety properties 150
There is one assertion for each signal that is extracted from the train route table. The following paragraph specifies the assertion for signalA.
SignalA must only display adrive aspect (indicated by a green light) if either train route 2 or 3 is locked. The conditions from train route 2 are: signal F is red, signalG is red or green, both points are in the plus position, and track sections A12, 01, 02, 03, and B12 are free. These requirements are specified in columns “Signaler”, “Sporskifter”, and “Sporisolationer” of the train route table. The ones for train route 3 can be deduced in the same way. Finally,A must not be green if neither train route 2 nor train route3 is locked. So the assertion for signalAis:
ltl assertion
[ signalA ] InterlockingSystem` G(idle∧aGreen⇒
∼ia∧a12∧t01∧t03∧b12∧
((t02∧plus01∧plus02∧fRed∧(gRed∨gGreen))∨
(t04∧minus01∧minus02∧eRed∧(hRed∨hGreen)))),
i.e. when signalA is green and there are no more possible internal transitions, train route2 or3 must be locked and the conditions concerning points, signals, and track sections for the locked train route must be valid.
8.3.2.3 Stop Fall
The pattern for specifying that the a signal stops displaying adriveaspect when a train is on a specific track section (see section 7.2.2.3, page 130) will now be instantiated.
The train route table specifies when each signal has to change from its drive aspect to its stop aspect. There is one assertion for each signal.
Two train routes,5 and6, use signalB as an entrance signal, i.e. when signal B displays a drive aspect, a train is allowed to enter one of the routes. Both express the same condition: signalBmust not display adriveaspect when track sectionB12 is occupied.
ltl assertion [ stopfallB ]
InterlockingSystem`
8.3 Safety properties 151
G(idle∧ ∼b12⇒ ∼bGreen),
i.e. if track section B12 is occupied, in the next state, either the system still has some possible internal transitions or signalBhas stopped displaying adrive aspect.
8.3.2.4 Point positions
The pattern for specifying that a point is in its required position when a train route is locked (see section 7.2.2.4, page 131) will now be instantiated.
When locking a train route, the position of the points has to be checked. For Stenstrup Station, when locking an entrance train route from Odense (shown by the steel core relay ia), there are two possible combinations of positions:
points 01 and 02 should be in the plus position (shown by relays plus01 and plus02), or they should be in the minus position (shown by relaysminus01 and minus02).
ltl assertion
[ locking points ia ] InterlockingSystem ` G(∼ia⇒
(plus01 ∧plus02)∨(minus01∧minus02)),
i.e. if an entrance train route from Odense is locked, the points are either both in their plus position or both in their minus position.
8.3.2.5 Train route release
The pattern for specifying that a train route is not released too early (see section 7.2.2.5, page 131) will now be instantiated.
For train route 5 and 6 (monitored by steel core relay ib), the 2 assertions expressing that the train routes are not released too early are:
ltl assertion
[ releaseIB1 ] InterlockingSystem` G(ib∧X(∼ib)⇒