In this chapter, we will explore some possible changes you can make in component behaviour to support the usage of ‘external’ for required interfaces. In a few steps, you will discover:

  • Where to build your solution

  • How to start solving the problem you face with ‘external’

  • Implementing the solution as component behaviour

Responsibilities and using ‘external’ components

To make it easier to accommodate for concurrent behaviours found in ‘external’ ports, it is recommended to define another component that provides the ITimer interface and requires an external ITimer interface. Then, in the System component, bind the provided ITimer port of the new component to the required ITimer port of the Controller. From the Controller point of view, the ITimer port is no longer ‘external’. Instead, the new component (let’s call it RobustTimer) becomes responsible for translating the ‘external’ ITimer port to a regular ITimer port.

Often reoccurring concepts when talking about software quality are:

Of course, these concepts are important in Dezyne as well. A component that is responsible for many different tasks becomes more complex to maintain and takes more time to be verified. In extreme cases, you might even find that the state space (the possible combinations of state within the component) is too large for verification to reason about. By dividing responsibilities over components, you can avoid such problems.

If you’ve performed the steps above, the situation should now look like this:

component RobustTimer {
  provides ITimer iTimer;
  requires external ITimer ext_iTimer;

  behaviour {

  }
}

image

image

Note that the required ‘external’ ITimer port on RobustTimer is coloured yellow; this is the case for all ports that are marked ‘external’. It is an easy way to identify these ports when looking at the System view. Note that the required ITimer port in Controller is no longer marked ‘external’.

How to start solving the problem you face with ‘external’

The RobustTimer component will be responsible for the mapping of an ‘external’ ITimer port to a regular ITimer port. The intent is to define the behaviour of the component in such a way that even if ‘external’ delays occur, communication over the provided ITimer port does not suffer from this.

The most straight-forward behaviour specification would be to map in-events on the provided ITimer port to in-events on the required ITimer port and to do the same for out-events of the required port. As a first exercise, implement the behaviour of RobustTimer this way.

Hint: make sure the states defined in the ITimer interface are followed in the RobustTimer component behaviour as well.


component RobustTimer {
  provides ITimer iTimer;
  requires external ITimer ext_iTimer;

  behaviour {
    enum State { Idle, Running };
    State state = State.Idle;

    on iTimer.start(ms): {
      [state.Idle] {
     ext_iTimer.start(ms);
     state = State.Running;
      }
    }

    on iTimer.cancel(): {
      [state.Running] {
     ext_iTimer.cancel();
     state = State.Idle;
      }
      [state.Idle] { }
       }

    on ext_iTimer.timeout(): {
      [state.Running] {
     iTimer.timeout();
     state = State.Idle;
      }
    }
  }
}


The above solution is a first rudimentary step towards a working solution. If you verify the RobustTimer component, you will see the exact same illegal assertion as we found earlier in the previous chapter. However, this time it is extracted from all interleaving with other required and provided ports of the Controller component and you can focus solely on the behaviour of the required ‘external’ ITimer port. Let’s reconsider the timeline described in How does this translate to runtime execution?:

image

Recall that x is the time it takes for the cancel event from iTimer to be processed. During x, the timeout occurs on ext_iTimer and is queued accordingly. After x, RobustTimer is in the Idle state but still has to handle the queued timeout. This scenario is not described in the behaviour of RobustTimer and as such, it is implicitly illegal.

In the next chapter, we will have a look at how to implement behaviour such that these possible concurrencies discovered by ‘external’ can be handled.

Implementing the solution as component behaviour

Now that the RobustTimer component has been created and the rudimentary communication between the provided ITimer and required ‘external’ ITimer has been established, it is time to start working towards a functional solution that is verifiably correct.

A logical first step could be to specify that when `ext_iTimer `sends a timeout event to the RobustTimer while RobustTimer is not in a Running state, the timeout event is ignored (so no operation occurs). This ensures that within the RobustTimer component, possibly delayed timeouts do not trigger `illegal`behaviour if the cancel event had already occurred.

As an exercise, make the aforementioned change to the handling of `ext_iTimer.timeout() ` and verify the RobustTimer again. Try to figure out what has happened in the scenario that the verifier shows you before moving on.


component RobustTimer {
  provides ITimer iTimer;
  requires external ITimer ext_iTimer;

  behaviour {
    enum State { Idle, Running };
    State state = State.Idle;

    on iTimer.start(ms): {
      [state.Idle] {
     ext_iTimer.start(ms);
     state = State.Running;
      }
    }

    on iTimer.cancel(): {
      [state.Running] {
     ext_iTimer.cancel();
     state = State.Idle;
      }
      [state.Idle] { }
       }

     on ext_iTimer.timeout(): {
      [state.Running] {
        iTimer.timeout();
        state = State.Idle;
      }
      [state.Idle] {}
    }
  }
}

image



The scenario shown to you by the verifier is one where a ‘timeout’ event sent in response to the first ‘start’ is misinterpreted by RobustTimer as if it was sent in response to the second ‘start’ event; however, ext_iTimer is Running while the timeout event is processed. After propagating the timeout event to iTimer, iTimer is Idle once again, allowing for a start event to occur. While ext_iTimer is Running, start events are illegal.

