Next: , Previous: , Up: How to use ‘external'?   [Contents]


4.2.3 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.

Solution:

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] {}
    }
  }
}
images/sequence_6

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.


Next: , Previous: , Up: How to use ‘external'?   [Contents]