Patterns for external behaviour and safety
7.2 Patterns for safety properties
7.2.1 Patterns for basic safety properties
With the random track relay behaviour, it is not possible to distinguish between trains and other objects that occupy a track section. Therefore, if one wants direct proofs of the basic safety goals, it is necessary to use ordered track relay behaviour, as specified in section 7.1.1.2.
Recall the station shown in figure 7.4, page 113. For that station, the following track positions were introduced:
T1 AtoB : Bool := false, T1 T2 AtoB : Bool :=false, T2 AtoB : Bool := false, T2 BtoA : Bool :=false, T2 T1 BtoA : Bool := false, T1 BtoA : Bool :=false
7.2.1.1 No collision
This section will formulate LTL assertions for checking that collisions do not take place.
7.2 Patterns for safety properties 126
When expressing the next LTL assertions, the following function will be used for extracting a Nat from a Bool expression such that 1 corresponds to true and0 corresponds tofalse:
value
v : Bool→Nat
v(b)≡ifbthen1else 0end
A collision on track sectionT1 has occurred if there is more than one train on T1.
The following LTL assertion checks that at most one train is on track section T1 at a time:
ltl assertion
[ noCollisionOnT1 ] InterlockingSystem`
G(v(T1 AtoB) + v(T1T2 AtoB) + v(T1 BtoA) + v(T2T1 BtoA)≤1)
This is not sufficient for checking that no collision takes place onT1. IfT1 AtoB is true and the signal A is green, a new train can enter the station without changing the train position variables. The transition rule for inserting the new train will setT1 AtoB to true. AsT1 AtoB is already true, the change will not be detected by the above assertion and thereby not be detected as a collision.
To check that such a collision does not take place, the followingLTL assertion is introduced:
ltl assertion
[ noTrainOnT1WhenAGreen ] InterlockingSystem` G(idle∧aGreen⇒
v(T1 AtoB) + v(T1T2 AtoB) + v(T1 BtoA) + v(T2T1 BtoA) = 0)
TheLTLexpression states that it holds for every state that if the system isidle and signalAis green, then track sectionT1 is empty. The check for havingidle must be added in order to give the system a chance to respond on having T1 occupied. SignalAis supposed to be green to allow a train to enterT1 (driving towards B). Then, when a train entersT1, the system is supposed to respond to that during a sequence of non-idle states. Finally, when idle becomes true, the system has responded and signalAis not supposed to be green any more.
7.2 Patterns for safety properties 127
Similar properties can be introduced forT2. In fact, they would be equivalent to the ones defined forT1 with a few modifications of the used variables in the expressions.
For a real station, one will have to analyse the track layout when formulating similar properties for a specific station.
7.2.1.2 No derailing
This section will formulateLTLassertions to check that derailing does not take place.
Consider pointP in figure 7.8. When trains approachP fromT0, they cannot derail if the point is either in the plus position or in the minus position and remains in that position while the train occupies it.
Figure 7.8: A point P and the track sections next to it.
Suppose thatP has relaysplusP andminusP for indicating its position. Fur-thermore, suppose thatp is the name of the track relay that monitors whether there is a train onP. The following expression will check thatP is either in the plus position or the minus position when P is occupied:
ltl assertion
[ plusOrMinusPositionWhenP ] InterlockingSystem` G(∼p⇒plusP∨minusP)
The expression states that if there is a train onP,P cannot be in the interme-diate position. As P needs to enter the intermediate position on the way from the plus position to the minus position or the other way around, the expression will also ensure that the position of the point is not changed when a train is on it.
When ensuring this, derailing cannot happen when trains are approaching P from T0. If a train reaches P, the point will remain in either the plus position or the minus position until the train has left the track. However, when a train
7.2 Patterns for safety properties 128
approachesP from eitherT1 orT2, this property is not sufficient to ensure that derailing does not take place. For instance, if P is in a position such that P and T1 are connected and a train approachesP fromT2, a derailing will take place.
Consider figure 7.9 that shows different occupations ofP,T1, andT2. When a train is on P and T1, the point must connect P and T1. Similarly, if a train occupies P andT2,P must connectP andT2.
Figure 7.9: Different ways of occupying a point and the track sections next to it.
Suppose that havingplusP drawn indicates thatP is connected toT2 and that P T2 fwd andT2 P back are the position variables for representing that a train occupies P andT2, going from P to T2 or fromT2 to P respectively. Then, the following expression will check chat P must be in the plus position when there is a train on both P andT2:
ltl assertion
[ no derailing P t01 ] InterlockingSystem `
G( (v(P T2 fwd) + v(T2 P back)≥1)⇒plusP)
IfminusPindicates thatPis connected toT1 and thatP T1 fwdandT1 P back are the position variables representing that a train occupies P and T1, going
7.2 Patterns for safety properties 129
from P toT1 or fromT1 to P respectively, the similar expression forT1 and P is:
ltl assertion
[ no derailing P t01 ] InterlockingSystem `
G( (v(P T1 fwd) + v(T1 P back)≥1)⇒minusP)
When model checking the above assertions for P using ordered track relay be-haviour, one can ensure that trains do not derail. Similar expressions should be introduced for each point of a station in order to make sure that derailing does not take place in the context of ordered track relay behaviour.