Patterns for button behaviour

This section will present patterns for button behaviour. First, assumptions will be stated about the button behaviour and then the patterns will be formulated.

7.1.3.1 Assumptions about button behaviour

In reality, buttons can be pushed or released any time, which in our context will correspond to allowing changing the state of a button when the system is idle as well as not idle. However, as explained in section 6.5, we will only allow the changes of a button when the system is idle.

7.1 Patterns for external behaviour 121

Figure 7.6: State transition diagram of point P, with the behaviour described in section 7.1.2

Also, it is in reality possible to have several buttons pushed at the same time.

However, there is a problem related to having several buttons pushed at the same time. If one tries to lock conflicting train routes at the same time by having several buttons pushed at the same time, it might lead to a competition between the locking of the train routes. Only one of these train routes can be locked at the same time, so the timing of the electrical circuits will decide which train route there will be locked. From a logical point of view, the end result of the locking procedure will be non-deterministic.

Non-determinism when drawing and dropping will contradict one of the confi-dence conditions introduced in section 6.4. It was decided to verify that if the condition for drawing or dropping a relay is true, it remains true until the relay has changed its state. Competition between the locking of several train routes will imply that some relays for locking the conflicting train routes can change state, but when one of the train routes eventually becomes locked, some of the relays cannot change their state any more due to the fact that the given train route was locked. In that way, the introduced confidence condition in 6.4 will be invalid for the involved relays.

As this type of confidence condition is important for the soundness of the verifi-cation of safety properties, it is decided not to include the competition between several buttons as part of the external behaviour. It is therefore decided to assume that only one button can be pushed at a time.

7.1 Patterns for external behaviour 122

Another problem occurs when a button is kept pushed too long. Usually inter-locking systems have an emergency release procedure for uninter-locking train routes in case a button is pushed too long. However, in this project, we do not model such a procedure. This implies that if a button remains pushed, it may prevent a train route from being unlocked even if all the conditions for unlocking it are true. Therefore, it is necessary to enforce that a button is not pushed too long.

This can be done by releasing every button before settingidleto true combined with pushing only one button at a time, i.e. when the system is in an idle state, all buttons are released.

7.1.3.2 Formulation of patterns

Suppose we have a system with two buttons, B1 andB2. The initialisation of these buttons in an auto-generated transition system would be:

B1 : Bool :=false, B2 : Bool :=false

Transition rules for pushing the two buttons are:

[ pushB1 ] idle →idle⁰=false, B1⁰=true de

bc

[ pushB2 ] idle →idle⁰=false, B2⁰=true

The two guards do not contain∼B1 or ∼B2 because one of the assumptions of this button behaviour is that the system cannot be idle if a button is pushed.

If one wishes to apply another kind of behaviour, one should not forget to add them to the guards.

Now, the only problem is how to release the button that is pushed before setting idle to true. One might be tempted to release it when idle is set to true.

However, releasing a button might enable some internal transitions, meaning that idle is not supposed to be true any more. Releasing a button and setting the system in an idle state must therefore happen in several steps:

1. When no internal transition is possible, the button that is pushed is re-leased. This might enable further internal transitions.

7.1 Patterns for external behaviour 123

2. When no internal transition is possible,idle is set to true.

Enforcing this can be done by modifying the transition rule for setting idle to true such that it can be taken twice before setting idle to true. Suppose ExternalOK is the requirement described in section 6.5.3.1 for setting idle to true.

Theidle transition described by section 6.5 is then on the following form:

[ setIdle ]∼idle∧ExternalOK→idle⁰=true

In a system with two buttons, B1 and B2, the idle transition can then be modified in the following way:

[ setIdle ]∼idle∧ExternalOK→idle⁰=∼(B1∨B2), B1⁰ =false, B2⁰=false

If no internal transition is possible,setIdlewill release the buttons. Furthermore, idle will be set to true if and only if all the buttons are released in the current state. WhensetIdle is taken, there will be two possible scenarios:

1. If every button is released,idle is set to true.

2. If a button is pushed, it will be released, butidle will not be set to true.

The next timesetIdle is taken, all the buttons are released andidleis set to true.

An example of a chain of transitions under the introduced button behaviour can be seen in figure 7.7.

Similar button behaviour can be introduced for an arbitrary transition system by treating every button in the same way as B1 andB2. In that way, competition between the locking of different train routes is avoided.

Note: It will still be possible to try locking a train routeR2 when a conflicting train route R1 is locked. When the conflicting train route R1 is locked, the buttons for locking this train route will be released and a new button (like the one initiating the locking ofR2) can be pushed.

In the real world, this behaviour corresponds to the fact that the operator must push a button until the actions enabled by it have taken place and that he or she