A specific semantics of relay diagrams

This section will present the idea of making a specific transition system that models the behaviour of a specific StaticInterlockingSystem. The idea is to ex-amine aStaticInterlockingSystem and then generate a specific transition system that models the behaviour of it.

6.2 Different approaches to a behavioural semantics of relay diagrams 70

If a transition of the transition system introduced in the previous section was taken, it would either draw or drop a single relay. Instead of making two general rules like in the previous section, one can introduce specific rules for drawing and dropping specific relays. For instance, one could, for each relay, make one rule for drawing it and one rule for dropping it.

The state of relays can be modelled as Boolean variables where true is equivalent to drawn and false is equivalent to dropped. Similarly, buttons can be modelled as Boolean variables where true is equivalent to pushed and false is equivalent to released.

Recall figure 6.1, page 64. A transition system that models the behaviour of relayRR1 is:

/∗ Other transition rules∗/

...

end

As the Boolean variables are false, relaysRR1 andA1 are dropped in the initial state and buttonB1 is released.

The transition ruledrawRR1 specifies that RR1 can be drawn if:

1. RR1 is dropped.

2. A1is drawn orB1 is pushed. This corresponds to the condition for having current throughRR1.

6.2 Different approaches to a behavioural semantics of relay diagrams 71

The transition ruledropRR1 states thatRR1 can be dropped if:

1. RR1 is drawn.

2. A1 is dropped andB1 is released. This corresponds to the condition for not having current throughRR1.

In more general terms: suppose the Diagrams of a StaticInterlockingSystem contain N relays. A transition system that will describe its behaviour will be on the following form:

/∗ Declarations of other variables∗/

...

/∗ Other transition rules∗/

...

end

When making such aninterleaving model for a specificStaticInterlockingSystem, the difficult parts is to calculate the guards of each transition rule. If one wishes to calculate the guards, one has to examine all the possible paths in

6.2 Different approaches to a behavioural semantics of relay diagrams 72

each Diagram of the StaticInterlockingSystem. For instance, the condition for drawing a regular relay is a condition that evaluates to true if and only if there is a conductive path through it.

Also, it is necessary to prove that the interleavings of relay changes also include the states that can be obtained by drawing and dropping relays concurrently.

Therefore, it is also necessary to introduce some confidence conditions (formu-lated asLTLassertions) that can be used for verifying that this is actually the case.

Specifying such a transition system for a specificStaticInterlockingSystem man-ually is not a trivial task. Therefore, this approach should be supported by functions that, given aStaticInterlockingSystem, automatically generate a tran-sition system and its confidence conditions. Such a generation is illustrated in figure 6.4.

Figure 6.4: Conversion from a StaticInterlockingSystem to a transition system and its confidence conditions.

The idea is to formulate an abstract syntax for an RSL-SAL transition sys-tem and for the necessary LTL expressions. Generator functions to convert an abstract syntax for relay diagrams (i.e. a StaticInterlockingSystem and its contained Diagrams) to abstract syntax of a transition system and confidence conditions can then be specified.

The functions shown in figure 6.4 correspond to the box marked B in figure 4.2, page 48. The abstract syntaxes for an RSL-SALtransition system and its confidence conditions correspond to the box markedE.

6.2.3 Conclusion

In this section, two approaches to obtaining the behaviour of an interlocking system described by the typeStaticInterlockingSystem have been presented.

There are two central problems related to theSISSemantics scheme introduced in section 6.2.1. First of all, as explained in chapter 3,RSL-SALsupports neither

6.3 Conditions for drawing and dropping a single relay 73

recursive nor iterative functions. For a regular relay,canDrawandcanDropwill have to examine whether a conductive path exists through it. For a steel core relay, the functions will have to examine whether a conductive path exists trough a specific part of it. Therefore, it seems difficult to formulate these functions without using recursion or iteration insideSISSemantics, making it impossible to translate the scheme toSAL.

The second central problem is that maps inRSL-SALseem to be quite inefficient in terms of verification time. Our experience with this data structure is that it takes a relatively long time to verify simple properties when using maps, even if the state space is small. As lists and recursive data types are not available in RSL-SAL, sets are the only alternative to maps. Formulating a completely set-based version of aStaticInterlockingSystemseems to be difficult in anRSL-SAL context, especially because it is impossible to iterate through sets (as explained in chapter 3, recursion, thehd set operator, and comprehended expressions are not allowed). Therefore, using maps seems to be unavoidable.

With these facts in mind, it is decided to use the approach introduced in section 6.2.2: generator functions will be specified for transforming a StaticInterlock-ingSystem to a transition system and its confidence conditions. Generating the transition system before translating it to RSL-SAL allows the use of recursive functions. Therefore, it is possible to use functions that would have been im-possible to use inSISSemantics. The drawback of making a specific transition system is that one needs to generate a transition system each time one wants the behaviour of a newStaticInterlockingSystem. However, with the limitations of RSL-SALin mind, it seems unlikely that one can succeed in using the first solution.

The rest of this chapter will discuss how to generate a specific transition system and its confidence conditions based on a StaticInterlockingSystem.

6.3 Conditions for drawing and dropping a