Menu

Time and Timers: Making an LED Blink

Language keywords: bool extern false inevitable out true

Operator: !

Dezyne’s logical models have no inherent concept of time; instead, Dezyne only knows sequences of events and responses to events. Model verification proceeds by examining, directly or indirectly, every possible eligible-event-initiated trace path through the component and/or interface(s) being verified. Each step in an underway verification trace represents zero elapsed time in the modeled system (and takes very little computation time during verification). Any verification trace stops immediately upon finding an error, thus running to completion signals that no logic-related errors were found in the model.

Dezyne can model and verify repeating behaviour. We’ll build a timer interface that makes our LED blink on and off at constant time intervals, and that works as-is in auto-generated C++ source code. The entirely new – but nearly all familiar – code below defines a simple timer interface and a hand-written component that will implement the interface. An out function names an event that a requiring (calling) component has to handle in its behaviour.

interface ITimer {
  enum State { Idle, Running };
  in void start();
  in void cancel();
  out void timeout();

  behaviour {
   State state = State.Idle;

   [state.Idle] {
      on start: state = State.Running;
      on cancel: {}
   }
   [state.Running] {
      on start: illegal;
      on cancel: state = State.Idle;
      on inevitable: { // ALWAYS happens eventually unless cancelled first
        state = State.Idle;
        timeout;
      }
   }
  }
}

component Timer { provides ITimer iTimer; }

Dezyne’s inevitable keyword indicates that the timeout event will always eventually happen during model verification, to test all possible execution paths, including the possibility of a timeout just before a cancel call arrives. The inevitable keyword has a companion we’ll discuss later, optional, which means “usually happens but might never happen”; both these keywords are used only in interfaces, to inform verification about certain special conditions it must check.

Note in the above the asymmetry between the Idle state and the Running state. The interface says it’s OK to cancel when the timer is idle, but it’s illegal to try to start when the timer is running. We assume the caller will manage its own state with respect to use of the timer.

The next version of the timer shows how to pass a parameter of a particular type to a model method.

interface ITimer {
  extern long_integer $long$; // source code data type will be long
  in void start(long_integer milliseconds);
  in void cancel();
  out void timeout();

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

    [state.Idle] {
      on start: state = State.Running;
      on cancel: {}
    }
    [state.Running] {
      on start: illegal;
      on cancel: state = State.Idle;
      on inevitable: { // ALWAYS happens eventually unless cancelled first
      state = State.Idle;
      timeout;
      }
    }
  }
}

component Timer { provides ITimer iTimer; }

The extern keyword above maps a model data type to an indicated data type in Dezyne-generated source, via string substitution. For example, the above sample leads to this line in generated C++ code:

std::function <void (long milliseconds)> start;

Now we integrate the timer into the LED controller. The interface definition below is complete; it uses the events-leading pattern.

interface ILED {
  in void shine();
  in void darken();
  in void blink();

  behaviour {
    enum State { Dark, Shining, Blinking };
    State state = State.Dark;

    on shine: { state = State.Shining; }
    on blink: { state = State.Blinking; }
    on darken: { state = State.Dark; }
  }
}

This interface allows a caller to reset the LED to the same state it’s already in. Below is a partial implementation of the blinkable LED component, sketching in a states-leading approach. You can create this exact component in Dezyne (though it might need a different name) and verify that it conforms to both the ILED interface and the ITimer interface, even though the interface expresses its logic in event-leading format. Also, in this component we will track the LED’s lit/dark state as part of managing the blinking state; as with state variables we have to initialize any boolean variable in its declaration.

component LED {
  provides ILED iLed;
  requires ITimer iTimer;

  behaviour {
    enum State { Dark, Shining, Blinking };
    State state = State.Dark;
    bool lit = false;

    [state.Dark] {
      on iLed.shine(): {}
      on iLed.darken(): {}
      on iLed.blink(): {}
      on iTimer.timeout(): {}
    }
    [state.Shining] {
      on iLed.shine(): {}
      on iLed.darken(): {}
      on iLed.blink(): {}
      on iTimer.timeout(): {}
    }
    [state.Blinking] {
      on iLed.shine(): {}
      on iLed.darken(): {}
      on iLed.blink(): {}
      on iTimer.timeout(): {}
    }
  }
}

In the above, we have added a new bool variable named “lit” to track the shining-darkened state changes when the LED is blinking. The light is off by default, hence variable lit is initialized to false. Booleans work in Dezyne as they do in C/C++/Java, including the negation operator !.

Filling in the event handlers for the initially dark LED:

[state.Dark] {
  on iLed.shine(): { // -> Shining, lit
     state = State.Shining;
     lit = true;
  }
  on iLed.darken(): {} // ignore
  on iLed.blink(): { // -> Blinking, half-second timer
     lit = false;
     state = State.Blinking;
     iTimer.start($500$);
  }
  on iTimer.timeout(): {} // -> shouldn’t occur, just ignore
}

The Shining state event handlers are essentially the same as for Dark. Blinking state handlers are below. When Blinking, on each timer timeout the light switches between off and on and restarts the timer.

[state.Blinking] {
  on iLed.shine(): {
     iTimer.cancel():
     state = State.Shining;
  }
  on iLed.darken(): {
     iTimer.cancel():
     state = State.Dark;
  }
  on iLed.blink(): {}
  on iTimer.timeout(): {
     lit = !lit;
     iTimer.start($500$);
  }
}

You can use if else instead of the negation operator when handling the timeout, as below. In Dezyne, the if-else construct can appear only within on-event behaviour.

[state.Blinking] {
  on iLed.shine(): {
    iTimer.cancel():
    state = State.Shining;
  }
  on iLed.darken(): {
    iTimer.cancel():
    state = State.Dark;
  }
  on iLed.blink(): {}
  on iTimer.timeout(): {
    if (lit) { lit = false; } else { lit = true; }
    iTimer.start($500$);
  }
}

Exercise: Complete the [state.Shining] event handlers, then verify and simulate.

Here is a screen shot showing some of the source and all of the Trace, Sequence and State Chart views for the completed, verified and simulated blink-able LED (the Shining event handlers are visible in it).

image

Challenge: The above model verifies completely and it simulates with no logic errors (by definition). But it has a functional bug related to exiting the Blinking state. Can you spot it?

Hint: observe the state variable “lit” in the Watch View window when you simulate. The answer is hidden below.


When exiting the Blinking state you must set the “lit” variable to the indicated new state, else the state variable might not match the actual on/off state of the LED. Which brings up an essential point: The first functional test of generated code from this model using an actual LED would probably reveal the state-tracking bug within minutes. You could then go directly to the Blinking state code in the model, insert the new assignments, regenerate the source, compile, and link – and the bug would be gone. Dezyne verifies your logic and helps you quickly validate your implemented system.



Simulation can generate trace inputs for automated regression tests

Observe that the Trace window contains the entire trace history to date after Dezyne processes each new simulation event. When you’re debugging a complex model, your automated test framework can save an arbitrarily long returned trace history to use as a regression test after a bug had been fixed

Enjoy this article? Don't forget to share.