Nonetheless, the length of the trace has increased, indicating that we have passed the first hurdle of illegal timeouts after the timer had already been cancelled. Progress has been made, but we’re not quite there yet.

We need to implement some way to distinguish between outdated timeout events and timeout events from the timer that was currently started. Let’s refer to the time window between a timer start and a timeout or cancel as a session. There are two ways to approach this situation: keep track of the current session and ignore others, or implement a handshake to ensure that a session is closed before starting a new one.

‘The’ solution: handshake protocol

The recommended option is to implement a handshake mechanism to ensure that the current session is closed. If you recall, the original problem we discovered was that it was possible to queue a timeout event while the timer was being cancelled. The description of the problem already hints at part of the solution: apparently there exists a state where the Timer is being cancelled. This state starts when the cancel event is sent and ends at some point in time.

When the being cancelled state has ended, this means that the Timer has fully stopped and as such, no timeout events can occur anymore. If you queue a notification that this condition is fulfilled, this notification can be used to denote the end of a Timer session.

As an exercise, extend the ITimer interface with a Stopping state that starts when a Running timer is cancelled. Within the Stopping state, in-events should be illegal and inevitably, an out-event cancelled should be sent.


interface ITimer {
  extern long_integer $long$;
  enum State { Idle, Running, Stopping };
  in void start(long_integer milliseconds);
  in void cancel();
  out void timeout();
  out void cancelled();

  behaviour {
    State state = State.Idle;

    [state.Idle] {
      on start: state = State.Running;
     on cancel: { }
      }

    [state.Running] {
      on start: illegal;
      on cancel: state = State.Stopping;
      on inevitable: {
        state = State.Idle;
        timeout;
      }
    }

    [state.Stopping] {
      on start: illegal;
      on cancel: illegal;
      on inevitable: {
        state = State.Idle;
        cancelled;
      }
    }
  }
}


With the above interface modification, a handshake protocol can be supported where the end of a Timer session is marked with a cancelled event. You may find yourself wondering why this is so useful.

Here’s the trick: the event that marks the end of a session travels through the same communication channel as the timeout events. The interface prohibits sending timeouts during the Stopping state and the Stopping state transitions to the Idle state where again, no timeouts can be sent. Therefore, it is guaranteed that there will be no more timeout events from the previous session after the cancelled event has been placed into the queue.

So, the modified ITimer interface complies with the handshake we want to implement to solve the ‘external’ delay problem. What remains to be done is update the RobustTimer component behaviour to make use of the newly added handshake.

The behaviour we want to add to the RobustTimer is the addition of the Stopping state. When a cancel event is sent to its provided ITimer port, this is propagated to the ‘external’ ITimer port and the RobustTimer transitions to the Stopping state. Until the ‘external’ ITimer port has replied with a cancelled event, any timeouts coming through the port while Stopping should be silently discarded. When the cancelled event is handled, the RobustTimer transitions back to the Idle state and the cancelled event is propagated to the provided ITimer.

Exercise: Add the changes listed above to the behaviour of the RobustTimer component.


component RobustTimer {
  provides ITimer iTimer;
  requires external ITimer ext_iTimer;

  behaviour {
    enum State { Idle, Running, Stopping };
    State state = State.Idle;

    on iTimer.start(ms): {
      [state.Idle] {
        ext_iTimer.start(ms);
        state = State.Running;
      }
    }

    on iTimer.cancel(): {
      [state.Running] {
     ext_iTimer.cancel();
   state = State.Stopping;
      }
      [state.Idle] {  }
    }

    on ext_iTimer.timeout(): {
      [state.Running] {
     iTimer.timeout();
     state = State.Idle;
      }
      [state.Stopping] { /* discard */ }
    }

    on ext_iTimer.cancelled(): {
      [state.Stopping] {
        iTimer.cancelled();
        state = State.Idle;
      }
    }
  }
}


If you verify the behaviour in the above solution, you will still encounter one last verification error. While we were focussing on making sure possibly delayed timeouts are properly handled, we didn’t implement the handshake we designed for that purpose in the scenario where an Idle Timer receives a cancel event. Luckily, the fix for this is a pretty simple one:

interface ITimer {
// variable and event declarations
    behaviour {
        [state.Idle] {
            on start: state = State.Running;
          on cancel: { cancelled; }
        }
    // rest of the behaviour specification

component RobustTimer {
    provides ITimer iTimer;
    requires external ITimer ext_iTimer;

    behaviour {
    // variable declarations
        on iTimer.cancel(): {
            [state.Running] {
                ext_iTimer.cancel();
                state = State.Stopping;
            }
          [state.Idle] { iTimer.cancelled(); }
        }
        // rest of the component implementation

With these additions in place, the RobustTimer component will pass verification and you have successfully implemented a protocol that is robust against possibly delayed asynchronous events from a native component. By doing this in a Dezyne component, any other component that is connected to the ITimer port provided by RobustTimer can use it as if it were not ‘external’. Only the RobustTimer component is responsible for handling the ‘external’ behaviour.

In the next and final chapter, we will have a look at what needs to be updated in the rest of the Alarm System and afterwards we will take a step back and summarise what we’ve discovered throughout this tutorial.