Towards a behavioural semantics of relay diagrams
6.5 Interaction with the environment
6.5.4 Properties related to the idle variable
After having introduced theidlevariable, it is possible to formulate some desired system properties in terms ofLTL assertions usingidle. The following sections will introduce these properties.
6.5.4.1 Initial state of the idle variable
As described in section 2.6, the diagrams or an interlocking system present the interlocking system as it is in its normal state. In our context, the initial state of a transition system will correspond to the normal state of an interlocking system. In the normal state of an interlocking system, no relay changes are possible unless something happens in the external world. If not, it means that at least one diagram of the interlocking system contains an error. This corresponds to having the conditions for being idle fulfilled in the initial state. For reasons of consistency, this property should be verified. To do this, there are two possible solutions:
• The idea of the first solution is to setidle to true in the initial state and verify that the conditions for being idle are fulfilled in the initial state. For the above transition system, theLTLassertion for verifying this would look like:
ltl assertion
[ InitIdle ] InterlockingSystem` ∼(gi1∨gi2)
• The second idea is havingidle = false in the initial state and verify that idleis true in the next state, i.e. the only possible transition in the initial
6.5 Interaction with the environment 94
state is the one that makes the system idle. InLTL, it can be expressed like this:
ltl assertion
[ InitIdle ] InterlockingSystem`X(idle)
The advantage of the second solution is that the LTLassertion is the same for all transition systems and can be applied to all transition systems that use the idlevariable. On the contrary, the first solution requires a specificLTLassertion for a specific transition system. Therefore, the second solution is chosen.
6.5.4.2 No internal cycle
Another desired property of interlocking systems is that a chain reaction of internal relay changes always ends in an idle state. For instance, if an input is received from the external world, the interlocking system should respond to it and at some point find another idle state where no change will happen until a new input is received from the external world. Thereby, it is verified that unrealistic starvation of events of the external world is avoided. In our context, this is equivalent to having an idle system over and over again. InLTL, it can be formulated like:
ltl assertion
[ AlwaysEventuallyIdle ] InterlockingSystem` G(F(idle))
The formula states that the system will always eventually be idle.
In general, both of the above properties should be verified for every transition system in order to detect possible errors in the diagrams of the interlocking system.
6.5.5 Conclusion
We have now discussed how to integrate the interaction with the external world.
The main problem was that the notion of time does not exist inRSL-SAL. There-fore, it has been decided to distinguish between internal events and external events. An internal event is something that happens inside the electrical circuit
6.5 Interaction with the environment 95
of an interlocking systems and an external event is something that happens in the external world. The main assumption is that external events cannot hap-pen if internal events are possible. This corresponds to assuming that changes happen faster in the circuit than in the external world.
To do that, it has been decided that a transition system can either be idle or busy. In a state where the system is idle, no internal events are possible and the transition system is ready to accept external events. If the system is busy, only internal events will be possible. To enforce this, the following concepts have been introduced:
• A Boolean variable called idle. If the variable is true, the system is idle.
Otherwise the system is busy.
• idleis initialised to false.
• External events cannot happen whenidle is false.
• When an external event happens,idle is set to false.
• A transition is made for settingidle to true. This transition can only be taken if no internal transition is possible.
Suppose we have a transition system containing the following internal transition rules:
guard1→relay10 =true de
bc
guard2→relay10 =false de
bc
guard3→relay20 =true de
bc
guard4→relay20 =false
The transition rule for settingidle to true will be:
∼idle∧ ∼(guard1∨guard2∨guard3∨guard4)→idle0 =true
Suppose the following external transitions are possible:
extguard1→extRelay10 =true
6.6 Abstract generation of behavioural semantics 96
de bc
extguard2→extRelay10 =false de
bc
extguard3→extRelay20 =true de
bc
extguard4→extRelay20 =false
Thenidle must be added as part of the guard and it must be set to false when taking one of the transitions:
idle∧extguard1→idle0 =false, extRelay10=true de
bc
idle∧extguard2→idle0 =false, extRelay10=false de
bc
idle∧extguard3→idle0 =false, extRelay20=true de
bc
idle∧extguard4→idle0 =false, extRelay20=false
In order to check that no relay change is possible in the initial state, one can check thatidle is true in the state after the initial state:
ltl assertion
[ InitIdle ] InterlockingSystem`X(idle)
In order to ensure that a sequence of internal transitions terminates, it is checked that the transition system always will be idleat some point in the future:
ltl assertion
[ AlwaysEventuallyIdle ] InterlockingSystem` G(F(idle))