Confidence conditions for the transition sys- sys-tem

As previously mentioned, it is decided to make a transition system that includes two transition rules for each relay: a rule for dropping it and a rule for drawing it. The guards of these rules can be computed in terms of abstract syntax by the functions introduced in section 6.3.

However, we have not discussed the problems related to only drawing and drop-ping a single relay at a time. The danger is that such a model might not include the states that can be obtained by changing relay states concurrently.

Also, we have not discussed a specific problem related to steel core relays: there should never be a dropping and a drawing current through a steel core relay at the same time.

This section will introduce confidence conditions that can be used for proving that such problems do not exist.

6.4.1 Steel core relay issue

As previously described in section 2.5.1.2, a steel core relay must not have a drawing current and a dropping current through it in the same state. The previously defined conditions for drawing and dropping a steel core relay cannot be true at the same time because a relay can only be dropped when it is drawn and it can only be drawn when it is dropped. However, the two conditions for having current through the two parts of the steel core relay can be true at the same time. Such a situation is not desired by Banedanmark and it is therefore relevant to prove that it does not happen.

Supposec1 is the condition for having a drawing current through a given steel core relay and c2 is the condition for having a dropping current through the same steel core relay (c1andc2can be computed by the functions drawingCur-rentThroughSteelRelay and droppingCurrentThroughSteelRelay given in section 6.3 and afterwards be converted from abstract syntax to concreteRSL-SAL syn-tax). Then an LTL assertion expressing that c1 and c2 are never true in the same state is:

ltl assertion

[ mutualExclusionC1C2 ] InterlockingSystem`G(∼(c1∧c2))

6.4 Confidence conditions for the transition system 83

In order to be sure that steel core relays behave in a consistent manner, it is decided that a similar property should be verified for each steel core relay.

6.4.2 Concurrency issues

When only dropping or drawing one relay at a time, we ignore the fact that events can happen concurrently. It might only happen rarely, but one cannot dismiss the possibility of a situation where several relays change their state at the exact same time. InRSL-SAL, the only way of modelling this would be to introduce other transition rules. For instance, one could introduce a transition rule for drawing a relayrelay1, a transition rule for drawing a relayrelay2, and a transition for drawing them at the same time. However, following this principle would lead to a lot of extra transition rules. Each time several events can happen concurrently, there should be a transition for handling this. Introducing such extra rules would lead to the following issues:

• The number of transition rules would be greatly increased.

• The introduction of transition rules for concurrent relay changes would lead to extra static analysis before making the transition system. It would be necessary to decide which guards can be true at the same time. Doing this statically might not be a trivial task.

• The introduction of a lot of extra rules would lead to an increased run-ning time when model checking. TheSALverification tool would have to evaluate a lot of extra guards when building the state space.

• The introduction of extra guards would probably make it difficult for a human reader to understand the transition system.

Instead of adding extra transitions, it would be better to prove that the order of the transitions does not matter. Verifying this will include proving that there is no race between transitions (i.e. it should be proved that taking one transition cannot falsify the guard of another transition). This can be proved by checking that if a guard is true at one point, it remains true until the transition protected by the guard is taken. In reality, it corresponds to that if a relay can change its state, it will change its state before the physical condition for changing it is no longer existing.

Verifying this is especially relevant because Banedanmark desires determinism:

a relay that can change state should change state even though other relay changes occur.

6.4 Confidence conditions for the transition system 84

By verifying this, Banedanmark can avoid situations where an interlocking sys-tem seems to be working properly, but suddenly one day a new sequence of relay changes takes place, making the interlocking system enter an unsafe state. This might happen because some relays react slower than they used to.

Theinterleaving model introduced in section 6.2.2 contains exactly two transi-tion rules for changing the state of a relay. Also, each transitransi-tion rule can only change the state of a single relay. Therefore, the transition rules can be grouped into pairs such that each pair is mutually assignment disjoint with every other pair. As each pair contains a rule for drawing and a rule for dropping the same relay, the guards of the rules cannot be true at the same time. This means that if one proves that there is no race between the transitions, one also proves that the model will include the states that can be obtained by taking two transitions concurrently.

One can ensure that the order does not matter by verifying that if a guard becomes true, then it will remain true until the corresponding transition is taken. If the condition for drawing a relay is fulfilled, it will remain true until the relay is drawn.

Assume that a guard, g1, contains all the conditions needed for drawing re-lay1. These conditions are given by the functioncanDrawRegularRelay or the functioncanDrawSteelRelay defined in section 6.3 (assuming that the abstract syntax is converted to concrete syntax). The followingLTLexpression will then correspond to expressing thatg1 remains true untilrelay1 is drawn:

ltl assertion

[ g1UntilDrawn ] InterlockingSystem ` G(g1⇒X(∼g1⇒relay1))

The LTL expression should be interpreted in the following way:

It holds for all states: if g1 is true in one state, the following will hold for the next state: If g1 is false, then relay1 is drawn. Therefore, when g1 becomes true in one state, it must remain true untilrelay1 is drawn.

An equivalent pattern can be used when dropping the relays. In the following LTL expression, it is assumed thatg2 is the guard for dropping relay1:

ltl assertion

[ g2UntilDropped ] InterlockingSystem` G(g2⇒X(∼g2⇒ ∼relay1))

6.4 Confidence conditions for the transition system 85

The two LTL expressions for relay1 are sufficient for verifying that there will not be any concurrency issues related to drawing and droppingrelay1. However, if one wishes to ensure that racing conditions do not exist and the transition system can obtain the states that can be obtained by changing relay states con-currently, one must verify equivalentLTLassertions for all relays. All theLTL expressions for verifying that no concurrency issues exist can then be consid-ered as confidence conditions for a transition system containing two rules for each relay, one for drawing it and one for dropping it. If one of the expressions is invalid, the model will not cover the case where some specific relay changes happen at the same time. That is, the interleaving model will not be completely sound if one of the confidence conditions is invalid.

It can therefore be concluded that the above pattern for detecting concurrency issues must be introduced for every transition that is capable of drawing and dropping a relay.

6.4.3 Conclusion

We have now studied an approach where we focus on the logics of interlocking systems instead of modelling the propagation of current. Section 6.3 described how to obtain the following conditions based on theDiagrams of a StaticInter-lockingSystem:

• A condition for when it is possible to draw a relay, g_up,r (given by can-DrawRegularRelayorcanDrawSteelRelay, converted to concreteRSL-SAL syntax).

• A condition for when it is possible to drop a relay, gdown,r (given by canDropRegularRelay or canDropSteelRelay, converted to concrete RSL-SALsyntax).

A transition system can be formulated by using these principles:

• Every relay and button are modelled as a Boolean variable. For relays, true means drawn and false means dropped. For buttons, true means pushed and false means released.

• The initial value of the Boolean variables will correspond to the normal state of theStaticInterlockingSystem.

• For each relayr of a diagram, two transition rules are added: